:: FINSEQ_8 semantic presentation begin definition let D be set ; let f, g be FinSequence of D; :: original: ^ redefine funcf ^ g -> FinSequence of D; correctness coherence f ^ g is FinSequence of D; proof rng (f ^ g) c= (rng f) \/ (rng g) by FINSEQ_1:31; hence f ^ g is FinSequence of D ; ::_thesis: verum end; end; theorem :: FINSEQ_8:1 for D being non empty set for f, g being FinSequence of D st len f >= 1 holds mid ((f ^ g),1,(len f)) = f proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st len f >= 1 holds mid ((f ^ g),1,(len f)) = f let f, g be FinSequence of D; ::_thesis: ( len f >= 1 implies mid ((f ^ g),1,(len f)) = f ) assume A1: len f >= 1 ; ::_thesis: mid ((f ^ g),1,(len f)) = f then (len f) - 1 >= 0 by XREAL_1:48; then (len f) - 1 = (len f) -' 1 by XREAL_0:def_2; then A2: ((len f) -' 1) + 1 = len f ; 1 - 1 = 0 ; then A3: 1 -' 1 = 0 by XREAL_0:def_2; (f ^ g) | (len f) = f by FINSEQ_5:23; then ((f ^ g) /^ 0) | (len f) = f by FINSEQ_5:28; hence mid ((f ^ g),1,(len f)) = f by A1, A2, A3, FINSEQ_6:def_3; ::_thesis: verum end; theorem Th2: :: FINSEQ_8:2 for D being set for f being FinSequence of D for i being Element of NAT st i >= len f holds f /^ i = <*> D proof let D be set ; ::_thesis: for f being FinSequence of D for i being Element of NAT st i >= len f holds f /^ i = <*> D let f be FinSequence of D; ::_thesis: for i being Element of NAT st i >= len f holds f /^ i = <*> D let i be Element of NAT ; ::_thesis: ( i >= len f implies f /^ i = <*> D ) assume A1: i >= len f ; ::_thesis: f /^ i = <*> D percases ( i > len f or i = len f ) by A1, XXREAL_0:1; suppose i > len f ; ::_thesis: f /^ i = <*> D hence f /^ i = <*> D by RFINSEQ:def_1; ::_thesis: verum end; supposeA2: i = len f ; ::_thesis: f /^ i = <*> D then len (f /^ i) = (len f) - i by RFINSEQ:def_1 .= 0 by A2 ; hence f /^ i = <*> D ; ::_thesis: verum end; end; end; theorem :: FINSEQ_8:3 for D being non empty set for k1, k2 being Element of NAT holds mid ((<*> D),k1,k2) = <*> D proof let D be non empty set ; ::_thesis: for k1, k2 being Element of NAT holds mid ((<*> D),k1,k2) = <*> D let k1, k2 be Element of NAT ; ::_thesis: mid ((<*> D),k1,k2) = <*> D percases ( k1 <= k2 or k1 > k2 ) ; suppose k1 <= k2 ; ::_thesis: mid ((<*> D),k1,k2) = <*> D hence mid ((<*> D),k1,k2) = ((<*> D) /^ (k1 -' 1)) | ((k2 -' k1) + 1) by FINSEQ_6:def_3 .= (<*> D) | ((k2 -' k1) + 1) by FINSEQ_6:80 .= <*> D by FINSEQ_5:78 ; ::_thesis: verum end; suppose k1 > k2 ; ::_thesis: mid ((<*> D),k1,k2) = <*> D hence mid ((<*> D),k1,k2) = Rev (((<*> D) /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by FINSEQ_6:def_3 .= Rev ((<*> D) | ((k1 -' k2) + 1)) by FINSEQ_6:80 .= Rev (<*> D) by FINSEQ_5:78 .= <*> D by FINSEQ_5:79 ; ::_thesis: verum end; end; end; definition let f be FinSequence; let k1, k2 be Nat; func smid (f,k1,k2) -> FinSequence equals :: FINSEQ_8:def 1 (f /^ (k1 -' 1)) | ((k2 + 1) -' k1); correctness coherence (f /^ (k1 -' 1)) | ((k2 + 1) -' k1) is FinSequence; ; end; :: deftheorem defines smid FINSEQ_8:def_1_:_ for f being FinSequence for k1, k2 being Nat holds smid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1); definition let D be set ; let f be FinSequence of D; let k1, k2 be Nat; :: original: smid redefine func smid (f,k1,k2) -> FinSequence of D; correctness coherence smid (f,k1,k2) is FinSequence of D; proof smid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1) ; hence smid (f,k1,k2) is FinSequence of D ; ::_thesis: verum end; end; theorem Th4: :: FINSEQ_8:4 for f being FinSequence for k1, k2 being Element of NAT st k1 <= k2 holds smid (f,k1,k2) = mid (f,k1,k2) proof let f be FinSequence; ::_thesis: for k1, k2 being Element of NAT st k1 <= k2 holds smid (f,k1,k2) = mid (f,k1,k2) let k1, k2 be Element of NAT ; ::_thesis: ( k1 <= k2 implies smid (f,k1,k2) = mid (f,k1,k2) ) assume A1: k1 <= k2 ; ::_thesis: smid (f,k1,k2) = mid (f,k1,k2) then (k2 -' k1) + 1 = (k2 - k1) + 1 by XREAL_1:233 .= (k2 + 1) - k1 .= (k2 + 1) -' k1 by A1, NAT_1:12, XREAL_1:233 ; hence smid (f,k1,k2) = mid (f,k1,k2) by A1, FINSEQ_6:def_3; ::_thesis: verum end; theorem Th5: :: FINSEQ_8:5 for D being non empty set for f being FinSequence of D for k2 being Element of NAT holds smid (f,1,k2) = f | k2 proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k2 being Element of NAT holds smid (f,1,k2) = f | k2 let f be FinSequence of D; ::_thesis: for k2 being Element of NAT holds smid (f,1,k2) = f | k2 let k2 be Element of NAT ; ::_thesis: smid (f,1,k2) = f | k2 thus smid (f,1,k2) = (f /^ 0) | ((k2 + 1) -' 1) by NAT_2:8 .= f | ((k2 + 1) -' 1) by FINSEQ_5:28 .= f | k2 by NAT_D:34 ; ::_thesis: verum end; theorem Th6: :: FINSEQ_8:6 for D being non empty set for f being FinSequence of D for k2 being Element of NAT st len f <= k2 holds smid (f,1,k2) = f proof let D be non empty set ; ::_thesis: for f being FinSequence of D for k2 being Element of NAT st len f <= k2 holds smid (f,1,k2) = f let f be FinSequence of D; ::_thesis: for k2 being Element of NAT st len f <= k2 holds smid (f,1,k2) = f let k2 be Element of NAT ; ::_thesis: ( len f <= k2 implies smid (f,1,k2) = f ) assume A1: len f <= k2 ; ::_thesis: smid (f,1,k2) = f thus smid (f,1,k2) = f | k2 by Th5 .= f by A1, FINSEQ_1:58 ; ::_thesis: verum end; theorem Th7: :: FINSEQ_8:7 for D being set for f being FinSequence of D for k1, k2 being Element of NAT st k1 > k2 holds smid (f,k1,k2) = {} proof let D be set ; ::_thesis: for f being FinSequence of D for k1, k2 being Element of NAT st k1 > k2 holds smid (f,k1,k2) = {} let f be FinSequence of D; ::_thesis: for k1, k2 being Element of NAT st k1 > k2 holds smid (f,k1,k2) = {} let k1, k2 be Element of NAT ; ::_thesis: ( k1 > k2 implies smid (f,k1,k2) = {} ) assume A1: k1 > k2 ; ::_thesis: smid (f,k1,k2) = {} reconsider g = f /^ (k1 -' 1) as FinSequence of D ; k2 + 1 <= k1 by A1, NAT_1:13; then smid (f,k1,k2) = g | 0 by NAT_2:8; hence smid (f,k1,k2) = {} ; ::_thesis: verum end; theorem :: FINSEQ_8:8 for D being set for f being FinSequence of D for k2 being Element of NAT holds smid (f,0,k2) = smid (f,1,(k2 + 1)) proof let D be set ; ::_thesis: for f being FinSequence of D for k2 being Element of NAT holds smid (f,0,k2) = smid (f,1,(k2 + 1)) let f be FinSequence of D; ::_thesis: for k2 being Element of NAT holds smid (f,0,k2) = smid (f,1,(k2 + 1)) let k2 be Element of NAT ; ::_thesis: smid (f,0,k2) = smid (f,1,(k2 + 1)) thus smid (f,0,k2) = (f /^ 0) | ((k2 + 1) -' 0) by NAT_2:8 .= f | ((k2 + 1) -' 0) by FINSEQ_5:28 .= f | (k2 + 1) by NAT_D:40 .= f | (((k2 + 1) + 1) -' 1) by NAT_D:34 .= (f /^ 0) | (((k2 + 1) + 1) -' 1) by FINSEQ_5:28 .= smid (f,1,(k2 + 1)) by NAT_2:8 ; ::_thesis: verum end; theorem Th9: :: FINSEQ_8:9 for D being non empty set for f, g being FinSequence of D holds smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g let f, g be FinSequence of D; ::_thesis: smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g (((len g) + (len f)) + 1) -' ((len f) + 1) = ((len g) + ((len f) + 1)) -' ((len f) + 1) .= len g by NAT_D:34 ; then g | ((((len g) + (len f)) + 1) -' ((len f) + 1)) = g by FINSEQ_1:58; then ((f ^ g) /^ (len f)) | ((((len f) + (len g)) + 1) -' ((len f) + 1)) = g by FINSEQ_5:37; hence smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g by NAT_D:34; ::_thesis: verum end; definition let D be non empty set ; let f, g be FinSequence of D; func ovlpart (f,g) -> FinSequence of D means :Def2: :: FINSEQ_8:def 2 ( len it <= len g & it = smid (g,1,(len it)) & it = smid (f,(((len f) -' (len it)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len it ) ); existence ex b1 being FinSequence of D st ( len b1 <= len g & b1 = smid (g,1,(len b1)) & b1 = smid (f,(((len f) -' (len b1)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len b1 ) ) proof defpred S1[ Nat] means ( $1 <= len g & smid (g,1,$1) = smid (f,(((len f) -' $1) + 1),(len f)) ); A1: smid (g,1,0) = {} by Th7; ((len f) -' 0) + 1 = ((len f) - 0) + 1 by XREAL_1:233 .= (len f) + 1 ; then smid (f,(((len f) -' 0) + 1),(len f)) = {} by Th7, XREAL_1:29; then A2: ex m being Nat st S1[m] by A1; A3: for n being Nat st S1[n] holds n <= len g ; consider k being Nat such that A4: ( S1[k] & ( for n being Nat st S1[n] holds n <= k ) ) from NAT_1:sch_6(A3, A2); reconsider k = k as Element of NAT by ORDINAL1:def_12; set b = smid (g,1,k); now__::_thesis:_(_(_k_>_0_&_len_(smid_(g,1,k))_=_k_)_or_(_k_<=_0_&_len_(smid_(g,1,k))_=_k_)_) percases ( k > 0 or k <= 0 ) ; caseA5: k > 0 ; ::_thesis: len (smid (g,1,k)) = k then A6: 0 + 1 <= k by NAT_1:13; then A7: smid (g,1,k) = mid (g,1,k) by Th4; now__::_thesis:_(_(_len_g_>_0_&_len_(smid_(g,1,k))_=_k_)_or_(_len_g_<=_0_&_contradiction_)_) percases ( len g > 0 or len g <= 0 ) ; case len g > 0 ; ::_thesis: len (smid (g,1,k)) = k then 0 + 1 <= len g by NAT_1:13; hence len (smid (g,1,k)) = (k -' 1) + 1 by A4, A6, A7, FINSEQ_6:118 .= (k - 1) + 1 by A6, XREAL_1:233 .= k ; ::_thesis: verum end; case len g <= 0 ; ::_thesis: contradiction hence contradiction by A4, A5; ::_thesis: verum end; end; end; hence len (smid (g,1,k)) = k ; ::_thesis: verum end; caseA8: k <= 0 ; ::_thesis: len (smid (g,1,k)) = k then A9: k = 0 ; smid (g,1,k) = {} by A8, Th7; hence len (smid (g,1,k)) = k by A9; ::_thesis: verum end; end; end; hence ex b1 being FinSequence of D st ( len b1 <= len g & b1 = smid (g,1,(len b1)) & b1 = smid (f,(((len f) -' (len b1)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len b1 ) ) by A4; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of D st len b1 <= len g & b1 = smid (g,1,(len b1)) & b1 = smid (f,(((len f) -' (len b1)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len b1 ) & len b2 <= len g & b2 = smid (g,1,(len b2)) & b2 = smid (f,(((len f) -' (len b2)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len b2 ) holds b1 = b2 proof let a, b be FinSequence of D; ::_thesis: ( len a <= len g & a = smid (g,1,(len a)) & a = smid (f,(((len f) -' (len a)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len a ) & len b <= len g & b = smid (g,1,(len b)) & b = smid (f,(((len f) -' (len b)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len b ) implies a = b ) assume that A10: len a <= len g and A11: a = smid (g,1,(len a)) and A12: a = smid (f,(((len f) -' (len a)) + 1),(len f)) and A13: for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len a and A14: len b <= len g and A15: b = smid (g,1,(len b)) and A16: b = smid (f,(((len f) -' (len b)) + 1),(len f)) and A17: for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len b ; ::_thesis: a = b A18: len a <= len b by A10, A11, A12, A17; len b <= len a by A13, A14, A15, A16; hence a = b by A11, A15, A18, XXREAL_0:1; ::_thesis: verum end; end; :: deftheorem Def2 defines ovlpart FINSEQ_8:def_2_:_ for D being non empty set for f, g, b4 being FinSequence of D holds ( b4 = ovlpart (f,g) iff ( len b4 <= len g & b4 = smid (g,1,(len b4)) & b4 = smid (f,(((len f) -' (len b4)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds j <= len b4 ) ) ); theorem Th10: :: FINSEQ_8:10 for D being non empty set for f, g being FinSequence of D holds len (ovlpart (f,g)) <= len f proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds len (ovlpart (f,g)) <= len f let f, g be FinSequence of D; ::_thesis: len (ovlpart (f,g)) <= len f now__::_thesis:_not_len_(ovlpart_(f,g))_>_len_f assume A1: len (ovlpart (f,g)) > len f ; ::_thesis: contradiction then (len f) - (len (ovlpart (f,g))) < 0 by XREAL_1:49; then (len f) -' (len (ovlpart (f,g))) = 0 by XREAL_0:def_2; then smid (f,(((len f) -' (len (ovlpart (f,g)))) + 1),(len f)) = f by Th6; hence contradiction by A1, Def2; ::_thesis: verum end; hence len (ovlpart (f,g)) <= len f ; ::_thesis: verum end; definition let D be non empty set ; let f, g be FinSequence of D; func ovlcon (f,g) -> FinSequence of D equals :: FINSEQ_8:def 3 f ^ (g /^ (len (ovlpart (f,g)))); correctness coherence f ^ (g /^ (len (ovlpart (f,g)))) is FinSequence of D; ; end; :: deftheorem defines ovlcon FINSEQ_8:def_3_:_ for D being non empty set for f, g being FinSequence of D holds ovlcon (f,g) = f ^ (g /^ (len (ovlpart (f,g)))); theorem Th11: :: FINSEQ_8:11 for D being non empty set for f, g being FinSequence of D holds ovlcon (f,g) = (f | ((len f) -' (len (ovlpart (f,g))))) ^ g proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds ovlcon (f,g) = (f | ((len f) -' (len (ovlpart (f,g))))) ^ g let f, g be FinSequence of D; ::_thesis: ovlcon (f,g) = (f | ((len f) -' (len (ovlpart (f,g))))) ^ g A1: (len f) -' (len (ovlpart (f,g))) = (len f) - (len (ovlpart (f,g))) by Th10, XREAL_1:233; (len f) + 1 <= ((len f) + 1) + (len (ovlpart (f,g))) by NAT_1:12; then ((len f) + 1) - (len (ovlpart (f,g))) <= (((len f) + 1) + (len (ovlpart (f,g)))) - (len (ovlpart (f,g))) by XREAL_1:9; then A2: ((len f) + 1) -' (((len f) -' (len (ovlpart (f,g)))) + 1) = ((len f) + 1) - (((len f) -' (len (ovlpart (f,g)))) + 1) by A1, XREAL_1:233 .= len (ovlpart (f,g)) by A1 ; (len f) -' (len (ovlpart (f,g))) <= len f by NAT_D:35; then A3: len (f /^ ((len f) -' (len (ovlpart (f,g))))) = (len f) - ((len f) -' (len (ovlpart (f,g)))) by RFINSEQ:def_1 .= 0 + (len (ovlpart (f,g))) by A1 ; A4: ovlpart (f,g) = smid (f,(((len f) -' (len (ovlpart (f,g)))) + 1),(len f)) by Def2 .= (f /^ ((len f) -' (len (ovlpart (f,g))))) | (len (ovlpart (f,g))) by A2, NAT_D:34 .= f /^ ((len f) -' (len (ovlpart (f,g)))) by A3, FINSEQ_1:58 ; ovlpart (f,g) = smid (g,1,(len (ovlpart (f,g)))) by Def2 .= (g /^ ((0 + 1) -' 1)) | (len (ovlpart (f,g))) by NAT_D:34 .= (g /^ 0) | (len (ovlpart (f,g))) by NAT_D:34 .= g | (len (ovlpart (f,g))) by FINSEQ_5:28 ; hence ovlcon (f,g) = ((f | ((len f) -' (len (ovlpart (f,g))))) ^ (g | (len (ovlpart (f,g))))) ^ (g /^ (len (ovlpart (f,g)))) by A4, RFINSEQ:8 .= (f | ((len f) -' (len (ovlpart (f,g))))) ^ ((g | (len (ovlpart (f,g)))) ^ (g /^ (len (ovlpart (f,g))))) by FINSEQ_1:32 .= (f | ((len f) -' (len (ovlpart (f,g))))) ^ g by RFINSEQ:8 ; ::_thesis: verum end; definition let D be non empty set ; let f, g be FinSequence of D; func ovlldiff (f,g) -> FinSequence of D equals :: FINSEQ_8:def 4 f | ((len f) -' (len (ovlpart (f,g)))); coherence f | ((len f) -' (len (ovlpart (f,g)))) is FinSequence of D ; end; :: deftheorem defines ovlldiff FINSEQ_8:def_4_:_ for D being non empty set for f, g being FinSequence of D holds ovlldiff (f,g) = f | ((len f) -' (len (ovlpart (f,g)))); definition let D be non empty set ; let f, g be FinSequence of D; func ovlrdiff (f,g) -> FinSequence of D equals :: FINSEQ_8:def 5 g /^ (len (ovlpart (f,g))); coherence g /^ (len (ovlpart (f,g))) is FinSequence of D ; end; :: deftheorem defines ovlrdiff FINSEQ_8:def_5_:_ for D being non empty set for f, g being FinSequence of D holds ovlrdiff (f,g) = g /^ (len (ovlpart (f,g))); theorem :: FINSEQ_8:12 for D being non empty set for f, g being FinSequence of D holds ( ovlcon (f,g) = ((ovlldiff (f,g)) ^ (ovlpart (f,g))) ^ (ovlrdiff (f,g)) & ovlcon (f,g) = (ovlldiff (f,g)) ^ ((ovlpart (f,g)) ^ (ovlrdiff (f,g))) ) proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds ( ovlcon (f,g) = ((ovlldiff (f,g)) ^ (ovlpart (f,g))) ^ (ovlrdiff (f,g)) & ovlcon (f,g) = (ovlldiff (f,g)) ^ ((ovlpart (f,g)) ^ (ovlrdiff (f,g))) ) let f, g be FinSequence of D; ::_thesis: ( ovlcon (f,g) = ((ovlldiff (f,g)) ^ (ovlpart (f,g))) ^ (ovlrdiff (f,g)) & ovlcon (f,g) = (ovlldiff (f,g)) ^ ((ovlpart (f,g)) ^ (ovlrdiff (f,g))) ) (ovlpart (f,g)) ^ (g /^ (len (ovlpart (f,g)))) = (smid (g,1,(len (ovlpart (f,g))))) ^ (g /^ (len (ovlpart (f,g)))) by Def2 .= (g | (len (ovlpart (f,g)))) ^ (g /^ (len (ovlpart (f,g)))) by Th5 .= g by RFINSEQ:8 ; hence ovlcon (f,g) = (f | ((len f) -' (len (ovlpart (f,g))))) ^ ((ovlpart (f,g)) ^ (g /^ (len (ovlpart (f,g))))) by Th11 .= ((ovlldiff (f,g)) ^ (ovlpart (f,g))) ^ (ovlrdiff (f,g)) by FINSEQ_1:32 ; ::_thesis: ovlcon (f,g) = (ovlldiff (f,g)) ^ ((ovlpart (f,g)) ^ (ovlrdiff (f,g))) hence ovlcon (f,g) = (ovlldiff (f,g)) ^ ((ovlpart (f,g)) ^ (ovlrdiff (f,g))) by FINSEQ_1:32; ::_thesis: verum end; theorem :: FINSEQ_8:13 for D being non empty set for f being FinSequence of D holds ( ovlcon (f,f) = f & ovlpart (f,f) = f & ovlldiff (f,f) = {} & ovlrdiff (f,f) = {} ) proof let D be non empty set ; ::_thesis: for f being FinSequence of D holds ( ovlcon (f,f) = f & ovlpart (f,f) = f & ovlldiff (f,f) = {} & ovlrdiff (f,f) = {} ) let f be FinSequence of D; ::_thesis: ( ovlcon (f,f) = f & ovlpart (f,f) = f & ovlldiff (f,f) = {} & ovlrdiff (f,f) = {} ) A1: ovlpart (f,f) = smid (f,1,(len (ovlpart (f,f)))) by Def2; ((len f) -' (len f)) + 1 = ((len f) - (len f)) + 1 by XREAL_1:233 .= 0 + 1 ; then smid (f,1,(len f)) = smid (f,(((len f) -' (len f)) + 1),(len f)) ; then A2: len f <= len (ovlpart (f,f)) by Def2; then A3: ovlcon (f,f) = f ^ (<*> D) by Th2 .= f by FINSEQ_1:34 ; A4: ovlldiff (f,f) = f | ((len f) -' (len f)) by A1, A2, Th6 .= f | 0 by XREAL_1:232 .= {} ; ovlrdiff (f,f) = <*> D by A2, Th2 .= {} ; hence ( ovlcon (f,f) = f & ovlpart (f,f) = f & ovlldiff (f,f) = {} & ovlrdiff (f,f) = {} ) by A1, A2, A3, A4, Th6; ::_thesis: verum end; theorem :: FINSEQ_8:14 for D being non empty set for f, g being FinSequence of D holds ( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f ) proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds ( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f ) let f, g be FinSequence of D; ::_thesis: ( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f ) A1: len (ovlpart ((f ^ g),g)) <= len g by Def2; A2: smid (g,1,(len g)) = g | (len g) by Th5 .= g by FINSEQ_1:58 ; ((len (f ^ g)) -' (len g)) + 1 = (((len f) + (len g)) -' (len g)) + 1 by FINSEQ_1:22 .= (len f) + 1 by NAT_D:34 ; then smid ((f ^ g),(((len (f ^ g)) -' (len g)) + 1),(len (f ^ g))) = smid ((f ^ g),((len f) + 1),((len f) + (len g))) by FINSEQ_1:22 .= g by Th9 ; then len g <= len (ovlpart ((f ^ g),g)) by A2, Def2; then A3: len g = len (ovlpart ((f ^ g),g)) by A1, XXREAL_0:1; A4: ovlpart ((f ^ g),g) = smid (g,1,(len (ovlpart ((f ^ g),g)))) by Def2 .= g | (len g) by A3, Th5 .= g by FINSEQ_1:58 ; A5: len (ovlpart (f,(f ^ g))) <= len f by Th10; ((len f) -' (len f)) + 1 = 0 + 1 by XREAL_1:232 .= 1 ; then A6: smid (f,(((len f) -' (len f)) + 1),(len f)) = (f /^ ((0 + 1) -' 1)) | (len f) by NAT_D:34 .= (f /^ 0) | (len f) by NAT_D:34 .= f | (len f) by FINSEQ_5:28 .= f by FINSEQ_1:58 ; len f <= (len f) + (len g) by NAT_1:12; then A7: len f <= len (f ^ g) by FINSEQ_1:22; smid ((f ^ g),1,(len f)) = (f ^ g) | (len f) by Th5 .= f by FINSEQ_5:23 ; then len f <= len (ovlpart (f,(f ^ g))) by A6, A7, Def2; then A8: len f = len (ovlpart (f,(f ^ g))) by A5, XXREAL_0:1; ovlpart (f,(f ^ g)) = smid ((f ^ g),1,(len (ovlpart (f,(f ^ g))))) by Def2 .= (f ^ g) | (len f) by A8, Th5 .= f by FINSEQ_5:23 ; hence ( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f ) by A4; ::_thesis: verum end; theorem Th15: :: FINSEQ_8:15 for D being non empty set for f, g being FinSequence of D holds ( len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) & len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) & len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) ) proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds ( len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) & len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) & len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) ) let f, g be FinSequence of D; ::_thesis: ( len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) & len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) & len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) ) A1: len (ovlpart (f,g)) <= len g by Def2; A2: len (ovlcon (f,g)) = (len f) + (len (g /^ (len (ovlpart (f,g))))) by FINSEQ_1:22 .= (len f) + ((len g) -' (len (ovlpart (f,g)))) by RFINSEQ:29 .= (len f) + ((len g) - (len (ovlpart (f,g)))) by A1, XREAL_1:233 ; hence A3: len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) ; ::_thesis: ( len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) & len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) ) A4: len (ovlpart (f,g)) <= len g by Def2; hence len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) by A3, NAT_1:12, XREAL_1:233; ::_thesis: len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) thus len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) by A2, A4, XREAL_1:233; ::_thesis: verum end; theorem Th16: :: FINSEQ_8:16 for D being non empty set for f, g being FinSequence of D holds ( len (ovlpart (f,g)) <= len f & len (ovlpart (f,g)) <= len g ) proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds ( len (ovlpart (f,g)) <= len f & len (ovlpart (f,g)) <= len g ) let f, g be FinSequence of D; ::_thesis: ( len (ovlpart (f,g)) <= len f & len (ovlpart (f,g)) <= len g ) now__::_thesis:_not_len_(ovlpart_(f,g))_>_len_f assume A1: len (ovlpart (f,g)) > len f ; ::_thesis: contradiction ovlpart (f,g) = smid (f,(((len f) -' (len (ovlpart (f,g)))) + 1),(len f)) by Def2 .= smid (f,(0 + 1),(len f)) by A1, NAT_2:8 .= f by Th6 ; hence contradiction by A1; ::_thesis: verum end; hence ( len (ovlpart (f,g)) <= len f & len (ovlpart (f,g)) <= len g ) by Def2; ::_thesis: verum end; definition let D be non empty set ; let CR be FinSequence of D; predCR separates_uniquely means :Def6: :: FINSEQ_8:def 6 for f being FinSequence of D for i, j being Element of NAT st 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) & smid (f,i,((i + (len CR)) -' 1)) = CR holds j -' i >= len CR; end; :: deftheorem Def6 defines separates_uniquely FINSEQ_8:def_6_:_ for D being non empty set for CR being FinSequence of D holds ( CR separates_uniquely iff for f being FinSequence of D for i, j being Element of NAT st 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) & smid (f,i,((i + (len CR)) -' 1)) = CR holds j -' i >= len CR ); theorem :: FINSEQ_8:17 for D being non empty set for CR being FinSequence of D holds ( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 ) proof let D be non empty set ; ::_thesis: for CR being FinSequence of D holds ( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 ) let CR be FinSequence of D; ::_thesis: ( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 ) set p = ovlpart ((CR /^ 1),CR); A1: now__::_thesis:_(_CR_separates_uniquely_implies_len_(ovlpart_((CR_/^_1),CR))_=_0_) assume A2: CR separates_uniquely ; ::_thesis: len (ovlpart ((CR /^ 1),CR)) = 0 set f = (CR | 1) ^ (ovlcon ((CR /^ 1),CR)); A3: (CR | 1) ^ (ovlcon ((CR /^ 1),CR)) = ((CR | 1) ^ (CR /^ 1)) ^ (CR /^ (len (ovlpart ((CR /^ 1),CR)))) by FINSEQ_1:32 .= CR ^ (CR /^ (len (ovlpart ((CR /^ 1),CR)))) by RFINSEQ:8 ; A4: (CR | 1) ^ (ovlcon ((CR /^ 1),CR)) = (CR | 1) ^ (((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR))))) ^ CR) by Th11 .= ((CR | 1) ^ ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR)))))) ^ CR by FINSEQ_1:32 ; A5: len ((CR | 1) ^ ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR)))))) = (len (CR | 1)) + (len ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR)))))) by FINSEQ_1:22 .= (len (CR | 1)) + ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR)))) by FINSEQ_1:59, NAT_D:35 .= (len (CR | 1)) + ((len (CR /^ 1)) - (len (ovlpart ((CR /^ 1),CR)))) by Th16, XREAL_1:233 .= ((len (CR | 1)) + (len (CR /^ 1))) - (len (ovlpart ((CR /^ 1),CR))) .= (len ((CR | 1) ^ (CR /^ 1))) - (len (ovlpart ((CR /^ 1),CR))) by FINSEQ_1:22 .= (len CR) - (len (ovlpart ((CR /^ 1),CR))) by RFINSEQ:8 ; A6: (len CR) - (len (ovlpart ((CR /^ 1),CR))) = (len CR) -' (len (ovlpart ((CR /^ 1),CR))) by Th16, XREAL_1:233; A7: ((len CR) + 1) -' 1 = len CR by NAT_D:34; A8: len (ovlpart ((CR /^ 1),CR)) <= len CR by Def2; A9: len ((CR | 1) ^ (ovlcon ((CR /^ 1),CR))) = (len (CR | 1)) + (len (ovlcon ((CR /^ 1),CR))) by FINSEQ_1:22 .= (len (CR | 1)) + (((len (CR /^ 1)) + (len CR)) - (len (ovlpart ((CR /^ 1),CR)))) by Th15 .= ((len (CR | 1)) + (len (CR /^ 1))) + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) .= (len ((CR | 1) ^ (CR /^ 1))) + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) by FINSEQ_1:22 .= (len CR) + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) by RFINSEQ:8 ; set j = ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))); A10: len CR < (len CR) + 1 by XREAL_1:29; A11: len (ovlpart ((CR /^ 1),CR)) <= len CR by Def2; then A12: ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))) = (1 + (len CR)) - (len (ovlpart ((CR /^ 1),CR))) by A10, XREAL_1:233, XXREAL_0:2 .= 1 + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) .= 1 + ((len CR) -' (len (ovlpart ((CR /^ 1),CR)))) by A11, XREAL_1:233 ; then A13: 1 <= ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))) by NAT_1:12; A14: smid (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))),1,((1 + (len CR)) -' 1)) = (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))) /^ ((0 + 1) -' 1)) | (((len CR) + 1) -' 1) by NAT_D:34 .= (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))) /^ 0) | (len CR) by A7, NAT_D:34 .= ((CR | 1) ^ (ovlcon ((CR /^ 1),CR))) | (len CR) by FINSEQ_5:28 .= CR by A3, FINSEQ_5:23 ; (((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) -' 1) + 1 = (((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) - 1) + 1 by A13, NAT_1:12, XREAL_1:233 .= (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR) ; then A15: ((((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) -' 1) + 1) -' (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) = ((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) - (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) by NAT_1:12, XREAL_1:233 .= len CR ; 1 <= 1 + ((len CR) -' (len (ovlpart ((CR /^ 1),CR)))) by NAT_1:12; then 1 <= 1 + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) by A8, XREAL_1:233; then 1 <= (1 + (len CR)) - (len (ovlpart ((CR /^ 1),CR))) ; then 1 <= ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))) by A8, NAT_1:12, XREAL_1:233; then (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) -' 1 = (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) - 1 by XREAL_1:233; then (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) -' 1 = (((len CR) + 1) - (len (ovlpart ((CR /^ 1),CR)))) - 1 by A8, NAT_1:12, XREAL_1:233 .= (((len CR) + 1) - 1) - (len (ovlpart ((CR /^ 1),CR))) .= (len CR) -' (len (ovlpart ((CR /^ 1),CR))) by A11, XREAL_1:233 ; then A16: smid (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))),(((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))),(((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) -' 1)) = CR | (len CR) by A4, A5, A6, A15, FINSEQ_5:37 .= smid (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))),1,((1 + (len CR)) -' 1)) by A14, FINSEQ_1:58 ; len (ovlpart ((CR /^ 1),CR)) <= len (CR /^ 1) by Th10; then len (ovlpart ((CR /^ 1),CR)) <= (len CR) -' 1 by RFINSEQ:29; then A17: ((len CR) + 1) - (len (ovlpart ((CR /^ 1),CR))) >= (1 + (len CR)) - ((len CR) -' 1) by XREAL_1:10; now__::_thesis:_(_(_len_CR_>=_1_&_len_(ovlpart_((CR_/^_1),CR))_=_0_)_or_(_len_CR_<_1_&_len_(ovlpart_((CR_/^_1),CR))_=_0_)_) percases ( len CR >= 1 or len CR < 1 ) ; case len CR >= 1 ; ::_thesis: len (ovlpart ((CR /^ 1),CR)) = 0 then (1 + (len CR)) - ((len CR) -' 1) = (1 + (len CR)) - ((len CR) - 1) by XREAL_1:233 .= 1 + 1 ; then 1 < ((len CR) + 1) - (len (ovlpart ((CR /^ 1),CR))) by A17, XXREAL_0:2; then A18: 1 < ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))) by A10, A11, XREAL_1:233, XXREAL_0:2; ((((len CR) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) + 1) -' 1 <= (len CR) + ((len CR) -' (len (ovlpart ((CR /^ 1),CR)))) by NAT_D:34; then ((1 + ((len CR) -' (len (ovlpart ((CR /^ 1),CR))))) + (len CR)) -' 1 <= (len CR) + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) by A11, XREAL_1:233; then A19: (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) -' 1 >= len CR by A2, A9, A12, A14, A16, A18, Def6; A20: (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) -' 1 = (1 + ((len CR) -' (len (ovlpart ((CR /^ 1),CR))))) - 1 by A12, NAT_1:12, XREAL_1:233 .= (len CR) -' (len (ovlpart ((CR /^ 1),CR))) ; A21: (len CR) -' (len (ovlpart ((CR /^ 1),CR))) <= len CR by NAT_D:35; (len CR) -' (len (ovlpart ((CR /^ 1),CR))) = (len CR) - (len (ovlpart ((CR /^ 1),CR))) by A11, XREAL_1:233; then (len CR) - (len (ovlpart ((CR /^ 1),CR))) = len CR by A19, A20, A21, XXREAL_0:1; hence len (ovlpart ((CR /^ 1),CR)) = 0 ; ::_thesis: verum end; case len CR < 1 ; ::_thesis: len (ovlpart ((CR /^ 1),CR)) = 0 then len CR < 0 + 1 ; then len CR <= 0 by NAT_1:13; hence len (ovlpart ((CR /^ 1),CR)) = 0 by Def2; ::_thesis: verum end; end; end; hence len (ovlpart ((CR /^ 1),CR)) = 0 ; ::_thesis: verum end; now__::_thesis:_(_len_(ovlpart_((CR_/^_1),CR))_=_0_implies_CR_separates_uniquely_) assume A22: len (ovlpart ((CR /^ 1),CR)) = 0 ; ::_thesis: CR separates_uniquely for f being FinSequence of D for i, j being Element of NAT st 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) & smid (f,i,((i + (len CR)) -' 1)) = CR holds j -' i >= len CR proof let f be FinSequence of D; ::_thesis: for i, j being Element of NAT st 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) & smid (f,i,((i + (len CR)) -' 1)) = CR holds j -' i >= len CR let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) & smid (f,i,((i + (len CR)) -' 1)) = CR implies j -' i >= len CR ) assume that A23: 1 <= i and A24: i < j and A25: (j + (len CR)) -' 1 <= len f and A26: smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) and A27: smid (f,i,((i + (len CR)) -' 1)) = CR ; ::_thesis: j -' i >= len CR A28: j - i > 0 by A24, XREAL_1:50; then A29: j -' i = j - i by XREAL_0:def_2; A30: i + (j -' i) = (j - i) + i by A28, XREAL_0:def_2 .= j ; now__::_thesis:_(_(_len_CR_<=_0_&_j_-'_i_>=_len_CR_)_or_(_len_CR_>_0_&_j_-'_i_>=_len_CR_)_) percases ( len CR <= 0 or len CR > 0 ) ; case len CR <= 0 ; ::_thesis: j -' i >= len CR hence j -' i >= len CR ; ::_thesis: verum end; caseA31: len CR > 0 ; ::_thesis: j -' i >= len CR then A32: 0 + 1 <= len CR by NAT_1:13; then A33: (len CR) -' 1 = (len CR) - 1 by XREAL_1:233; A34: (i + (len CR)) -' 1 = (i + (len CR)) - 1 by A32, NAT_1:12, XREAL_1:233; A35: i <= i + ((len CR) -' 1) by NAT_1:12; then A36: 1 <= (i + (len CR)) -' 1 by A23, A33, A34, XXREAL_0:2; set k = j -' i; A37: 0 + 1 <= j -' i by A28, A29, NAT_1:13; then A38: (j -' i) - 1 = (j -' i) -' 1 by XREAL_1:233; A39: i + ((j -' i) -' 1) = i + ((j -' i) - 1) by A37, XREAL_1:233 .= i + ((j - i) - 1) by A28, XREAL_0:def_2 .= j - 1 ; i + 1 <= j by A24, NAT_1:13; then A40: (i + 1) - 1 <= j - 1 by XREAL_1:9; then A41: j -' 1 = j - 1 by XREAL_0:def_2; j - i > 0 by A24, XREAL_1:50; then j -' i > 0 by XREAL_0:def_2; then A42: j -' i >= 0 + 1 by NAT_1:13; A43: j -' 1 <= (j -' 1) + (len CR) by NAT_1:12; j <= j + (len CR) by NAT_1:12; then A44: i < j + (len CR) by A24, XXREAL_0:2; (j -' 1) + (len CR) = (j - 1) + (len CR) by A40, XREAL_0:def_2 .= (j + (len CR)) - 1 .= (j + (len CR)) -' 1 by A23, A44, XREAL_1:233, XXREAL_0:2 ; then A45: i + ((j -' i) -' 1) <= len f by A25, A39, A41, A43, XXREAL_0:2; now__::_thesis:_not_j_-'_i_<_len_CR assume A46: j -' i < len CR ; ::_thesis: contradiction then (j -' i) - 1 < (len CR) - 1 by XREAL_1:9; then (j -' i) -' 1 < (len CR) - 1 by A42, XREAL_1:233; then (j -' i) -' 1 < (len CR) -' 1 by A32, XREAL_1:233; then A47: ((j -' i) -' 1) + 1 <= (len CR) -' 1 by NAT_1:13; A48: (j -' i) - (j -' i) < (len CR) - (j -' i) by A46, XREAL_1:9; then 0 < (len CR) -' (j -' i) by XREAL_0:def_2; then A49: 0 + 1 <= (len CR) -' (j -' i) by NAT_1:13; A50: (len CR) -' (j -' i) = (len CR) - (j -' i) by A48, XREAL_0:def_2; 1 < len CR by A37, A46, XXREAL_0:2; then 1 + 1 <= len CR by NAT_1:13; then A51: (1 + 1) - 1 <= (len CR) - 1 by XREAL_1:9; A52: (len CR) -' 1 = (len CR) - 1 by A37, A46, XREAL_1:233, XXREAL_0:2; then A53: (len CR) -' (j -' i) <= (len CR) -' 1 by A37, A50, XREAL_1:10; i <= i + ((j -' i) -' 1) by NAT_1:12; then A54: i <= len f by A45, XXREAL_0:2; (j + (len CR)) -' 1 = (j + (len CR)) - 1 by A23, A44, XREAL_1:233, XXREAL_0:2 .= j + ((len CR) - 1) .= j + ((len CR) -' 1) by A32, XREAL_1:233 ; then j <= (j + (len CR)) -' 1 by NAT_1:12; then A55: j <= len f by A25, XXREAL_0:2; i + 1 <= j by A24, NAT_1:13; then (i + 1) + (len CR) <= j + (len CR) by XREAL_1:7; then A56: ((i + 1) + (len CR)) - 1 <= (j + (len CR)) - 1 by XREAL_1:9; A57: 1 < j by A23, A24, XXREAL_0:2; A58: j < j + (len CR) by A31, XREAL_1:29; then A59: 1 < j + (len CR) by A57, XXREAL_0:2; A60: (j + (len CR)) -' 1 = (j + (len CR)) - 1 by A57, A58, XREAL_1:233, XXREAL_0:2; then A61: ((i + 1) - 1) + (len CR) <= len f by A25, A56, XXREAL_0:2; i + (len CR) <= (i + (len CR)) + 1 by NAT_1:12; then (i + (len CR)) -' 1 <= i + (len CR) by A34, XREAL_1:20; then A62: (i + (len CR)) -' 1 <= len f by A61, XXREAL_0:2; 0 < (j + (len CR)) - 1 by A59, XREAL_1:50; then A63: 0 + 1 <= (j + (len CR)) -' 1 by A60, NAT_1:13; j + 1 <= j + (len CR) by A58, NAT_1:13; then A64: (j + 1) - 1 <= (j + (len CR)) - 1 by XREAL_1:9; A65: len CR <= (len CR) + (j -' i) by NAT_1:12; then A66: (len CR) - (j -' i) <= len CR by XREAL_1:20; A67: (len CR) -' (j -' i) <= len CR by A50, A65, XREAL_1:20; A68: len (smid (CR,1,((len CR) -' (j -' i)))) = len (mid (CR,1,((len CR) -' (j -' i)))) by A49, Th4; A69: len (mid (CR,1,((len CR) -' (j -' i)))) = (((len CR) -' (j -' i)) -' 1) + 1 by A32, A49, A50, A66, FINSEQ_6:118 .= (((len CR) -' (j -' i)) - 1) + 1 by A49, XREAL_1:233 .= (len CR) -' (j -' i) ; A70: ((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1 = (((len CR) -' 1) -' ((len CR) -' (j -' i))) + 1 by RFINSEQ:29 .= (((len CR) -' 1) - ((len CR) -' (j -' i))) + 1 by A53, XREAL_1:233 .= (((len CR) - 1) - ((len CR) - (j -' i))) + 1 by A37, A46, A50, XREAL_1:233, XXREAL_0:2 .= j -' i ; A71: len (CR /^ 1) = (len CR) -' 1 by RFINSEQ:29; then A72: smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1))) = mid ((CR /^ 1),(j -' i),((len CR) -' 1)) by A38, A47, A70, Th4; A73: len (mid ((CR /^ 1),(j -' i),((len CR) -' 1))) = (((len CR) -' 1) -' (j -' i)) + 1 by A37, A38, A47, A51, A52, A71, FINSEQ_6:118 .= (((len CR) -' 1) - (j -' i)) + 1 by A38, A47, XREAL_1:233 .= (((len CR) - 1) - (j -' i)) + 1 by A37, A46, XREAL_1:233, XXREAL_0:2 .= (len CR) -' (j -' i) by A48, XREAL_0:def_2 ; for jj being Nat st 1 <= jj & jj <= (len CR) -' (j -' i) holds (smid (CR,1,((len CR) -' (j -' i)))) . jj = (smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)))) . jj proof let jj be Nat; ::_thesis: ( 1 <= jj & jj <= (len CR) -' (j -' i) implies (smid (CR,1,((len CR) -' (j -' i)))) . jj = (smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)))) . jj ) assume that A74: 1 <= jj and A75: jj <= (len CR) -' (j -' i) ; ::_thesis: (smid (CR,1,((len CR) -' (j -' i)))) . jj = (smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)))) . jj A76: jj + (j -' i) <= ((len CR) -' (j -' i)) + (j -' i) by A75, XREAL_1:7; then A77: (jj + (j -' i)) - 1 <= (len CR) - 1 by A50, XREAL_1:9; reconsider j1 = jj as Element of NAT by ORDINAL1:def_12; A78: len (mid (f,i,((i + (len CR)) -' 1))) = (((i + (len CR)) -' 1) -' i) + 1 by A23, A33, A34, A35, A36, A54, A62, FINSEQ_6:118 .= (((i + (len CR)) - 1) - i) + 1 by A33, A34, A35, XREAL_1:233 .= len CR ; (len CR) -' (j -' i) <= len CR by NAT_D:35; then A79: jj <= len CR by A75, XXREAL_0:2; A80: 1 <= jj + ((j -' i) -' 1) by A74, NAT_1:12; A81: jj + ((j -' i) -' 1) = jj + ((j -' i) - 1) by A37, XREAL_1:233 .= (jj + (j -' i)) - 1 .= (jj + (j -' i)) -' 1 by A74, NAT_1:12, XREAL_1:233 ; A82: 1 <= jj + (j -' i) by A74, NAT_1:12; (jj + (j -' i)) -' 1 <= (len CR) - 1 by A74, A77, NAT_1:12, XREAL_1:233; then (jj + (j -' i)) -' 1 <= (len CR) -' 1 by A32, XREAL_1:233; then (jj + (j -' i)) -' 1 in Seg (len (CR /^ 1)) by A71, A80, A81; then A83: (jj + (j -' i)) -' 1 in dom (CR /^ 1) by FINSEQ_1:def_3; A84: smid (f,j,((j + (len CR)) -' 1)) = mid (f,j,((j + (len CR)) -' 1)) by A60, A64, Th4; thus (smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)))) . jj = (CR /^ 1) . ((j1 + (j -' i)) -' 1) by A37, A38, A47, A51, A52, A71, A72, A73, A74, A75, FINSEQ_6:118 .= (smid (f,i,((i + (len CR)) -' 1))) . (((jj + (j -' i)) -' 1) + 1) by A27, A32, A83, RFINSEQ:def_1 .= (mid (f,i,((i + (len CR)) -' 1))) . (((jj + (j -' i)) -' 1) + 1) by A33, A34, A35, Th4 .= (mid (f,i,((i + (len CR)) -' 1))) . (((jj + (j -' i)) - 1) + 1) by A74, NAT_1:12, XREAL_1:233 .= f . ((i + (j1 + (j -' i))) -' 1) by A23, A33, A34, A35, A36, A50, A54, A62, A76, A78, A82, FINSEQ_6:118 .= f . (((i + (j -' i)) + j1) -' 1) .= CR . jj by A25, A26, A27, A30, A55, A57, A60, A63, A64, A74, A79, A84, FINSEQ_6:118 .= CR . ((j1 + 1) -' 1) by NAT_D:34 .= (mid (CR,1,((len CR) -' (j -' i)))) . j1 by A32, A49, A50, A66, A69, A74, A75, FINSEQ_6:118 .= (smid (CR,1,((len CR) -' (j -' i)))) . jj by A49, Th4 ; ::_thesis: verum end; then smid (CR,1,((len CR) -' (j -' i))) = smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1))) by A68, A69, A72, A73, FINSEQ_1:14; then (len CR) -' (j -' i) <= len (ovlpart ((CR /^ 1),CR)) by A67, Def2; hence contradiction by A22, A48, XREAL_0:def_2; ::_thesis: verum end; hence j -' i >= len CR ; ::_thesis: verum end; end; end; hence j -' i >= len CR ; ::_thesis: verum end; hence CR separates_uniquely by Def6; ::_thesis: verum end; hence ( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 ) by A1; ::_thesis: verum end; definition let D be non empty set ; let f, g be FinSequence of D; let n be Element of NAT ; predg is_substring_of f,n means :Def7: :: FINSEQ_8:def 7 ( len g > 0 implies ex i being Element of NAT st ( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ); correctness ; end; :: deftheorem Def7 defines is_substring_of FINSEQ_8:def_7_:_ for D being non empty set for f, g being FinSequence of D for n being Element of NAT holds ( g is_substring_of f,n iff ( len g > 0 implies ex i being Element of NAT st ( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) ); theorem :: FINSEQ_8:18 for D being non empty set for f, g being FinSequence of D for n, m being Element of NAT st m >= n & g is_substring_of f,m holds g is_substring_of f,n proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D for n, m being Element of NAT st m >= n & g is_substring_of f,m holds g is_substring_of f,n let f, g be FinSequence of D; ::_thesis: for n, m being Element of NAT st m >= n & g is_substring_of f,m holds g is_substring_of f,n let n, m be Element of NAT ; ::_thesis: ( m >= n & g is_substring_of f,m implies g is_substring_of f,n ) assume that A1: m >= n and A2: g is_substring_of f,m ; ::_thesis: g is_substring_of f,n now__::_thesis:_(_(_len_g_>_0_&_g_is_substring_of_f,n_)_or_(_len_g_<=_0_&_g_is_substring_of_f,n_)_) percases ( len g > 0 or len g <= 0 ) ; case len g > 0 ; ::_thesis: g is_substring_of f,n then consider i being Element of NAT such that A3: m <= i and A4: i <= len f and A5: mid (f,i,((i -' 1) + (len g))) = g by A2, Def7; n <= i by A1, A3, XXREAL_0:2; hence g is_substring_of f,n by A4, A5, Def7; ::_thesis: verum end; case len g <= 0 ; ::_thesis: g is_substring_of f,n hence g is_substring_of f,n by Def7; ::_thesis: verum end; end; end; hence g is_substring_of f,n ; ::_thesis: verum end; theorem Th19: :: FINSEQ_8:19 for D being non empty set for f being FinSequence of D st 1 <= len f holds f is_substring_of f,1 proof let D be non empty set ; ::_thesis: for f being FinSequence of D st 1 <= len f holds f is_substring_of f,1 let f be FinSequence of D; ::_thesis: ( 1 <= len f implies f is_substring_of f,1 ) assume A1: 1 <= len f ; ::_thesis: f is_substring_of f,1 (1 -' 1) + (len f) = 0 + (len f) by NAT_2:8 .= len f ; then mid (f,1,((1 -' 1) + (len f))) = f by A1, FINSEQ_6:120; hence f is_substring_of f,1 by A1, Def7; ::_thesis: verum end; theorem Th20: :: FINSEQ_8:20 for D being non empty set for f, g being FinSequence of D st g is_substring_of f, 0 holds g is_substring_of f,1 proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st g is_substring_of f, 0 holds g is_substring_of f,1 let f, g be FinSequence of D; ::_thesis: ( g is_substring_of f, 0 implies g is_substring_of f,1 ) assume A1: g is_substring_of f, 0 ; ::_thesis: g is_substring_of f,1 now__::_thesis:_(_(_len_g_>_0_&_g_is_substring_of_f,1_)_or_(_len_g_<=_0_&_g_is_substring_of_f,1_)_) percases ( len g > 0 or len g <= 0 ) ; caseA2: len g > 0 ; ::_thesis: g is_substring_of f,1 then consider i being Element of NAT such that 0 <= i and A3: i <= len f and A4: mid (f,i,((i -' 1) + (len g))) = g by A1, Def7; A5: len g >= 0 + 1 by A2, NAT_1:13; now__::_thesis:_(_(_i_=_0_&_g_is_substring_of_f,1_)_or_(_i_<>_0_&_g_is_substring_of_f,1_)_) percases ( i = 0 or i <> 0 ) ; caseA6: i = 0 ; ::_thesis: g is_substring_of f,1 0 - 1 < 0 ; then A7: i -' 1 = 0 by A6, XREAL_0:def_2; then A8: (f /^ (0 -' 1)) | (((len g) -' 0) + 1) = g by A4, A6, FINSEQ_6:def_3; (len g) -' 0 = (len g) - 0 by XREAL_0:def_2 .= len g ; then A9: f | ((len g) + 1) = g by A6, A7, A8, FINSEQ_5:28; now__::_thesis:_(_(_(len_g)_+_1_>=_len_f_&_g_is_substring_of_f,1_)_or_(_(len_g)_+_1_<_len_f_&_contradiction_)_) percases ( (len g) + 1 >= len f or (len g) + 1 < len f ) ; case (len g) + 1 >= len f ; ::_thesis: g is_substring_of f,1 then f = g by A9, FINSEQ_1:58; hence g is_substring_of f,1 by A5, Th19; ::_thesis: verum end; caseA10: (len g) + 1 < len f ; ::_thesis: contradiction dom (f | (Seg ((len g) + 1))) = (dom f) /\ (Seg ((len g) + 1)) by RELAT_1:61 .= (Seg (len f)) /\ (Seg ((len g) + 1)) by FINSEQ_1:def_3 .= Seg ((len g) + 1) by A10, FINSEQ_1:7 ; then len g = (len g) + 1 by A9, FINSEQ_1:def_3; hence contradiction ; ::_thesis: verum end; end; end; hence g is_substring_of f,1 ; ::_thesis: verum end; case i <> 0 ; ::_thesis: g is_substring_of f,1 then i >= 0 + 1 by NAT_1:13; hence g is_substring_of f,1 by A3, A4, Def7; ::_thesis: verum end; end; end; hence g is_substring_of f,1 ; ::_thesis: verum end; case len g <= 0 ; ::_thesis: g is_substring_of f,1 hence g is_substring_of f,1 by Def7; ::_thesis: verum end; end; end; hence g is_substring_of f,1 ; ::_thesis: verum end; notation let D be non empty set ; let g, f be FinSequence of D; synonym g is_preposition_of f for D c= g; end; definition let D be non empty set ; let g, f be FinSequence of D; :: original: is_preposition_of redefine predg c= f means :Def8: :: FINSEQ_8:def 8 ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ); compatibility ( f is_preposition_of iff ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) ) proof thus ( g c= f & len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) ::_thesis: ( ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) implies f is_preposition_of ) proof assume that A1: g c= f and A2: len g > 0 ; ::_thesis: ( 1 <= len f & mid (f,1,(len g)) = g ) A3: 0 + 1 <= len g by A2, NAT_1:13; len g <= len f by A1, FINSEQ_1:63; hence 1 <= len f by A3, XXREAL_0:2; ::_thesis: mid (f,1,(len g)) = g thus mid (f,1,(len g)) = (f /^ (1 -' 1)) | (((len g) -' 1) + 1) by A3, FINSEQ_6:def_3 .= (f /^ (1 -' 1)) | (len g) by A3, XREAL_1:235 .= (f /^ 0) | (len g) by XREAL_1:232 .= f | (len g) by FINSEQ_5:28 .= g by A1, FINSEQ_3:113 ; ::_thesis: verum end; assume A4: ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) ; ::_thesis: f is_preposition_of percases ( len g <= 0 or ( len g > 0 & mid (f,1,(len g)) = g ) ) by A4; suppose len g <= 0 ; ::_thesis: f is_preposition_of then g = {} ; hence f is_preposition_of by XBOOLE_1:2; ::_thesis: verum end; supposethat A5: len g > 0 and A6: mid (f,1,(len g)) = g ; ::_thesis: f is_preposition_of 0 + 1 <= len g by A5, NAT_1:13; then g = f | (len g) by A6, FINSEQ_6:116; hence f is_preposition_of by RELAT_1:59; ::_thesis: verum end; end; end; end; :: deftheorem Def8 defines c= FINSEQ_8:def_8_:_ for D being non empty set for g, f being FinSequence of D holds ( g c= f iff ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) ); theorem :: FINSEQ_8:21 for D being non empty set for f, g being FinSequence of D st len g > 0 & f is_preposition_of holds g . 1 = f . 1 proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st len g > 0 & f is_preposition_of holds g . 1 = f . 1 let f, g be FinSequence of D; ::_thesis: ( len g > 0 & f is_preposition_of implies g . 1 = f . 1 ) assume that A1: len g > 0 and A2: f is_preposition_of ; ::_thesis: g . 1 = f . 1 A3: mid (f,1,(len g)) = g by A1, A2, Def8; A4: len g <= len f by A2, FINSEQ_1:63; 0 + 1 <= len g by A1, NAT_1:13; hence g . 1 = f . 1 by A3, A4, FINSEQ_6:123; ::_thesis: verum end; definition let D be non empty set ; let f, g be FinSequence of D; predg is_postposition_of f means :Def9: :: FINSEQ_8:def 9 Rev f is_preposition_of ; correctness ; end; :: deftheorem Def9 defines is_postposition_of FINSEQ_8:def_9_:_ for D being non empty set for f, g being FinSequence of D holds ( g is_postposition_of f iff Rev f is_preposition_of ); theorem Th22: :: FINSEQ_8:22 for D being non empty set for f, g being FinSequence of D st len g = 0 holds g is_postposition_of f proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st len g = 0 holds g is_postposition_of f let f, g be FinSequence of D; ::_thesis: ( len g = 0 implies g is_postposition_of f ) assume A1: len g = 0 ; ::_thesis: g is_postposition_of f len (Rev g) = len g by FINSEQ_5:def_3; then Rev f is_preposition_of by A1, Def8; hence g is_postposition_of f by Def9; ::_thesis: verum end; theorem Th23: :: FINSEQ_8:23 for D being non empty set for f, g being FinSequence of D st g is_postposition_of f holds len g <= len f proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st g is_postposition_of f holds len g <= len f let f, g be FinSequence of D; ::_thesis: ( g is_postposition_of f implies len g <= len f ) assume g is_postposition_of f ; ::_thesis: len g <= len f then A1: Rev f is_preposition_of by Def9; A2: len (Rev g) = len g by FINSEQ_5:def_3; len (Rev f) = len f by FINSEQ_5:def_3; hence len g <= len f by A1, A2, FINSEQ_1:63; ::_thesis: verum end; theorem :: FINSEQ_8:24 for D being non empty set for f, g being FinSequence of D st g is_postposition_of f & len g > 0 holds ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st g is_postposition_of f & len g > 0 holds ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) let f, g be FinSequence of D; ::_thesis: ( g is_postposition_of f & len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) assume A1: g is_postposition_of f ; ::_thesis: ( not len g > 0 or ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) then A2: Rev f is_preposition_of by Def9; then A3: ( len (Rev g) > 0 implies ( 1 <= len (Rev f) & mid ((Rev f),1,(len (Rev g))) = Rev g ) ) by Def8; A4: len (Rev g) = len g by FINSEQ_5:def_3; A5: len (Rev f) = len f by FINSEQ_5:def_3; now__::_thesis:_(_len_g_>_0_implies_(_len_g_<=_len_f_&_mid_(f,(((len_f)_+_1)_-'_(len_g)),(len_f))_=_g_)_) assume A6: len g > 0 ; ::_thesis: ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) then A7: 1 <= len f by A2, A4, A5, Def8; A8: mid ((Rev f),1,(len g)) = Rev g by A2, A4, A6, Def8; A9: (len f) - 1 >= 0 by A3, A5, A6, FINSEQ_5:def_3, XREAL_1:48; A10: len g <= len f by A1, Th23; A11: (len f) - (len g) >= 0 by A1, Th23, XREAL_1:48; len f < (len f) + 1 by XREAL_1:29; then len g < (len f) + 1 by A10, XXREAL_0:2; then A12: ((len f) + 1) - (len g) > 0 by XREAL_1:50; A13: 0 + 1 <= len g by A6, NAT_1:13; A14: g = Rev (Rev g) .= mid ((Rev (Rev f)),(((len f) -' (len g)) + 1),(((len f) -' 1) + 1)) by A5, A7, A8, A10, A13, FINSEQ_6:113 .= mid (f,(((len f) -' (len g)) + 1),(((len f) -' 1) + 1)) ; A15: ((len f) -' (len g)) + 1 = ((len f) - (len g)) + 1 by A11, XREAL_0:def_2 .= ((len f) + 1) -' (len g) by A12, XREAL_0:def_2 ; ((len f) -' 1) + 1 = ((len f) - 1) + 1 by A9, XREAL_0:def_2 .= len f ; hence ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) by A1, A14, A15, Th23; ::_thesis: verum end; hence ( not len g > 0 or ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) ; ::_thesis: verum end; theorem :: FINSEQ_8:25 for D being non empty set for f, g being FinSequence of D st ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) holds g is_postposition_of f proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) holds g is_postposition_of f let f, g be FinSequence of D; ::_thesis: ( ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) implies g is_postposition_of f ) assume A1: ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) ; ::_thesis: g is_postposition_of f A2: len (Rev f) = len f by FINSEQ_5:def_3; now__::_thesis:_(_(_len_g_>_0_&_g_is_postposition_of_f_)_or_(_len_g_<=_0_&_g_is_postposition_of_f_)_) percases ( len g > 0 or len g <= 0 ) ; caseA3: len g > 0 ; ::_thesis: g is_postposition_of f then A4: 0 + 1 <= len g by NAT_1:13; then A5: (len g) - 1 >= 0 by XREAL_1:48; len f < (len f) + 1 by XREAL_1:29; then len g < (len f) + 1 by A1, XXREAL_0:2; then A6: ((len f) + 1) - (len g) > 0 by XREAL_1:50; then ((len f) + 1) -' (len g) = ((len f) + 1) - (len g) by XREAL_0:def_2; then A7: 0 + 1 <= ((len f) + 1) -' (len g) by A6, NAT_1:13; A8: ((len f) + 1) -' (len g) = (len f) - ((len g) - 1) by A6, XREAL_0:def_2; (len f) + 0 <= (len f) + ((len g) - 1) by A5, XREAL_1:7; then A9: (len f) - ((len g) - 1) <= len f by XREAL_1:20; A10: 1 <= len f by A1, A4, XXREAL_0:2; A11: ((len f) -' (len f)) + 1 = ((len f) - (len f)) + 1 by XREAL_0:def_2 .= 1 ; len f < (len f) + 1 by XREAL_1:29; then len g <= (len f) + 1 by A1, XXREAL_0:2; then ((len f) + 1) - (len g) >= 0 by XREAL_1:48; then A12: (len f) - (((len f) + 1) -' (len g)) = (len f) - (((len f) + 1) - (len g)) by XREAL_0:def_2 .= (len g) - 1 ; then A13: ((len f) -' (((len f) + 1) -' (len g))) + 1 = ((len f) - (((len f) + 1) -' (len g))) + 1 by A5, XREAL_0:def_2; A14: Rev g = mid ((Rev f),(((len f) -' (len f)) + 1),(((len f) -' (((len f) + 1) -' (len g))) + 1)) by A1, A3, A7, A8, A9, A10, FINSEQ_6:113 .= mid ((Rev f),1,(len (Rev g))) by A11, A12, A13, FINSEQ_5:def_3 ; 1 <= len (Rev f) by A1, A2, A4, XXREAL_0:2; then Rev f is_preposition_of by A14, Def8; hence g is_postposition_of f by Def9; ::_thesis: verum end; case len g <= 0 ; ::_thesis: g is_postposition_of f then len g = 0 ; hence g is_postposition_of f by Th22; ::_thesis: verum end; end; end; hence g is_postposition_of f ; ::_thesis: verum end; theorem :: FINSEQ_8:26 for D being non empty set for f, g being FinSequence of D st 1 <= len f & f is_preposition_of holds g is_substring_of f,1 proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D st 1 <= len f & f is_preposition_of holds g is_substring_of f,1 let f, g be FinSequence of D; ::_thesis: ( 1 <= len f & f is_preposition_of implies g is_substring_of f,1 ) assume that A1: 1 <= len f and A2: f is_preposition_of ; ::_thesis: g is_substring_of f,1 now__::_thesis:_(_(_len_g_>_0_&_g_is_substring_of_f,1_)_or_(_len_g_<=_0_&_g_is_substring_of_f,1_)_) percases ( len g > 0 or len g <= 0 ) ; caseA3: len g > 0 ; ::_thesis: g is_substring_of f,1 mid (f,1,((1 -' 1) + (len g))) = mid (f,1,(0 + (len g))) by NAT_2:8 .= g by A2, A3, Def8 ; hence g is_substring_of f,1 by A1, Def7; ::_thesis: verum end; case len g <= 0 ; ::_thesis: g is_substring_of f,1 hence g is_substring_of f,1 by Def7; ::_thesis: verum end; end; end; hence g is_substring_of f,1 ; ::_thesis: verum end; theorem Th27: :: FINSEQ_8:27 for D being non empty set for f, g being FinSequence of D for n being Element of NAT st not g is_substring_of f,n holds for i being Element of NAT st n <= i & 0 < i holds mid (f,i,((i -' 1) + (len g))) <> g proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D for n being Element of NAT st not g is_substring_of f,n holds for i being Element of NAT st n <= i & 0 < i holds mid (f,i,((i -' 1) + (len g))) <> g let f, g be FinSequence of D; ::_thesis: for n being Element of NAT st not g is_substring_of f,n holds for i being Element of NAT st n <= i & 0 < i holds mid (f,i,((i -' 1) + (len g))) <> g let n be Element of NAT ; ::_thesis: ( not g is_substring_of f,n implies for i being Element of NAT st n <= i & 0 < i holds mid (f,i,((i -' 1) + (len g))) <> g ) assume A1: not g is_substring_of f,n ; ::_thesis: for i being Element of NAT st n <= i & 0 < i holds mid (f,i,((i -' 1) + (len g))) <> g now__::_thesis:_for_i_being_Element_of_NAT_st_n_<=_i_&_0_<_i_holds_ mid_(f,i,((i_-'_1)_+_(len_g)))_<>_g let i be Element of NAT ; ::_thesis: ( n <= i & 0 < i implies mid (f,i,((i -' 1) + (len g))) <> g ) assume that A2: n <= i and A3: 0 < i ; ::_thesis: mid (f,i,((i -' 1) + (len g))) <> g now__::_thesis:_(_(_i_<=_len_f_&_mid_(f,i,((i_-'_1)_+_(len_g)))_<>_g_)_or_(_i_>_len_f_&_mid_(f,i,((i_-'_1)_+_(len_g)))_<>_g_)_) percases ( i <= len f or i > len f ) ; case i <= len f ; ::_thesis: mid (f,i,((i -' 1) + (len g))) <> g hence mid (f,i,((i -' 1) + (len g))) <> g by A1, A2, Def7; ::_thesis: verum end; caseA4: i > len f ; ::_thesis: mid (f,i,((i -' 1) + (len g))) <> g now__::_thesis:_(_(_i_<=_(i_-'_1)_+_(len_g)_&_mid_(f,i,((i_-'_1)_+_(len_g)))_<>_g_)_or_(_i_>_(i_-'_1)_+_(len_g)_&_contradiction_)_) percases ( i <= (i -' 1) + (len g) or i > (i -' 1) + (len g) ) ; caseA5: i <= (i -' 1) + (len g) ; ::_thesis: mid (f,i,((i -' 1) + (len g))) <> g then A6: mid (f,i,((i -' 1) + (len g))) = (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by FINSEQ_6:def_3; A7: now__::_thesis:_(_(_i_-'_1_<=_len_f_&_len_(f_/^_(i_-'_1))_=_0_)_or_(_i_-'_1_>_len_f_&_len_(f_/^_(i_-'_1))_=_0_)_) percases ( i -' 1 <= len f or i -' 1 > len f ) ; caseA8: i -' 1 <= len f ; ::_thesis: len (f /^ (i -' 1)) = 0 i >= (len f) + 1 by A4, NAT_1:13; then A9: i - 1 >= ((len f) + 1) - 1 by XREAL_1:9; 0 + 1 <= i by A3, NAT_1:13; then 0 <= i - 1 by XREAL_1:48; then i -' 1 = i - 1 by XREAL_0:def_2; then A10: i -' 1 = len f by A8, A9, XXREAL_0:1; len (f /^ (i -' 1)) = (len f) - (i -' 1) by A8, RFINSEQ:def_1; hence len (f /^ (i -' 1)) = 0 by A10; ::_thesis: verum end; case i -' 1 > len f ; ::_thesis: len (f /^ (i -' 1)) = 0 then f /^ (i -' 1) = <*> D by RFINSEQ:def_1; hence len (f /^ (i -' 1)) = 0 ; ::_thesis: verum end; end; end; then f /^ (i -' 1) = <*> D ; then A11: (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) = <*> D by A7, FINSEQ_1:58; now__::_thesis:_not_mid_(f,i,((i_-'_1)_+_(len_g)))_=_g assume A12: mid (f,i,((i -' 1) + (len g))) = g ; ::_thesis: contradiction 0 + 1 <= i by A3, NAT_1:13; then A13: 0 <= i - 1 by XREAL_1:48; i < i + 1 by XREAL_1:29; then i - 1 < (i + 1) - 1 by XREAL_1:9; hence contradiction by A5, A6, A7, A11, A12, A13, XREAL_0:def_2; ::_thesis: verum end; hence mid (f,i,((i -' 1) + (len g))) <> g ; ::_thesis: verum end; caseA14: i > (i -' 1) + (len g) ; ::_thesis: contradiction now__::_thesis:_not_len_g_>_0 assume len g > 0 ; ::_thesis: contradiction then len g >= 0 + 1 by NAT_1:13; then A15: (i -' 1) + (len g) >= (i -' 1) + 1 by XREAL_1:7; 0 + 1 <= i by A3, NAT_1:13; then 0 <= i - 1 by XREAL_1:48; then i -' 1 = i - 1 by XREAL_0:def_2; hence contradiction by A14, A15; ::_thesis: verum end; hence contradiction by A1, Def7; ::_thesis: verum end; end; end; hence mid (f,i,((i -' 1) + (len g))) <> g ; ::_thesis: verum end; end; end; hence mid (f,i,((i -' 1) + (len g))) <> g ; ::_thesis: verum end; hence for i being Element of NAT st n <= i & 0 < i holds mid (f,i,((i -' 1) + (len g))) <> g ; ::_thesis: verum end; definition let D be non empty set ; let f, g be FinSequence of D; let n be Element of NAT ; func instr (n,f,g) -> Element of NAT means :Def10: :: FINSEQ_8:def 10 ( ( it <> 0 implies ( n <= it & f /^ (it -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= it ) ) ) & ( it = 0 implies not g is_substring_of f,n ) ); existence ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) proof A1: 1 -' 1 = 1 - 1 by XREAL_0:def_2; now__::_thesis:_(_(_g_is_substring_of_f,n_&_ex_b1_being_Element_of_NAT_st_ (_(_b1_<>_0_implies_(_n_<=_b1_&_f_/^_(b1_-'_1)_is_preposition_of_&_(_for_j_being_Element_of_NAT_st_j_>=_n_&_j_>_0_&_f_/^_(j_-'_1)_is_preposition_of_holds_ j_>=_b1_)_)_)_&_(_b1_=_0_implies_not_g_is_substring_of_f,n_)_)_)_or_(_not_g_is_substring_of_f,n_&_ex_b1_being_Element_of_NAT_st_ (_(_b1_<>_0_implies_(_n_<=_b1_&_f_/^_(b1_-'_1)_is_preposition_of_&_(_for_j_being_Element_of_NAT_st_j_>=_n_&_j_>_0_&_f_/^_(j_-'_1)_is_preposition_of_holds_ j_>=_b1_)_)_)_&_(_b1_=_0_implies_not_g_is_substring_of_f,n_)_)_)_) percases ( g is_substring_of f,n or not g is_substring_of f,n ) ; caseA2: g is_substring_of f,n ; ::_thesis: ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) now__::_thesis:_(_(_len_g_>_0_&_ex_b1_being_Element_of_NAT_st_ (_(_b1_<>_0_implies_(_n_<=_b1_&_f_/^_(b1_-'_1)_is_preposition_of_&_(_for_j_being_Element_of_NAT_st_j_>=_n_&_j_>_0_&_f_/^_(j_-'_1)_is_preposition_of_holds_ j_>=_b1_)_)_)_&_(_b1_=_0_implies_not_g_is_substring_of_f,n_)_)_)_or_(_len_g_<=_0_&_ex_b1_being_Element_of_NAT_st_ (_(_b1_<>_0_implies_(_n_<=_b1_&_f_/^_(b1_-'_1)_is_preposition_of_&_(_for_j_being_Element_of_NAT_st_j_>=_n_&_j_>_0_&_f_/^_(j_-'_1)_is_preposition_of_holds_ j_>=_b1_)_)_)_&_(_b1_=_0_implies_not_g_is_substring_of_f,n_)_)_)_) percases ( len g > 0 or len g <= 0 ) ; caseA3: len g > 0 ; ::_thesis: ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) then A4: ex i2 being Element of NAT st ( n <= i2 & i2 <= len f & mid (f,i2,((i2 -' 1) + (len g))) = g ) by A2, Def7; A5: 0 + 1 <= len g by A3, NAT_1:13; now__::_thesis:_(_(_n_>_0_&_ex_b1_being_Element_of_NAT_st_ (_(_b1_<>_0_implies_(_n_<=_b1_&_f_/^_(b1_-'_1)_is_preposition_of_&_(_for_j_being_Element_of_NAT_st_j_>=_n_&_j_>_0_&_f_/^_(j_-'_1)_is_preposition_of_holds_ j_>=_b1_)_)_)_&_(_b1_=_0_implies_not_g_is_substring_of_f,n_)_)_)_or_(_n_=_0_&_ex_b1_being_Element_of_NAT_st_ (_(_b1_<>_0_implies_(_n_<=_b1_&_f_/^_(b1_-'_1)_is_preposition_of_&_(_for_j_being_Element_of_NAT_st_j_>=_n_&_j_>_0_&_f_/^_(j_-'_1)_is_preposition_of_holds_ j_>=_b1_)_)_)_&_(_b1_=_0_implies_not_g_is_substring_of_f,n_)_)_)_) percases ( n > 0 or n = 0 ) ; caseA6: n > 0 ; ::_thesis: ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) defpred S1[ Nat] means ( n <= $1 & $1 <= len f & mid (f,$1,(($1 -' 1) + (len g))) = g ); A7: ex i being Nat st S1[i] by A4; ex k being Nat st ( S1[k] & ( for m being Nat st S1[m] holds m >= k ) ) from NAT_1:sch_5(A7); then consider k0 being Nat such that A8: n <= k0 and A9: k0 <= len f and A10: mid (f,k0,((k0 -' 1) + (len g))) = g and A11: for m being Nat st n <= m & m <= len f & mid (f,m,((m -' 1) + (len g))) = g holds m >= k0 ; reconsider k0 = k0 as Element of NAT by ORDINAL1:def_12; 0 + 1 <= k0 by A6, A8, NAT_1:13; then k0 - 1 >= 0 by XREAL_1:48; then A12: k0 -' 1 = k0 - 1 by XREAL_0:def_2; k0 < k0 + 1 by XREAL_1:29; then k0 - 1 < (k0 + 1) - 1 by XREAL_1:9; then k0 -' 1 < len f by A9, A12, XXREAL_0:2; then A13: len (f /^ (k0 -' 1)) = (len f) - (k0 -' 1) by RFINSEQ:def_1; (len f) - k0 >= 0 by A9, XREAL_1:48; then A14: ((len f) - k0) + 1 >= 0 + 1 by XREAL_1:7; A15: 1 -' 1 = 1 - 1 by XREAL_0:def_2; A16: 0 + 1 <= len g by A3, NAT_1:13; then A17: (k0 -' 1) + 1 <= (k0 -' 1) + (len g) by XREAL_1:7; A18: (len g) - 1 >= 0 by A16, XREAL_1:48; then (((- 1) + (len g)) + k0) - k0 >= 0 ; then A19: (((k0 -' 1) + (len g)) -' k0) + 1 = ((len g) - 1) + 1 by A12, XREAL_0:def_2 .= ((len g) -' 1) + 1 by A18, XREAL_0:def_2 ; mid ((f /^ (k0 -' 1)),1,(len g)) = ((f /^ (k0 -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def_3 .= (f /^ (k0 -' 1)) | ((((k0 -' 1) + (len g)) -' k0) + 1) by A15, A19, FINSEQ_5:28 .= mid (f,k0,((k0 -' 1) + (len g))) by A12, A17, FINSEQ_6:def_3 ; then A20: f /^ (k0 -' 1) is_preposition_of by A10, A12, A13, A14, Def8; for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k0 proof let j be Element of NAT ; ::_thesis: ( j >= n & j > 0 & f /^ (j -' 1) is_preposition_of implies j >= k0 ) assume that A21: j >= n and A22: j > 0 and A23: f /^ (j -' 1) is_preposition_of ; ::_thesis: j >= k0 A24: mid ((f /^ (j -' 1)),1,(len g)) = g by A3, A23, Def8; now__::_thesis:_(_(_j_<=_len_f_&_j_>=_k0_)_or_(_j_>_len_f_&_j_>=_k0_)_) percases ( j <= len f or j > len f ) ; caseA25: j <= len f ; ::_thesis: j >= k0 0 + 1 <= j by A22, NAT_1:13; then j - 1 >= 0 by XREAL_1:48; then A26: j -' 1 = j - 1 by XREAL_0:def_2; (((- 1) + (len g)) + j) - j >= 0 by A18; then A27: (((j -' 1) + (len g)) -' j) + 1 = ((len g) - 1) + 1 by A26, XREAL_0:def_2 .= ((len g) -' 1) + 1 by A18, XREAL_0:def_2 ; A28: (j -' 1) + 1 <= (j -' 1) + (len g) by A16, XREAL_1:7; mid ((f /^ (j -' 1)),1,(len g)) = ((f /^ (j -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def_3 .= (f /^ (j -' 1)) | ((((j -' 1) + (len g)) -' j) + 1) by A15, A27, FINSEQ_5:28 .= mid (f,j,((j -' 1) + (len g))) by A26, A28, FINSEQ_6:def_3 ; hence j >= k0 by A11, A21, A24, A25; ::_thesis: verum end; case j > len f ; ::_thesis: j >= k0 hence j >= k0 by A9, XXREAL_0:2; ::_thesis: verum end; end; end; hence j >= k0 ; ::_thesis: verum end; hence ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) by A6, A8, A20; ::_thesis: verum end; caseA29: n = 0 ; ::_thesis: ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) then A30: g is_substring_of f,1 by A2, Th20; reconsider n2 = 1 as Element of NAT ; A31: ex i2 being Element of NAT st ( n2 <= i2 & i2 <= len f & mid (f,i2,((i2 -' 1) + (len g))) = g ) by A3, A30, Def7; defpred S1[ Nat] means ( n2 <= $1 & $1 <= len f & mid (f,$1,(($1 -' 1) + (len g))) = g ); A32: ex i being Nat st S1[i] by A31; ex k being Nat st ( S1[k] & ( for m being Nat st S1[m] holds m >= k ) ) from NAT_1:sch_5(A32); then consider k0 being Nat such that A33: n2 <= k0 and A34: k0 <= len f and A35: mid (f,k0,((k0 -' 1) + (len g))) = g and A36: for m being Nat st n2 <= m & m <= len f & mid (f,m,((m -' 1) + (len g))) = g holds m >= k0 ; reconsider k0 = k0 as Element of NAT by ORDINAL1:def_12; k0 - 1 >= 0 by A33, XREAL_1:48; then A37: k0 -' 1 = k0 - 1 by XREAL_0:def_2; k0 < k0 + 1 by XREAL_1:29; then k0 - 1 < (k0 + 1) - 1 by XREAL_1:9; then k0 -' 1 < len f by A34, A37, XXREAL_0:2; then A38: len (f /^ (k0 -' 1)) = (len f) - (k0 -' 1) by RFINSEQ:def_1; (len f) - k0 >= 0 by A34, XREAL_1:48; then A39: ((len f) - k0) + 1 >= 0 + 1 by XREAL_1:7; A40: 0 + 1 <= len g by A3, NAT_1:13; then A41: (k0 -' 1) + 1 <= (k0 -' 1) + (len g) by XREAL_1:7; A42: (len g) - 1 >= 0 by A40, XREAL_1:48; then (((- 1) + (len g)) + k0) - k0 >= 0 ; then A43: (((k0 -' 1) + (len g)) -' k0) + 1 = ((len g) - 1) + 1 by A37, XREAL_0:def_2 .= ((len g) -' 1) + 1 by A42, XREAL_0:def_2 ; mid ((f /^ (k0 -' 1)),1,(len g)) = ((f /^ (k0 -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def_3 .= (f /^ (k0 -' 1)) | ((((k0 -' 1) + (len g)) -' k0) + 1) by A1, A43, FINSEQ_5:28 .= mid (f,k0,((k0 -' 1) + (len g))) by A37, A41, FINSEQ_6:def_3 ; then A44: f /^ (k0 -' 1) is_preposition_of by A35, A37, A38, A39, Def8; A45: for j being Element of NAT st j >= n2 & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k0 proof let j be Element of NAT ; ::_thesis: ( j >= n2 & j > 0 & f /^ (j -' 1) is_preposition_of implies j >= k0 ) assume that A46: j >= n2 and j > 0 and A47: f /^ (j -' 1) is_preposition_of ; ::_thesis: j >= k0 A48: mid ((f /^ (j -' 1)),1,(len g)) = g by A3, A47, Def8; now__::_thesis:_(_(_j_<=_len_f_&_j_>=_k0_)_or_(_j_>_len_f_&_j_>=_k0_)_) percases ( j <= len f or j > len f ) ; caseA49: j <= len f ; ::_thesis: j >= k0 j - 1 >= 0 by A46, XREAL_1:48; then A50: j -' 1 = j - 1 by XREAL_0:def_2; (((- 1) + (len g)) + j) - j >= 0 by A42; then A51: (((j -' 1) + (len g)) -' j) + 1 = ((len g) - 1) + 1 by A50, XREAL_0:def_2 .= ((len g) -' 1) + 1 by A42, XREAL_0:def_2 ; A52: (j -' 1) + 1 <= (j -' 1) + (len g) by A40, XREAL_1:7; mid ((f /^ (j -' 1)),1,(len g)) = ((f /^ (j -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def_3 .= (f /^ (j -' 1)) | ((((j -' 1) + (len g)) -' j) + 1) by A1, A51, FINSEQ_5:28 .= mid (f,j,((j -' 1) + (len g))) by A50, A52, FINSEQ_6:def_3 ; hence j >= k0 by A36, A46, A48, A49; ::_thesis: verum end; case j > len f ; ::_thesis: j >= k0 hence j >= k0 by A34, XXREAL_0:2; ::_thesis: verum end; end; end; hence j >= k0 ; ::_thesis: verum end; for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k0 proof let j be Element of NAT ; ::_thesis: ( j >= n & j > 0 & f /^ (j -' 1) is_preposition_of implies j >= k0 ) assume that j >= n and A53: j > 0 and A54: f /^ (j -' 1) is_preposition_of ; ::_thesis: j >= k0 j >= 0 + n2 by A53, NAT_1:13; hence j >= k0 by A45, A54; ::_thesis: verum end; hence ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) by A29, A33, A44; ::_thesis: verum end; end; end; hence ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) ; ::_thesis: verum end; caseA55: len g <= 0 ; ::_thesis: ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) reconsider nn = max (n,1) as Element of NAT ; A56: nn >= n by XXREAL_0:25; A57: nn >= 0 + 1 by XXREAL_0:25; A58: f /^ (nn -' 1) is_preposition_of by A55, Def8; for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= nn proof let j be Element of NAT ; ::_thesis: ( j >= n & j > 0 & f /^ (j -' 1) is_preposition_of implies j >= nn ) assume that A59: j >= n and A60: j > 0 and f /^ (j -' 1) is_preposition_of ; ::_thesis: j >= nn j >= 0 + 1 by A60, NAT_1:13; hence j >= nn by A59, XXREAL_0:28; ::_thesis: verum end; hence ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) by A56, A57, A58; ::_thesis: verum end; end; end; hence ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) ; ::_thesis: verum end; case not g is_substring_of f,n ; ::_thesis: ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) hence ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) ; ::_thesis: verum end; end; end; hence ex b1 being Element of NAT st ( ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ( b1 <> 0 implies ( n <= b1 & f /^ (b1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b1 ) ) ) & ( b1 = 0 implies not g is_substring_of f,n ) & ( b2 <> 0 implies ( n <= b2 & f /^ (b2 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b2 ) ) ) & ( b2 = 0 implies not g is_substring_of f,n ) holds b1 = b2 proof A61: 1 -' 1 = 1 - 1 by XREAL_0:def_2; thus for k1, k2 being Element of NAT st ( k1 <> 0 implies ( n <= k1 & f /^ (k1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k1 ) ) ) & ( k1 = 0 implies not g is_substring_of f,n ) & ( k2 <> 0 implies ( n <= k2 & f /^ (k2 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k2 ) ) ) & ( k2 = 0 implies not g is_substring_of f,n ) holds k1 = k2 ::_thesis: verum proof let k1, k2 be Element of NAT ; ::_thesis: ( ( k1 <> 0 implies ( n <= k1 & f /^ (k1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k1 ) ) ) & ( k1 = 0 implies not g is_substring_of f,n ) & ( k2 <> 0 implies ( n <= k2 & f /^ (k2 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k2 ) ) ) & ( k2 = 0 implies not g is_substring_of f,n ) implies k1 = k2 ) assume that A62: ( k1 <> 0 implies ( n <= k1 & f /^ (k1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k1 ) ) ) and A63: ( k1 = 0 implies not g is_substring_of f,n ) and A64: ( k2 <> 0 implies ( n <= k2 & f /^ (k2 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= k2 ) ) ) and A65: ( k2 = 0 implies not g is_substring_of f,n ) ; ::_thesis: k1 = k2 now__::_thesis:_(_(_len_g_>_0_&_k1_=_k2_)_or_(_len_g_<=_0_&_k1_=_k2_)_) percases ( len g > 0 or len g <= 0 ) ; case len g > 0 ; ::_thesis: k1 = k2 then A66: 0 + 1 <= len g by NAT_1:13; then A67: (len g) - 1 >= 0 by XREAL_1:48; now__::_thesis:_(_(_k1_<>_0_&_k2_<>_0_&_k1_=_k2_)_or_(_k1_<>_0_&_k2_=_0_&_contradiction_)_or_(_k1_=_0_&_k2_<>_0_&_contradiction_)_or_(_k1_=_0_&_k2_=_0_&_k1_=_k2_)_) percases ( ( k1 <> 0 & k2 <> 0 ) or ( k1 <> 0 & k2 = 0 ) or ( k1 = 0 & k2 <> 0 ) or ( k1 = 0 & k2 = 0 ) ) ; caseA68: ( k1 <> 0 & k2 <> 0 ) ; ::_thesis: k1 = k2 then A69: k2 >= k1 by A62, A64; k1 >= k2 by A62, A64, A68; hence k1 = k2 by A69, XXREAL_0:1; ::_thesis: verum end; caseA70: ( k1 <> 0 & k2 = 0 ) ; ::_thesis: contradiction then A71: len g > 0 by A65, Def7; for i being Element of NAT st n <= i & 0 < i holds not f /^ (i -' 1) is_preposition_of proof let i be Element of NAT ; ::_thesis: ( n <= i & 0 < i implies not f /^ (i -' 1) is_preposition_of ) assume that A72: n <= i and A73: 0 < i ; ::_thesis: not f /^ (i -' 1) is_preposition_of 0 + 1 <= i by A73, NAT_1:13; then i - 1 >= 0 by XREAL_1:48; then A74: i -' 1 = i - 1 by XREAL_0:def_2; (((- 1) + (len g)) + i) - i >= 0 by A67; then A75: (((i -' 1) + (len g)) -' i) + 1 = ((len g) - 1) + 1 by A74, XREAL_0:def_2 .= ((len g) -' 1) + 1 by A67, XREAL_0:def_2 ; A76: (i -' 1) + 1 <= (i -' 1) + (len g) by A66, XREAL_1:7; mid ((f /^ (i -' 1)),1,(len g)) = ((f /^ (i -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A66, FINSEQ_6:def_3 .= (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by A61, A75, FINSEQ_5:28 .= mid (f,i,((i -' 1) + (len g))) by A74, A76, FINSEQ_6:def_3 ; then ( not 1 <= len (f /^ (i -' 1)) or not mid ((f /^ (i -' 1)),1,(len g)) = g ) by A65, A70, A72, A73, Th27; hence not f /^ (i -' 1) is_preposition_of by A71, Def8; ::_thesis: verum end; hence contradiction by A62, A70; ::_thesis: verum end; caseA77: ( k1 = 0 & k2 <> 0 ) ; ::_thesis: contradiction then A78: len g > 0 by A63, Def7; for i being Element of NAT st n <= i & 0 < i holds not f /^ (i -' 1) is_preposition_of proof let i be Element of NAT ; ::_thesis: ( n <= i & 0 < i implies not f /^ (i -' 1) is_preposition_of ) assume that A79: n <= i and A80: 0 < i ; ::_thesis: not f /^ (i -' 1) is_preposition_of 0 + 1 <= i by A80, NAT_1:13; then i - 1 >= 0 by XREAL_1:48; then A81: i -' 1 = i - 1 by XREAL_0:def_2; (((- 1) + (len g)) + i) - i >= 0 by A67; then A82: (((i -' 1) + (len g)) -' i) + 1 = ((len g) - 1) + 1 by A81, XREAL_0:def_2 .= ((len g) -' 1) + 1 by A67, XREAL_0:def_2 ; A83: (i -' 1) + 1 <= (i -' 1) + (len g) by A66, XREAL_1:7; mid ((f /^ (i -' 1)),1,(len g)) = ((f /^ (i -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A66, FINSEQ_6:def_3 .= (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by A61, A82, FINSEQ_5:28 .= mid (f,i,((i -' 1) + (len g))) by A81, A83, FINSEQ_6:def_3 ; then ( not 1 <= len (f /^ (i -' 1)) or not mid ((f /^ (i -' 1)),1,(len g)) = g ) by A63, A77, A79, A80, Th27; hence not f /^ (i -' 1) is_preposition_of by A78, Def8; ::_thesis: verum end; hence contradiction by A64, A77; ::_thesis: verum end; case ( k1 = 0 & k2 = 0 ) ; ::_thesis: k1 = k2 hence k1 = k2 ; ::_thesis: verum end; end; end; hence k1 = k2 ; ::_thesis: verum end; caseA84: len g <= 0 ; ::_thesis: k1 = k2 now__::_thesis:_(_(_k1_<>_0_&_k2_<>_0_&_k1_=_k2_)_or_(_k1_<>_0_&_k2_=_0_&_contradiction_)_or_(_k1_=_0_&_k2_<>_0_&_contradiction_)_or_(_k1_=_0_&_k2_=_0_&_contradiction_)_) percases ( ( k1 <> 0 & k2 <> 0 ) or ( k1 <> 0 & k2 = 0 ) or ( k1 = 0 & k2 <> 0 ) or ( k1 = 0 & k2 = 0 ) ) ; caseA85: ( k1 <> 0 & k2 <> 0 ) ; ::_thesis: k1 = k2 then A86: k2 >= k1 by A62, A64; k1 >= k2 by A62, A64, A85; hence k1 = k2 by A86, XXREAL_0:1; ::_thesis: verum end; case ( k1 <> 0 & k2 = 0 ) ; ::_thesis: contradiction hence contradiction by A65, A84, Def7; ::_thesis: verum end; case ( k1 = 0 & k2 <> 0 ) ; ::_thesis: contradiction hence contradiction by A63, A84, Def7; ::_thesis: verum end; case ( k1 = 0 & k2 = 0 ) ; ::_thesis: contradiction hence contradiction by A63, A84, Def7; ::_thesis: verum end; end; end; hence k1 = k2 ; ::_thesis: verum end; end; end; hence k1 = k2 ; ::_thesis: verum end; end; end; :: deftheorem Def10 defines instr FINSEQ_8:def_10_:_ for D being non empty set for f, g being FinSequence of D for n, b5 being Element of NAT holds ( b5 = instr (n,f,g) iff ( ( b5 <> 0 implies ( n <= b5 & f /^ (b5 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= b5 ) ) ) & ( b5 = 0 implies not g is_substring_of f,n ) ) ); definition let D be non empty set ; let f, CR be FinSequence of D; func addcr (f,CR) -> FinSequence of D equals :: FINSEQ_8:def 11 ovlcon (f,CR); correctness coherence ovlcon (f,CR) is FinSequence of D; ; end; :: deftheorem defines addcr FINSEQ_8:def_11_:_ for D being non empty set for f, CR being FinSequence of D holds addcr (f,CR) = ovlcon (f,CR); definition let D be non empty set ; let r, CR be FinSequence of D; predr is_terminated_by CR means :Def12: :: FINSEQ_8:def 12 ( len CR > 0 implies ( len r >= len CR & instr (1,r,CR) = ((len r) + 1) -' (len CR) ) ); correctness ; end; :: deftheorem Def12 defines is_terminated_by FINSEQ_8:def_12_:_ for D being non empty set for r, CR being FinSequence of D holds ( r is_terminated_by CR iff ( len CR > 0 implies ( len r >= len CR & instr (1,r,CR) = ((len r) + 1) -' (len CR) ) ) ); theorem :: FINSEQ_8:28 for D being non empty set for f being FinSequence of D holds f is_terminated_by f proof let D be non empty set ; ::_thesis: for f being FinSequence of D holds f is_terminated_by f let f be FinSequence of D; ::_thesis: f is_terminated_by f A1: ((len f) + 1) -' (len f) = ((len f) + 1) - (len f) by XREAL_0:def_2; 1 -' 1 = (0 + 1) -' 1 .= 0 by NAT_D:34 ; then A2: f /^ (1 -' 1) = f by FINSEQ_5:28; for j being Element of NAT st j >= 1 & j > 0 & f /^ (j -' 1) is_preposition_of holds j >= 1 ; then instr (1,f,f) = ((len f) + 1) -' (len f) by A1, A2, Def10; hence f is_terminated_by f by Def12; ::_thesis: verum end;