:: FILEREC1 semantic presentation begin theorem Th1: :: FILEREC1:1 for D being non empty set for p, q, r, s being FinSequence of D holds ( ((p ^ q) ^ r) ^ s = (p ^ (q ^ r)) ^ s & ((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) & (p ^ (q ^ r)) ^ s = (p ^ q) ^ (r ^ s) ) proof let D be non empty set ; ::_thesis: for p, q, r, s being FinSequence of D holds ( ((p ^ q) ^ r) ^ s = (p ^ (q ^ r)) ^ s & ((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) & (p ^ (q ^ r)) ^ s = (p ^ q) ^ (r ^ s) ) let p, q, r, s be FinSequence of D; ::_thesis: ( ((p ^ q) ^ r) ^ s = (p ^ (q ^ r)) ^ s & ((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) & (p ^ (q ^ r)) ^ s = (p ^ q) ^ (r ^ s) ) ((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) by FINSEQ_1:32; hence ( ((p ^ q) ^ r) ^ s = (p ^ (q ^ r)) ^ s & ((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) & (p ^ (q ^ r)) ^ s = (p ^ q) ^ (r ^ s) ) by FINSEQ_1:32; ::_thesis: verum end; theorem Th2: :: FILEREC1:2 for D being set for f being FinSequence of D holds f | (len f) = f proof let D be set ; ::_thesis: for f being FinSequence of D holds f | (len f) = f let f be FinSequence of D; ::_thesis: f | (len f) = f f | (len f) = f | (Seg (len f)) by FINSEQ_1:def_15; hence f | (len f) = f by FINSEQ_2:20; ::_thesis: verum end; theorem Th3: :: FILEREC1:3 for D being non empty set for p, q being FinSequence of D st len p = 0 holds q = p ^ q proof let D be non empty set ; ::_thesis: for p, q being FinSequence of D st len p = 0 holds q = p ^ q let p, q be FinSequence of D; ::_thesis: ( len p = 0 implies q = p ^ q ) assume len p = 0 ; ::_thesis: q = p ^ q then p = <*> D .= {} ; hence q = p ^ q by FINSEQ_1:34; ::_thesis: verum end; theorem Th4: :: FILEREC1:4 for D being non empty set for f being FinSequence of D for n, m being Element of NAT st n <= m holds len (f /^ m) <= len (f /^ n) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for n, m being Element of NAT st n <= m holds len (f /^ m) <= len (f /^ n) let f be FinSequence of D; ::_thesis: for n, m being Element of NAT st n <= m holds len (f /^ m) <= len (f /^ n) let n, m be Element of NAT ; ::_thesis: ( n <= m implies len (f /^ m) <= len (f /^ n) ) A1: len (f /^ m) = (len f) -' m by RFINSEQ:29; assume A2: n <= m ; ::_thesis: len (f /^ m) <= len (f /^ n) then A3: n - n <= m - n by XREAL_1:9; now__::_thesis:_(len_(f_/^_n))_-_(len_(f_/^_m))_>=_0 percases ( len f <= n or len f > n ) ; supposeA4: len f <= n ; ::_thesis: (len (f /^ n)) - (len (f /^ m)) >= 0 then ((len f) -' n) - ((len f) -' m) = ((len f) -' n) - 0 by A2, NAT_2:8, XXREAL_0:2 .= 0 by A4, NAT_2:8 ; hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A1, RFINSEQ:29; ::_thesis: verum end; supposeA5: len f > n ; ::_thesis: (len (f /^ n)) - (len (f /^ m)) >= 0 percases ( len f <= m or len f > m ) ; suppose len f <= m ; ::_thesis: (len (f /^ n)) - (len (f /^ m)) >= 0 then ((len f) -' n) - ((len f) -' m) = ((len f) -' n) - 0 by NAT_2:8 .= (len f) -' n ; hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A1, RFINSEQ:29; ::_thesis: verum end; suppose len f > m ; ::_thesis: (len (f /^ n)) - (len (f /^ m)) >= 0 then ((len f) -' n) - ((len f) -' m) = ((len f) -' n) - ((len f) - m) by XREAL_1:233 .= ((len f) - n) - ((len f) - m) by A5, XREAL_1:233 .= m - n ; hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A3, A1, RFINSEQ:29; ::_thesis: verum end; end; end; end; end; then ((len (f /^ n)) - (len (f /^ m))) + (len (f /^ m)) >= 0 + (len (f /^ m)) by XREAL_1:6; hence len (f /^ m) <= len (f /^ n) ; ::_thesis: verum end; theorem Th5: :: FILEREC1:5 for D being non empty set for f, g being FinSequence of D st len g >= 1 holds mid ((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 st len g >= 1 holds mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g let f, g be FinSequence of D; ::_thesis: ( len g >= 1 implies mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g ) assume A1: len g >= 1 ; ::_thesis: mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g A2: g | (len g) = g | (Seg (len g)) by FINSEQ_1:def_15; percases ( (len f) + 1 <= (len f) + (len g) or (len f) + 1 > (len f) + (len g) ) ; supposeA3: (len f) + 1 <= (len f) + (len g) ; ::_thesis: mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g then A4: len f < (len f) + (len g) by NAT_1:13; then (len f) - (len f) < ((len f) + (len g)) - (len f) by XREAL_1:14; then A5: ((len f) + (len g)) -' (len f) = len g by XREAL_0:def_2; mid ((f ^ g),((len f) + 1),((len f) + (len g))) = ((f ^ g) /^ (((len f) + 1) -' 1)) | ((((len f) + (len g)) -' ((len f) + 1)) + 1) by A3, FINSEQ_6:def_3 .= ((f ^ g) /^ (len f)) | ((((len f) + (len g)) -' ((len f) + 1)) + 1) by NAT_D:34 .= ((f ^ g) /^ (len f)) | (((len f) + (len g)) -' (len f)) by A4, NAT_2:7 .= g | (len g) by A5, FINSEQ_5:37 ; hence mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g by A2, FINSEQ_2:20; ::_thesis: verum end; suppose (len f) + 1 > (len f) + (len g) ; ::_thesis: mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g then ((len f) + 1) - (len f) > ((len f) + (len g)) - (len f) by XREAL_1:14; hence mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g by A1; ::_thesis: verum end; end; end; theorem Th6: :: FILEREC1:6 for D being non empty set for f, g being FinSequence of D for i, j being Element of NAT st 1 <= i & i <= j & j <= len f holds mid ((f ^ g),i,j) = mid (f,i,j) proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D for i, j being Element of NAT st 1 <= i & i <= j & j <= len f holds mid ((f ^ g),i,j) = mid (f,i,j) let f, g be FinSequence of D; ::_thesis: for i, j being Element of NAT st 1 <= i & i <= j & j <= len f holds mid ((f ^ g),i,j) = mid (f,i,j) let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i <= j & j <= len f implies mid ((f ^ g),i,j) = mid (f,i,j) ) assume that A1: 1 <= i and A2: i <= j and A3: j <= len f ; ::_thesis: mid ((f ^ g),i,j) = mid (f,i,j) A4: ((len (f /^ (i -' 1))) + (i - 1)) - (i - 1) = len (f /^ (i -' 1)) ; len f >= i by A2, A3, XXREAL_0:2; then (len f) - 0 >= i - 1 by XREAL_1:13; then A5: len f >= i -' 1 by A1, XREAL_1:233; (len (f /^ (i -' 1))) + (i -' 1) = ((len f) -' (i -' 1)) + (i -' 1) by RFINSEQ:29 .= len f by A5, XREAL_1:235 ; then A6: len (f /^ (i -' 1)) = (len f) - (i - 1) by A1, A4, XREAL_1:233 .= ((len f) - i) + 1 ; (len f) - i >= j - i by A3, XREAL_1:9; then A7: ((len f) - i) + 1 >= (j - i) + 1 by XREAL_1:6; j - i >= i - i by A2, XREAL_1:9; then A8: len (f /^ (i -' 1)) >= (j -' i) + 1 by A7, A6, XREAL_0:def_2; A9: ( i -' 1 <= i & i <= len f ) by A2, A3, NAT_D:35, XXREAL_0:2; mid ((f ^ g),i,j) = ((f ^ g) /^ (i -' 1)) | ((j -' i) + 1) by A2, FINSEQ_6:def_3 .= ((f /^ (i -' 1)) ^ g) | ((j -' i) + 1) by A9, GENEALG1:1, XXREAL_0:2 .= (f /^ (i -' 1)) | ((j -' i) + 1) by A8, FINSEQ_5:22 ; hence mid ((f ^ g),i,j) = mid (f,i,j) by A2, FINSEQ_6:def_3; ::_thesis: verum end; theorem :: FILEREC1:7 for D being non empty set for f being FinSequence of D for i, j, n being Element of NAT st 1 <= i & i <= j & i <= len (f | n) & j <= len (f | n) holds mid (f,i,j) = mid ((f | n),i,j) proof let D be non empty set ; ::_thesis: for f being FinSequence of D for i, j, n being Element of NAT st 1 <= i & i <= j & i <= len (f | n) & j <= len (f | n) holds mid (f,i,j) = mid ((f | n),i,j) let f be FinSequence of D; ::_thesis: for i, j, n being Element of NAT st 1 <= i & i <= j & i <= len (f | n) & j <= len (f | n) holds mid (f,i,j) = mid ((f | n),i,j) let i, j, n be Element of NAT ; ::_thesis: ( 1 <= i & i <= j & i <= len (f | n) & j <= len (f | n) implies mid (f,i,j) = mid ((f | n),i,j) ) assume that A1: 1 <= i and A2: i <= j and A3: i <= len (f | n) and A4: j <= len (f | n) ; ::_thesis: mid (f,i,j) = mid ((f | n),i,j) A5: (j -' i) + 1 = (j - i) + 1 by A2, XREAL_1:233; A6: len (f | n) <= n by FINSEQ_5:17; then n >= i by A3, XXREAL_0:2; then A7: n - 0 >= i - 1 by XREAL_1:13; j <= n by A4, A6, XXREAL_0:2; then j - i <= n - i by XREAL_1:9; then A8: (j - i) + 1 <= (n - i) + 1 by XREAL_1:6; i -' 1 = i - 1 by A1, XREAL_1:233; then A9: n -' (i -' 1) = n - (i - 1) by A7, XREAL_1:233 .= (n - i) + 1 ; mid ((f | n),i,j) = ((f | n) /^ (i -' 1)) | ((j -' i) + 1) by A2, FINSEQ_6:def_3 .= ((f /^ (i -' 1)) | (n -' (i -' 1))) | ((j -' i) + 1) by FINSEQ_5:80 .= (f /^ (i -' 1)) | ((j -' i) + 1) by A9, A5, A8, FINSEQ_5:77 ; hence mid (f,i,j) = mid ((f | n),i,j) by A2, FINSEQ_6:def_3; ::_thesis: verum end; theorem :: FILEREC1:8 for a being set for D being non empty set for f being FinSequence of D st f = <*a*> holds a in D proof let a be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a*> holds a in D let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a*> holds a in D let f be FinSequence of D; ::_thesis: ( f = <*a*> implies a in D ) A1: f is Function of (dom f),D by FINSEQ_2:26; assume A2: f = <*a*> ; ::_thesis: a in D then 1 <= len f by FINSEQ_1:40; then A3: 1 in dom f by FINSEQ_3:25; f . 1 = a by A2, FINSEQ_1:40; hence a in D by A3, A1, FUNCT_2:5; ::_thesis: verum end; theorem :: FILEREC1:9 for a, b being set for D being non empty set for f being FinSequence of D st f = <*a,b*> holds ( a in D & b in D ) proof let a, b be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a,b*> holds ( a in D & b in D ) let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a,b*> holds ( a in D & b in D ) let f be FinSequence of D; ::_thesis: ( f = <*a,b*> implies ( a in D & b in D ) ) A1: f is Function of (dom f),D by FINSEQ_2:26; assume A2: f = <*a,b*> ; ::_thesis: ( a in D & b in D ) then A3: ( 1 in dom f & 2 in dom f ) by CALCUL_1:14; ( f . 1 = a & f . 2 = b ) by A2, FINSEQ_1:44; hence ( a in D & b in D ) by A3, A1, FUNCT_2:5; ::_thesis: verum end; theorem Th10: :: FILEREC1:10 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds ( a in D & b in D & c in D ) proof let a, b, c be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds ( a in D & b in D & c in D ) let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a,b,c*> holds ( a in D & b in D & c in D ) let f be FinSequence of D; ::_thesis: ( f = <*a,b,c*> implies ( a in D & b in D & c in D ) ) A1: f is Function of (dom f),D by FINSEQ_2:26; assume A2: f = <*a,b,c*> ; ::_thesis: ( a in D & b in D & c in D ) then A3: ( f . 3 = c & 1 in dom f ) by FINSEQ_1:45, TOPREAL3:1; A4: ( 2 in dom f & 3 in dom f ) by A2, TOPREAL3:1; ( f . 1 = a & f . 2 = b ) by A2, FINSEQ_1:45; hence ( a in D & b in D & c in D ) by A3, A4, A1, FUNCT_2:5; ::_thesis: verum end; theorem :: FILEREC1:11 for a being set for D being non empty set for f being FinSequence of D st f = <*a*> holds f | 1 = <*a*> proof let a be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a*> holds f | 1 = <*a*> let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a*> holds f | 1 = <*a*> let f be FinSequence of D; ::_thesis: ( f = <*a*> implies f | 1 = <*a*> ) assume A1: f = <*a*> ; ::_thesis: f | 1 = <*a*> then len f <= 1 by FINSEQ_1:40; hence f | 1 = <*a*> by A1, FINSEQ_1:58; ::_thesis: verum end; theorem :: FILEREC1:12 for a, b being set for D being non empty set for f being FinSequence of D st f = <*a,b*> holds f /^ 1 = <*b*> proof let a, b be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a,b*> holds f /^ 1 = <*b*> let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a,b*> holds f /^ 1 = <*b*> let f be FinSequence of D; ::_thesis: ( f = <*a,b*> implies f /^ 1 = <*b*> ) A1: f is Function of (dom f),D by FINSEQ_2:26; assume A2: f = <*a,b*> ; ::_thesis: f /^ 1 = <*b*> then A3: ( 1 in dom f & 2 in dom f ) by CALCUL_1:14; ( f . 1 = a & f . 2 = b ) by A2, FINSEQ_1:44; then reconsider a2 = a, b2 = b as Element of D by A3, A1, FUNCT_2:5; f /^ 1 = <*a2,b2*> /^ 1 by A2 .= <*b2*> by FINSEQ_6:46 ; hence f /^ 1 = <*b*> ; ::_thesis: verum end; theorem :: FILEREC1:13 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f | 1 = <*a*> proof let a, b, c be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f | 1 = <*a*> let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a,b,c*> holds f | 1 = <*a*> let f be FinSequence of D; ::_thesis: ( f = <*a,b,c*> implies f | 1 = <*a*> ) assume A1: f = <*a,b,c*> ; ::_thesis: f | 1 = <*a*> f | 1 = f | (Seg 1) by FINSEQ_1:def_15 .= <*a*> by A1, FINSEQ_6:4 ; hence f | 1 = <*a*> ; ::_thesis: verum end; theorem Th14: :: FILEREC1:14 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f | 2 = <*a,b*> proof let a, b, c be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f | 2 = <*a,b*> let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a,b,c*> holds f | 2 = <*a,b*> let f be FinSequence of D; ::_thesis: ( f = <*a,b,c*> implies f | 2 = <*a,b*> ) assume A1: f = <*a,b,c*> ; ::_thesis: f | 2 = <*a,b*> f | 2 = f | (Seg 2) by FINSEQ_1:def_15 .= <*a,b*> by A1, FINSEQ_6:5 ; hence f | 2 = <*a,b*> ; ::_thesis: verum end; theorem :: FILEREC1:15 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f /^ 1 = <*b,c*> proof let a, b, c be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f /^ 1 = <*b,c*> let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a,b,c*> holds f /^ 1 = <*b,c*> let f be FinSequence of D; ::_thesis: ( f = <*a,b,c*> implies f /^ 1 = <*b,c*> ) assume A1: f = <*a,b,c*> ; ::_thesis: f /^ 1 = <*b,c*> then reconsider a2 = a, b2 = b, c2 = c as Element of D by Th10; A2: f . 3 = c2 by A1, FINSEQ_1:45; ( f . 1 = a2 & f . 2 = b2 ) by A1, FINSEQ_1:45; hence f /^ 1 = <*b,c*> by A1, A2, FINSEQ_6:47; ::_thesis: verum end; theorem :: FILEREC1:16 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f /^ 2 = <*c*> proof let a, b, c be set ; ::_thesis: for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f /^ 2 = <*c*> let D be non empty set ; ::_thesis: for f being FinSequence of D st f = <*a,b,c*> holds f /^ 2 = <*c*> let f be FinSequence of D; ::_thesis: ( f = <*a,b,c*> implies f /^ 2 = <*c*> ) assume A1: f = <*a,b,c*> ; ::_thesis: f /^ 2 = <*c*> then reconsider a2 = a, b2 = b, c2 = c as Element of D by Th10; f /^ 2 = (<*a2*> ^ <*b2,c2*>) /^ (1 + 1) by A1, FINSEQ_1:43 .= (<*a2*> ^ <*b2,c2*>) /^ ((len <*a2*>) + 1) by FINSEQ_1:40 .= <*b2,c2*> /^ 1 by FINSEQ_5:36 .= <*c2*> by FINSEQ_6:46 ; hence f /^ 2 = <*c*> ; ::_thesis: verum end; theorem :: FILEREC1:17 for D being non empty set for f being FinSequence of D st len f = 0 holds Rev f = f proof let D be non empty set ; ::_thesis: for f being FinSequence of D st len f = 0 holds Rev f = f let f be FinSequence of D; ::_thesis: ( len f = 0 implies Rev f = f ) assume len f = 0 ; ::_thesis: Rev f = f then f = <*> D .= {} ; hence Rev f = f ; ::_thesis: verum end; theorem Th18: :: FILEREC1:18 for D being non empty set for r being FinSequence of D for i being Element of NAT st i <= len r holds Rev (r /^ i) = (Rev r) | ((len r) -' i) proof let D be non empty set ; ::_thesis: for r being FinSequence of D for i being Element of NAT st i <= len r holds Rev (r /^ i) = (Rev r) | ((len r) -' i) let r be FinSequence of D; ::_thesis: for i being Element of NAT st i <= len r holds Rev (r /^ i) = (Rev r) | ((len r) -' i) let i be Element of NAT ; ::_thesis: ( i <= len r implies Rev (r /^ i) = (Rev r) | ((len r) -' i) ) set s = Rev r; (len r) -' i <= len r by NAT_D:50; then (len r) -' i <= len (Rev r) by FINSEQ_5:def_3; then A1: (len (Rev r)) -' i <= len (Rev r) by FINSEQ_5:def_3; A2: len ((Rev r) | ((len r) -' i)) = len ((Rev r) | ((len (Rev r)) -' i)) by FINSEQ_5:def_3 .= (len (Rev r)) -' i by A1, FINSEQ_1:59 ; assume A3: i <= len r ; ::_thesis: Rev (r /^ i) = (Rev r) | ((len r) -' i) then (len r) - i >= 0 by XREAL_1:48; then A4: (len r) - i = (len r) -' i by XREAL_0:def_2; A5: for k being Nat st 1 <= k & k <= len (Rev (r /^ i)) holds (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len (Rev (r /^ i)) implies (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k ) assume that A6: 1 <= k and A7: k <= len (Rev (r /^ i)) ; ::_thesis: (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k k in dom (Rev (r /^ i)) by A6, A7, FINSEQ_3:25; then A8: (Rev (r /^ i)) . k = (r /^ i) . (((len (r /^ i)) - k) + 1) by FINSEQ_5:def_3 .= (r /^ i) . ((((len r) - i) - k) + 1) by A3, RFINSEQ:def_1 ; 0 <= i by NAT_1:2; then (len r) + 0 <= (len r) + i by XREAL_1:7; then (len r) - i <= ((len r) + i) - i by XREAL_1:9; then len (r /^ i) <= len r by A3, RFINSEQ:def_1; then len (Rev (r /^ i)) <= len r by FINSEQ_5:def_3; then A9: k <= len r by A7, XXREAL_0:2; then A10: (len r) - k >= 0 by XREAL_1:48; then A11: (len r) - k = (len r) -' k by XREAL_0:def_2; k - 1 >= 0 by A6, XREAL_1:48; then (len r) + 0 <= (len r) + (k - 1) by XREAL_1:7; then (len r) - (k - 1) <= ((len r) + (k - 1)) - (k - 1) by XREAL_1:9; then ((len r) - k) + 1 <= len r ; then A12: ((len r) -' k) + 1 <= len r by A10, XREAL_0:def_2; ((len r) -' k) + 1 > 0 ; then ((len r) - k) + 1 >= 0 + 1 by A11, NAT_1:13; then A13: ((len r) - k) + 1 in dom r by A11, A12, FINSEQ_3:25; A14: r = r /^ 0 by FINSEQ_5:28; k in dom r by A6, A9, FINSEQ_3:25; then A15: k in dom (Rev r) by FINSEQ_5:57; k <= len (r /^ i) by A7, FINSEQ_5:def_3; then A16: k <= (len r) - i by A3, RFINSEQ:def_1; then A17: ((len r) -' i) - k >= 0 by A4, XREAL_1:48; then A18: ((len r) -' i) -' k = ((len r) -' i) - k by XREAL_0:def_2; k <= (len r) -' i by A16, XREAL_0:def_2; then A19: ((Rev r) | ((len r) -' i)) . k = (Rev r) . k by FINSEQ_3:112 .= r . (((len r) - k) + 1) by A15, FINSEQ_5:def_3 ; A20: i + ((((len r) -' i) -' k) + 1) = i + ((((len r) - i) - k) + 1) by A4, A17, XREAL_0:def_2 .= ((((len r) - i) + i) - k) + 1 ; k - 1 >= 0 by A6, XREAL_1:48; then ((len r) - i) + 0 <= ((len r) - i) + (k - 1) by XREAL_1:7; then ((len r) - i) - (k - 1) <= (((len r) - i) + (k - 1)) - (k - 1) by XREAL_1:9; then ( (((len r) -' i) -' k) + 1 >= 0 + 1 & (((len r) -' i) -' k) + 1 <= len (r /^ i) ) by A3, A4, A18, RFINSEQ:def_1, XREAL_1:7; then (((len r) - i) - k) + 1 in Seg (len (r /^ i)) by A4, A18, FINSEQ_1:1; then A21: (((len r) - i) - k) + 1 in dom (r /^ i) by FINSEQ_1:def_3; then (r /^ i) . ((((len r) - i) - k) + 1) = (r /^ i) /. ((((len r) -' i) -' k) + 1) by A4, A18, PARTFUN1:def_6 .= (r /^ 0) /. (i + ((((len r) -' i) -' k) + 1)) by A4, A18, A21, A14, FINSEQ_5:27 .= r . (((len r) - k) + 1) by A20, A13, A14, PARTFUN1:def_6 ; hence (Rev (r /^ i)) . k = ((Rev r) | ((len r) -' i)) . k by A8, A19; ::_thesis: verum end; len (Rev (r /^ i)) = len (r /^ i) by FINSEQ_5:def_3 .= (len r) -' i by RFINSEQ:29 .= len ((Rev r) | ((len r) -' i)) by A2, FINSEQ_5:def_3 ; hence Rev (r /^ i) = (Rev r) | ((len r) -' i) by A5, FINSEQ_1:14; ::_thesis: verum end; theorem Th19: :: FILEREC1:19 for D being non empty set for f, CR being FinSequence of D st not CR is_substring_of f,1 & CR separates_uniquely holds instr (1,(f ^ CR),CR) = (len f) + 1 proof let D be non empty set ; ::_thesis: for f, CR being FinSequence of D st not CR is_substring_of f,1 & CR separates_uniquely holds instr (1,(f ^ CR),CR) = (len f) + 1 let f, CR be FinSequence of D; ::_thesis: ( not CR is_substring_of f,1 & CR separates_uniquely implies instr (1,(f ^ CR),CR) = (len f) + 1 ) assume that A1: not CR is_substring_of f,1 and A2: CR separates_uniquely ; ::_thesis: instr (1,(f ^ CR),CR) = (len f) + 1 A3: len CR > 0 by A1, FINSEQ_8:def_7; then A4: len CR >= 0 + 1 by NAT_1:13; A5: for j being Element of NAT st j >= 1 & j > 0 & (f ^ CR) /^ (j -' 1) is_preposition_of holds j >= (len f) + 1 proof set i0 = (len f) + 1; set j0 = (((len f) + 1) + (len CR)) -' 1; let j be Element of NAT ; ::_thesis: ( j >= 1 & j > 0 & (f ^ CR) /^ (j -' 1) is_preposition_of implies j >= (len f) + 1 ) assume that A6: j >= 1 and j > 0 and A7: (f ^ CR) /^ (j -' 1) is_preposition_of ; ::_thesis: j >= (len f) + 1 A8: ( len CR > 0 implies ( 1 <= len ((f ^ CR) /^ (j -' 1)) & mid (((f ^ CR) /^ (j -' 1)),1,(len CR)) = CR ) ) by A7, FINSEQ_8:def_8; A9: 0 + j < (len CR) + j by A3, XREAL_1:8; then j + 1 <= (len CR) + j by NAT_1:13; then A10: j <= ((len CR) + j) - 1 by XREAL_1:19; 1 <= (len CR) + j by A6, A9, XXREAL_0:2; then A11: ((len CR) + j) - 1 >= 0 by XREAL_1:48; then A12: ((len CR) + j) -' 1 = ((len CR) + j) - 1 by XREAL_0:def_2; (len CR) - 1 >= 0 by A4, XREAL_1:48; then ((((len CR) + j) -' 1) -' j) + 1 = ((((len CR) + j) - 1) - j) + 1 by A12, XREAL_0:def_2 .= len CR ; then A13: ((f ^ CR) /^ (j -' 1)) | (((((len CR) + j) -' 1) -' j) + 1) = CR by A4, A8, FINSEQ_6:116; (j + (len CR)) - 1 >= 0 by A6, NAT_1:12, XREAL_1:48; then A14: (j + (len CR)) -' 1 = (j + (len CR)) - 1 by XREAL_0:def_2; A15: (((len f) + 1) + (len CR)) -' 1 = (((len f) + (len CR)) + 1) -' 1 .= (len f) + (len CR) by NAT_D:34 ; (((len f) + 1) + (len CR)) -' 1 = (((len CR) + (len f)) + 1) -' 1 .= (len CR) + (len f) by NAT_D:34 ; then mid ((f ^ CR),((len f) + 1),((((len f) + 1) + (len CR)) -' 1)) = CR by A4, Th5; then A16: smid ((f ^ CR),((len f) + 1),((((len f) + 1) + (len CR)) -' 1)) = CR by A4, A15, FINSEQ_8:4, XREAL_1:7; A17: ( len CR > 0 implies len CR >= 0 + 1 ) by NAT_1:13; then j + (len CR) >= j + 1 by A1, FINSEQ_8:def_7, XREAL_1:7; then A18: (j + (len CR)) - 1 >= (j + 1) - 1 by XREAL_1:9; j + (len CR) >= j + 1 by A1, A17, FINSEQ_8:def_7, XREAL_1:7; then A19: (j + (len CR)) - 1 >= (j + 1) - 1 by XREAL_1:9; A20: j - 1 >= 0 by A6, XREAL_1:48; then A21: j -' 1 = j - 1 by XREAL_0:def_2; (j -' 1) + (len CR) = (j - 1) + (len CR) by A20, XREAL_0:def_2 .= ((len CR) + j) -' 1 by A11, XREAL_0:def_2 ; then A22: mid ((f ^ CR),j,((j -' 1) + (len CR))) = CR by A10, A12, A13, FINSEQ_6:def_3; (j -' 1) + (len CR) = (j - 1) + (len CR) by A20, XREAL_0:def_2 .= (j + (len CR)) - 1 ; then A23: smid ((f ^ CR),j,((j + (len CR)) -' 1)) = CR by A14, A19, A22, FINSEQ_8:4; now__::_thesis:_not_j_<_(len_f)_+_1 assume A24: j < (len f) + 1 ; ::_thesis: contradiction then ((len f) + 1) - j > 0 by XREAL_1:50; then A25: ((len f) + 1) -' j = ((len f) + 1) - j by XREAL_0:def_2; (((len f) + 1) + (len CR)) -' 1 <= len (f ^ CR) by A15, FINSEQ_1:22; then ((len f) + 1) -' j >= len CR by A2, A6, A16, A23, A24, FINSEQ_8:def_6; then (((len f) + 1) - j) + j >= (len CR) + j by A25, XREAL_1:7; then ((len f) + 1) - 1 >= (j + (len CR)) - 1 by XREAL_1:9; then mid (f,j,((j -' 1) + (len CR))) = CR by A6, A21, A18, A22, Th6; then j > len f by A1, A6, FINSEQ_8:def_7; hence contradiction by A24, NAT_1:13; ::_thesis: verum end; hence j >= (len f) + 1 ; ::_thesis: verum end; (f ^ CR) /^ (len f) = CR by FINSEQ_5:37; then ( (len f) + 1 <> 0 implies ( 1 <= (len f) + 1 & (f ^ CR) /^ (((len f) + 1) -' 1) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & (f ^ CR) /^ (j -' 1) is_preposition_of holds j >= (len f) + 1 ) ) ) by A5, NAT_1:11, NAT_D:34; hence instr (1,(f ^ CR),CR) = (len f) + 1 by FINSEQ_8:def_10, NAT_1:11; ::_thesis: verum end; theorem :: FILEREC1:20 for D being non empty set for f, CR being FinSequence of D st not CR is_substring_of f,1 & CR separates_uniquely holds f ^ CR is_terminated_by CR proof let D be non empty set ; ::_thesis: for f, CR being FinSequence of D st not CR is_substring_of f,1 & CR separates_uniquely holds f ^ CR is_terminated_by CR let f, CR be FinSequence of D; ::_thesis: ( not CR is_substring_of f,1 & CR separates_uniquely implies f ^ CR is_terminated_by CR ) A1: ((len (f ^ CR)) + 1) -' (len CR) = (((len f) + (len CR)) + 1) -' (len CR) by FINSEQ_1:22 .= ((len CR) + ((len f) + 1)) -' (len CR) .= (len f) + 1 by NAT_D:34 ; len CR <= (len f) + (len CR) by NAT_1:12; then A2: len CR <= len (f ^ CR) by FINSEQ_1:22; assume ( not CR is_substring_of f,1 & CR separates_uniquely ) ; ::_thesis: f ^ CR is_terminated_by CR then instr (1,(f ^ CR),CR) = ((len (f ^ CR)) + 1) -' (len CR) by A1, Th19; hence f ^ CR is_terminated_by CR by A2, FINSEQ_8:def_12; ::_thesis: verum end; notation let D be set ; synonym File of D for FinSequence of D; end; definition let D be non empty set ; let r, f, CR be File of D; predr is_a_record_of f,CR means :Def1: :: FILEREC1:def 1 ( ( CR ^ r is_substring_of addcr (f,CR),1 or addcr (f,CR) is_preposition_of ) & r is_terminated_by CR ); end; :: deftheorem Def1 defines is_a_record_of FILEREC1:def_1_:_ for D being non empty set for r, f, CR being File of D holds ( r is_a_record_of f,CR iff ( ( CR ^ r is_substring_of addcr (f,CR),1 or addcr (f,CR) is_preposition_of ) & r is_terminated_by CR ) ); theorem Th21: :: FILEREC1:21 for D being non empty set for r being FinSequence of D holds ( ovlpart ((<*> D),r) = <*> D & ovlpart (r,(<*> D)) = <*> D ) proof let D be non empty set ; ::_thesis: for r being FinSequence of D holds ( ovlpart ((<*> D),r) = <*> D & ovlpart (r,(<*> D)) = <*> D ) let r be FinSequence of D; ::_thesis: ( ovlpart ((<*> D),r) = <*> D & ovlpart (r,(<*> D)) = <*> D ) ( (<*> D) ^ r = r & r ^ (<*> D) = r ) by FINSEQ_1:34; hence ( ovlpart ((<*> D),r) = <*> D & ovlpart (r,(<*> D)) = <*> D ) by FINSEQ_8:14; ::_thesis: verum end; theorem Th22: :: FILEREC1:22 for D being non empty set for CR being FinSequence of D holds CR is_a_record_of <*> D,CR proof let D be non empty set ; ::_thesis: for CR being FinSequence of D holds CR is_a_record_of <*> D,CR let CR be FinSequence of D; ::_thesis: CR is_a_record_of <*> D,CR A1: CR is_terminated_by CR by FINSEQ_8:28; addcr ((<*> D),CR) = ovlcon ((<*> D),CR) by FINSEQ_8:def_11 .= (<*> D) ^ (CR /^ (len (ovlpart ((<*> D),CR)))) by FINSEQ_8:def_3 .= (<*> D) ^ (CR /^ (len (<*> D))) by Th21 .= (<*> D) ^ (CR /^ 0) .= CR /^ 0 by FINSEQ_1:34 .= CR by FINSEQ_5:28 ; hence CR is_a_record_of <*> D,CR by A1, Def1; ::_thesis: verum end; theorem :: FILEREC1:23 for D being non empty set for a, b being set for f, r, CR being File of D st a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) proof let D be non empty set ; ::_thesis: for a, b being set for f, r, CR being File of D st a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) let a, b be set ; ::_thesis: for f, r, CR being File of D st a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) let f, r, CR be File of D; ::_thesis: ( a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> implies ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) ) assume that A1: a <> b and A2: CR = <*b*> and A3: f = <*b,a,b*> and A4: r = <*a,b*> ; ::_thesis: ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) reconsider b2 = b, a2 = a as Element of D by A3, Th10; A5: ( CR . 1 = b & len CR = 1 ) by A2, FINSEQ_1:40; f = <*b,a*> ^ <*b*> by A3, FINSEQ_1:43 .= (f | 2) ^ CR by A2, A3, Th14 ; then ovlpart (f,CR) = CR by FINSEQ_8:14; then CR /^ (len (ovlpart (f,CR))) = {} by REVROT_1:2; then f ^ (CR /^ (len (ovlpart (f,CR)))) = f by FINSEQ_1:34; then A6: ovlcon (f,CR) = f by FINSEQ_8:def_3; A7: f = CR ^ r by A2, A3, A4, FINSEQ_1:43; then A8: len f = (len CR) + (len r) by FINSEQ_1:22 .= 1 + (len <*a,b*>) by A2, A4, FINSEQ_1:40 .= 1 + 2 by FINSEQ_1:44 .= 3 ; then CR ^ r is_substring_of f,1 by A7, FINSEQ_8:19; then A9: CR ^ r is_substring_of addcr (f,CR),1 by A6, FINSEQ_8:def_11; A10: len CR = 1 by A2, FINSEQ_1:40; then mid (f,1,(len CR)) = (f /^ (1 -' 1)) | ((1 -' 1) + 1) by FINSEQ_6:def_3 .= (f /^ (1 -' 1)) | (1 + 0) by NAT_2:8 .= (f /^ 0) | 1 by NAT_D:34 .= f | 1 by FINSEQ_5:28 .= <*b2,a2,b2*> | (Seg 1) by A3, FINSEQ_1:def_15 .= CR by A2, FINSEQ_6:4 ; then f is_preposition_of by A8, FINSEQ_8:def_8; then A11: addcr (f,CR) is_preposition_of by A6, FINSEQ_8:def_11; r /^ (1 -' 1) = r /^ ((0 + 1) -' 1) .= r /^ 0 by NAT_D:34 .= r by FINSEQ_5:28 ; then (r /^ (1 -' 1)) . 1 = a by A4, FINSEQ_1:44; then A12: not r /^ (1 -' 1) is_preposition_of by A1, A5, FINSEQ_8:21; A13: for j being Element of NAT st j >= 1 & j > 0 & r /^ (j -' 1) is_preposition_of holds j >= 2 proof let j be Element of NAT ; ::_thesis: ( j >= 1 & j > 0 & r /^ (j -' 1) is_preposition_of implies j >= 2 ) assume that A14: j >= 1 and j > 0 and A15: r /^ (j -' 1) is_preposition_of ; ::_thesis: j >= 2 j > 1 by A12, A14, A15, XXREAL_0:1; then 1 + 1 <= j by NAT_1:13; hence j >= 2 ; ::_thesis: verum end; r /^ (2 -' 1) = r /^ ((1 + 1) -' 1) .= <*a2,b2*> /^ 1 by A4, NAT_D:34 .= CR by A2, FINSEQ_6:46 ; then A16: instr (1,r,CR) = 2 by A13, FINSEQ_8:def_10; A17: len r = 2 by A4, FINSEQ_1:44; then ((len r) + 1) -' (len CR) = 2 by A10, NAT_D:34; then ( CR is_terminated_by CR & r is_terminated_by CR ) by A10, A17, A16, FINSEQ_8:28, FINSEQ_8:def_12; hence ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) by A11, A9, Def1; ::_thesis: verum end; theorem Th24: :: FILEREC1:24 for D being non empty set for f, CR being File of D holds f ^ CR is_preposition_of proof let D be non empty set ; ::_thesis: for f, CR being File of D holds f ^ CR is_preposition_of let f, CR be File of D; ::_thesis: f ^ CR is_preposition_of percases ( len f > 0 or len f <= 0 ) ; supposeA1: len f > 0 ; ::_thesis: f ^ CR is_preposition_of len CR >= 0 by NAT_1:2; then 0 + 1 <= (len f) + (len CR) by A1, NAT_1:13; then A2: 1 <= len (f ^ CR) by FINSEQ_1:22; 0 + 1 <= len f by A1, NAT_1:13; then mid ((f ^ CR),1,(len f)) = f by FINSEQ_8:1; hence f ^ CR is_preposition_of by A2, FINSEQ_8:def_8; ::_thesis: verum end; suppose len f <= 0 ; ::_thesis: f ^ CR is_preposition_of hence f ^ CR is_preposition_of by FINSEQ_8:def_8; ::_thesis: verum end; end; end; theorem :: FILEREC1:25 for D being non empty set for f, CR being File of D holds addcr (f,CR) is_preposition_of proof let D be non empty set ; ::_thesis: for f, CR being File of D holds addcr (f,CR) is_preposition_of let f, CR be File of D; ::_thesis: addcr (f,CR) is_preposition_of addcr (f,CR) = ovlcon (f,CR) by FINSEQ_8:def_11 .= f ^ (CR /^ (len (ovlpart (f,CR)))) by FINSEQ_8:def_3 ; hence addcr (f,CR) is_preposition_of by Th24; ::_thesis: verum end; theorem Th26: :: FILEREC1:26 for D being non empty set for r, CR being File of D st CR is_postposition_of r holds 0 <= (len r) - (len CR) proof let D be non empty set ; ::_thesis: for r, CR being File of D st CR is_postposition_of r holds 0 <= (len r) - (len CR) let f, g be File of D; ::_thesis: ( g is_postposition_of f implies 0 <= (len f) - (len g) ) assume g is_postposition_of f ; ::_thesis: 0 <= (len f) - (len g) then len g <= len f by FINSEQ_8:23; then (len g) - (len g) <= (len f) - (len g) by XREAL_1:9; hence 0 <= (len f) - (len g) ; ::_thesis: verum end; theorem Th27: :: FILEREC1:27 for D being non empty set for CR, r being File of D st CR is_postposition_of r holds r = addcr (r,CR) proof let D be non empty set ; ::_thesis: for CR, r being File of D st CR is_postposition_of r holds r = addcr (r,CR) let CR, r be File of D; ::_thesis: ( CR is_postposition_of r implies r = addcr (r,CR) ) A1: len r = len (Rev r) by FINSEQ_5:def_3; assume A2: CR is_postposition_of r ; ::_thesis: r = addcr (r,CR) then A3: ( len CR = len (Rev CR) & Rev r is_preposition_of ) by FINSEQ_5:def_3, FINSEQ_8:def_9; 0 <= (len r) - (len CR) by A2, Th26; then A4: 0 + (len CR) <= ((len r) - (len CR)) + (len CR) by XREAL_1:7; percases ( len CR > 0 or len CR <= 0 ) ; supposeA5: len CR > 0 ; ::_thesis: r = addcr (r,CR) then Rev (mid ((Rev r),1,(len CR))) = Rev (Rev CR) by A3, FINSEQ_8:def_8; then A6: mid ((Rev r),(len CR),1) = Rev (Rev CR) by JORDAN4:18 .= CR ; A7: len (Rev r) = ((len (Rev r)) - (len CR)) + (len CR) ; A8: ( mid (r,(((len r) + 1) -' (len CR)),(len r)) = CR & len CR >= 0 + 1 ) by A2, A5, FINSEQ_8:24, NAT_1:13; now__::_thesis:_(_(_len_CR_>_1_&_r_=_addcr_(r,CR)_)_or_(_len_CR_<=_1_&_r_=_addcr_(r,CR)_)_) percases ( len CR > 1 or len CR <= 1 ) ; caseA9: len CR > 1 ; ::_thesis: r = addcr (r,CR) then len CR >= 1 + 1 by NAT_1:13; then (len CR) - 1 >= (1 + 1) - 1 by XREAL_1:9; then A10: ((len CR) -' 1) + 1 = len CR by NAT_D:43; A11: (len (Rev r)) -' (len CR) = (len (Rev r)) - (len CR) by A1, A4, XREAL_1:233; mid ((Rev r),(len CR),1) = Rev (((Rev r) /^ (1 -' 1)) | (((len CR) -' 1) + 1)) by A9, FINSEQ_6:def_3 .= Rev (((Rev r) /^ 0) | (len CR)) by A10, NAT_2:8 .= Rev ((Rev r) | (len CR)) by FINSEQ_5:28 .= (Rev (Rev r)) /^ ((len (Rev r)) -' (len CR)) by A7, A11, FINSEQ_6:85 .= r /^ ((len r) -' (len CR)) by A1 ; then A12: ovlpart (r,CR) = ovlpart (((r | ((len r) -' (len CR))) ^ CR),CR) by A6, RFINSEQ:8 .= CR by FINSEQ_8:14 ; ovlcon (r,CR) = r ^ (CR /^ (len (ovlpart (r,CR)))) by FINSEQ_8:def_3 .= r ^ {} by A12, REVROT_1:2 .= r by FINSEQ_1:34 ; hence r = addcr (r,CR) by FINSEQ_8:def_11; ::_thesis: verum end; case len CR <= 1 ; ::_thesis: r = addcr (r,CR) then CR = mid (r,(((len r) + 1) -' 1),(len r)) by A8, XXREAL_0:1 .= mid (r,(len r),(len r)) by NAT_D:34 .= r /^ ((len r) -' 1) by FINSEQ_6:117 ; then A13: r = (r | ((len r) -' 1)) ^ CR by RFINSEQ:8; A14: CR /^ (len CR) = {} by REVROT_1:2; ovlcon (r,CR) = r ^ (CR /^ (len (ovlpart (r,CR)))) by FINSEQ_8:def_3 .= r ^ (CR /^ (len CR)) by A13, FINSEQ_8:14 .= r by A14, FINSEQ_1:34 ; hence r = addcr (r,CR) by FINSEQ_8:def_11; ::_thesis: verum end; end; end; hence r = addcr (r,CR) ; ::_thesis: verum end; suppose len CR <= 0 ; ::_thesis: r = addcr (r,CR) then A15: CR = {} by NAT_1:2; then A16: len (ovlpart (r,CR)) = len (<*> D) by Th21 .= 0 ; thus addcr (r,CR) = ovlcon (r,CR) by FINSEQ_8:def_11 .= r ^ (CR /^ (len (ovlpart (r,CR)))) by FINSEQ_8:def_3 .= r ^ CR by A16, FINSEQ_5:28 .= r by A15, FINSEQ_1:34 ; ::_thesis: verum end; end; end; theorem Th28: :: FILEREC1:28 for D being non empty set for CR, r being File of D st r is_terminated_by CR holds r = addcr (r,CR) proof let D be non empty set ; ::_thesis: for CR, r being File of D st r is_terminated_by CR holds r = addcr (r,CR) let CR, r be File of D; ::_thesis: ( r is_terminated_by CR implies r = addcr (r,CR) ) assume A1: r is_terminated_by CR ; ::_thesis: r = addcr (r,CR) percases ( len CR <= 0 or len CR > 0 ) ; suppose len CR <= 0 ; ::_thesis: r = addcr (r,CR) then len CR = 0 by NAT_1:2; then len (Rev CR) = 0 by FINSEQ_5:def_3; then Rev r is_preposition_of by FINSEQ_8:def_8; then CR is_postposition_of r by FINSEQ_8:def_9; hence r = addcr (r,CR) by Th27; ::_thesis: verum end; supposeA2: len CR > 0 ; ::_thesis: r = addcr (r,CR) then 0 < len r by A1, FINSEQ_8:def_12; then 0 + 1 <= len r by NAT_1:13; then A3: 1 <= len (Rev r) by FINSEQ_5:def_3; A4: 0 + 1 <= len CR by A2, NAT_1:13; then (len CR) - 1 >= 0 by XREAL_1:48; then A5: (len CR) -' 1 = (len CR) - 1 by XREAL_0:def_2; A6: len r >= len CR by A1, A2, FINSEQ_8:def_12; then (len r) + 1 > len CR by NAT_1:13; then A7: ((len r) + 1) - (len CR) > 0 by XREAL_1:50; then A8: ((len r) + 1) -' (len CR) = ((len r) + 1) - (len CR) by XREAL_0:def_2; A9: (len r) - (len CR) >= 0 by A6, XREAL_1:48; then A10: (len r) - (len CR) = (len r) -' (len CR) by XREAL_0:def_2; then A11: ( len (r /^ ((len r) -' (len CR))) = (len r) -' ((len r) -' (len CR)) & (len r) - ((len r) -' (len CR)) = (len r) -' ((len r) -' (len CR)) ) by A2, RFINSEQ:29, XREAL_0:def_2; instr (1,r,CR) = ((len r) + 1) -' (len CR) by A1, A2, FINSEQ_8:def_12; then r /^ ((((len r) + 1) -' (len CR)) -' 1) is_preposition_of by A7, A8, FINSEQ_8:def_10; then mid ((r /^ ((((len r) + 1) -' (len CR)) -' 1)),1,(len CR)) = CR by A2, FINSEQ_8:def_8; then ((r /^ ((((len r) + 1) -' (len CR)) -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) = CR by A4, FINSEQ_6:def_3; then A12: ((r /^ ((((len r) + 1) -' (len CR)) -' 1)) /^ 0) | (((len CR) -' 1) + 1) = CR by NAT_2:8; (len r) - ((len r) -' (len CR)) >= 0 by NAT_D:35, XREAL_1:48; then A13: (len r) -' ((len r) -' (len CR)) = (len r) - ((len r) -' (len CR)) by XREAL_0:def_2 .= (len r) - ((len r) - (len CR)) by A9, XREAL_0:def_2 .= len CR ; ((len r) + 1) - (len CR) >= 0 + 1 by A7, A8, NAT_1:13; then (((len r) + 1) -' (len CR)) - 1 >= 0 by A8, XREAL_1:48; then (((len r) + 1) -' (len CR)) -' 1 = (len r) - (len CR) by A8, XREAL_0:def_2; then A14: (r /^ ((len r) -' (len CR))) | (len CR) = CR by A5, A10, A12, FINSEQ_5:28; mid ((Rev r),1,(len CR)) = ((Rev r) /^ (1 -' 1)) | (((len CR) -' 1) + 1) by A4, FINSEQ_6:def_3 .= ((Rev r) /^ 0) | (len CR) by A5, NAT_2:8 .= (Rev r) | ((len r) -' ((len r) -' (len CR))) by A13, FINSEQ_5:28 .= Rev (r /^ ((len r) -' (len CR))) by Th18, NAT_D:35 .= Rev CR by A10, A14, A11, FINSEQ_1:58 ; then mid ((Rev r),1,(len (Rev CR))) = Rev CR by FINSEQ_5:def_3; then Rev r is_preposition_of by A3, FINSEQ_8:def_8; then CR is_postposition_of r by FINSEQ_8:def_9; hence r = addcr (r,CR) by Th27; ::_thesis: verum end; end; end; theorem :: FILEREC1:29 for D being non empty set for f, g being File of D st f is_terminated_by g holds len g <= len f proof let D be non empty set ; ::_thesis: for f, g being File of D st f is_terminated_by g holds len g <= len f let f, g be File of D; ::_thesis: ( f is_terminated_by g implies len g <= len f ) assume A1: f is_terminated_by g ; ::_thesis: len g <= len f percases ( len g > 0 or len g <= 0 ) ; suppose len g > 0 ; ::_thesis: len g <= len f hence len g <= len f by A1, FINSEQ_8:def_12; ::_thesis: verum end; suppose len g <= 0 ; ::_thesis: len g <= len f hence len g <= len f by NAT_1:2; ::_thesis: verum end; end; end; theorem Th30: :: FILEREC1:30 for D being non empty set for f, CR being File of D holds ( len (addcr (f,CR)) >= len f & len (addcr (f,CR)) >= len CR ) proof let D be non empty set ; ::_thesis: for f, CR being File of D holds ( len (addcr (f,CR)) >= len f & len (addcr (f,CR)) >= len CR ) let f, CR be File of D; ::_thesis: ( len (addcr (f,CR)) >= len f & len (addcr (f,CR)) >= len CR ) A1: addcr (f,CR) = ovlcon (f,CR) by FINSEQ_8:def_11; len (ovlcon (f,CR)) = (len f) + ((len CR) -' (len (ovlpart (f,CR)))) by FINSEQ_8:15; hence len (addcr (f,CR)) >= len f by A1, NAT_1:12; ::_thesis: len (addcr (f,CR)) >= len CR ovlcon (f,CR) = (f | ((len f) -' (len (ovlpart (f,CR))))) ^ CR by FINSEQ_8:11; then len (ovlcon (f,CR)) = (len (f | ((len f) -' (len (ovlpart (f,CR)))))) + (len CR) by FINSEQ_1:22; hence len (addcr (f,CR)) >= len CR by A1, NAT_1:12; ::_thesis: verum end; theorem Th31: :: FILEREC1:31 for D being non empty set for f, g being FinSequence of D holds g = (ovlpart (f,g)) ^ (ovlrdiff (f,g)) proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds g = (ovlpart (f,g)) ^ (ovlrdiff (f,g)) let f, g be FinSequence of D; ::_thesis: g = (ovlpart (f,g)) ^ (ovlrdiff (f,g)) ovlpart (f,g) = smid (g,1,(len (ovlpart (f,g)))) by FINSEQ_8:def_2 .= g | (len (ovlpart (f,g))) by FINSEQ_8:5 ; then (ovlpart (f,g)) ^ (ovlrdiff (f,g)) = (g | (len (ovlpart (f,g)))) ^ (g /^ (len (ovlpart (f,g)))) by FINSEQ_8:def_5 .= g by RFINSEQ:8 ; hence g = (ovlpart (f,g)) ^ (ovlrdiff (f,g)) ; ::_thesis: verum end; theorem :: FILEREC1:32 for D being non empty set for f, g being FinSequence of D holds ovlcon (f,g) = (ovlldiff (f,g)) ^ g proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D holds ovlcon (f,g) = (ovlldiff (f,g)) ^ g let f, g be FinSequence of D; ::_thesis: ovlcon (f,g) = (ovlldiff (f,g)) ^ g ovlcon (f,g) = (ovlldiff (f,g)) ^ ((ovlpart (f,g)) ^ (ovlrdiff (f,g))) by FINSEQ_8:12; hence ovlcon (f,g) = (ovlldiff (f,g)) ^ g by Th31; ::_thesis: verum end; theorem :: FILEREC1:33 for D being non empty set for CR, r being File of D holds addcr (r,CR) = (ovlldiff (r,CR)) ^ CR proof let D be non empty set ; ::_thesis: for CR, r being File of D holds addcr (r,CR) = (ovlldiff (r,CR)) ^ CR let CR, r be File of D; ::_thesis: addcr (r,CR) = (ovlldiff (r,CR)) ^ CR addcr (r,CR) = ovlcon (r,CR) by FINSEQ_8:def_11 .= (ovlldiff (r,CR)) ^ ((ovlpart (r,CR)) ^ (ovlrdiff (r,CR))) by FINSEQ_8:12 .= (ovlldiff (r,CR)) ^ CR by Th31 ; hence addcr (r,CR) = (ovlldiff (r,CR)) ^ CR ; ::_thesis: verum end; theorem Th34: :: FILEREC1:34 for D being non empty set for r1, r2, f being File of D st f = r1 ^ r2 holds ( r1 is_substring_of f,1 & r2 is_substring_of f,1 ) proof let D be non empty set ; ::_thesis: for r1, r2, f being File of D st f = r1 ^ r2 holds ( r1 is_substring_of f,1 & r2 is_substring_of f,1 ) let r1, r2, f be File of D; ::_thesis: ( f = r1 ^ r2 implies ( r1 is_substring_of f,1 & r2 is_substring_of f,1 ) ) A1: len (r1 ^ r2) = (len r1) + (len r2) by FINSEQ_1:22; assume A2: f = r1 ^ r2 ; ::_thesis: ( r1 is_substring_of f,1 & r2 is_substring_of f,1 ) A3: now__::_thesis:_r2_is_substring_of_f,1 percases ( len r2 > 0 or len r2 <= 0 ) ; supposeA4: len r2 > 0 ; ::_thesis: r2 is_substring_of f,1 then A5: (len r1) + (len r2) > (len r1) + 0 by XREAL_1:8; A6: r2 | (len r2) = r2 | (Seg (len r2)) by FINSEQ_1:def_15; A7: ((len r1) + (len r2)) -' (len r1) = ((len r1) + (len r2)) - (len r1) by A4, XREAL_0:def_2 .= len r2 ; A8: len r2 >= 0 + 1 by A4, NAT_1:13; then (len r1) + 1 <= len (r1 ^ r2) by A1, XREAL_1:6; then A9: mid ((r1 ^ r2),((len r1) + 1),(len (r1 ^ r2))) = ((r1 ^ r2) /^ (((len r1) + 1) -' 1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by FINSEQ_6:def_3 .= ((r1 ^ r2) /^ (len r1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by NAT_D:34 .= ((r1 ^ r2) /^ (len r1)) | ((((len r1) + (len r2)) -' ((len r1) + 1)) + 1) by FINSEQ_1:22 .= ((r1 ^ r2) /^ (len r1)) | (((len r1) + (len r2)) -' (len r1)) by A5, NAT_2:7 .= r2 | (len r2) by A7, FINSEQ_5:37 .= r2 by A6, FINSEQ_2:20 ; ( len r2 > 0 implies ex i being Element of NAT st ( 1 <= i & i <= len (r1 ^ r2) & mid ((r1 ^ r2),i,((i -' 1) + (len r2))) = r2 ) ) proof consider i being Element of NAT such that A10: i = (len r1) + 1 ; A11: i <= len (r1 ^ r2) by A1, A8, A10, XREAL_1:6; A12: (((len r1) + 1) -' 1) + (len r2) = (len r1) + (len r2) by NAT_D:34 .= len (r1 ^ r2) by FINSEQ_1:22 ; then 1 <= i by A1, A8, A10, XREAL_1:6; hence ( len r2 > 0 implies ex i being Element of NAT st ( 1 <= i & i <= len (r1 ^ r2) & mid ((r1 ^ r2),i,((i -' 1) + (len r2))) = r2 ) ) by A9, A10, A12, A11; ::_thesis: verum end; hence r2 is_substring_of f,1 by A2, FINSEQ_8:def_7; ::_thesis: verum end; suppose len r2 <= 0 ; ::_thesis: r2 is_substring_of f,1 hence r2 is_substring_of f,1 by FINSEQ_8:def_7; ::_thesis: verum end; end; end; A13: ( len r2 >= 0 & len (r1 ^ r2) = (len r1) + (len r2) ) by FINSEQ_1:22, NAT_1:2; now__::_thesis:_r1_is_substring_of_f,1 percases ( len r1 > 0 or len r1 <= 0 ) ; suppose len r1 > 0 ; ::_thesis: r1 is_substring_of f,1 then A14: len r1 >= 0 + 1 by NAT_1:13; then A15: mid ((r1 ^ r2),1,(len r1)) = ((r1 ^ r2) /^ (1 -' 1)) | (((len r1) -' 1) + 1) by FINSEQ_6:def_3 .= ((r1 ^ r2) /^ 0) | (((len r1) -' 1) + 1) by XREAL_1:232 .= ((r1 ^ r2) /^ 0) | (len r1) by A14, XREAL_1:235 .= (r1 ^ r2) | (len r1) by FINSEQ_5:28 .= r1 by FINSEQ_5:23 ; ( len r1 > 0 implies ex i being Element of NAT st ( 1 <= i & i <= len (r1 ^ r2) & mid ((r1 ^ r2),i,((i -' 1) + (len r1))) = r1 ) ) proof set i = 1; A16: (1 -' 1) + (len r1) = 0 + (len r1) by XREAL_1:232 .= len r1 ; 1 <= len (r1 ^ r2) by A13, A14, XREAL_1:7; hence ( len r1 > 0 implies ex i being Element of NAT st ( 1 <= i & i <= len (r1 ^ r2) & mid ((r1 ^ r2),i,((i -' 1) + (len r1))) = r1 ) ) by A15, A16; ::_thesis: verum end; hence r1 is_substring_of f,1 by A2, FINSEQ_8:def_7; ::_thesis: verum end; suppose len r1 <= 0 ; ::_thesis: r1 is_substring_of f,1 hence r1 is_substring_of f,1 by FINSEQ_8:def_7; ::_thesis: verum end; end; end; hence ( r1 is_substring_of f,1 & r2 is_substring_of f,1 ) by A3; ::_thesis: verum end; theorem Th35: :: FILEREC1:35 for D being non empty set for r1, r2, r3, f being File of D st f = (r1 ^ r2) ^ r3 holds ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) proof let D be non empty set ; ::_thesis: for r1, r2, r3, f being File of D st f = (r1 ^ r2) ^ r3 holds ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) let r1, r2, r3, f be File of D; ::_thesis: ( f = (r1 ^ r2) ^ r3 implies ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) ) assume A1: f = (r1 ^ r2) ^ r3 ; ::_thesis: ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) A2: len (r1 ^ r2) = (len r1) + (len r2) by FINSEQ_1:22; A3: len r3 >= 0 by NAT_1:2; A4: now__::_thesis:_r2_is_substring_of_f,1 percases ( len r2 > 0 or len r2 <= 0 ) ; supposeA5: len r2 > 0 ; ::_thesis: r2 is_substring_of f,1 then A6: ((len r1) + (len r2)) -' (len r1) = ((len r1) + (len r2)) - (len r1) by XREAL_0:def_2 .= len r2 ; A7: (len r1) + (len r2) > (len r1) + 0 by A5, XREAL_1:8; len r2 >= 0 + 1 by A5, NAT_1:13; then A8: (len r1) + 1 <= len (r1 ^ r2) by A2, XREAL_1:6; then A9: mid (((r1 ^ r2) ^ r3),((len r1) + 1),(len (r1 ^ r2))) = (((r1 ^ r2) ^ r3) /^ (((len r1) + 1) -' 1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by FINSEQ_6:def_3 .= (((r1 ^ r2) ^ r3) /^ (len r1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by NAT_D:34 .= (((r1 ^ r2) ^ r3) /^ (len r1)) | ((((len r1) + (len r2)) -' ((len r1) + 1)) + 1) by FINSEQ_1:22 .= (((r1 ^ r2) ^ r3) /^ (len r1)) | (((len r1) + (len r2)) -' (len r1)) by A7, NAT_2:7 .= ((r1 ^ (r2 ^ r3)) /^ (len r1)) | (len r2) by A6, FINSEQ_1:32 .= (r2 ^ r3) | (len r2) by FINSEQ_5:37 .= r2 by FINSEQ_5:23 ; len r1 >= 0 by NAT_1:2; then A10: (len r1) + 1 >= 0 + 1 by XREAL_1:6; A11: ((len r1) + 1) + 0 <= ((len r1) + (len r2)) + (len r3) by A3, A2, A8, XREAL_1:7; ( len r2 > 0 implies ex i being Element of NAT st ( 1 <= i & i <= len ((r1 ^ r2) ^ r3) & mid (((r1 ^ r2) ^ r3),i,((i -' 1) + (len r2))) = r2 ) ) proof A12: (((len r1) + 1) -' 1) + (len r2) = (len r1) + (len r2) by NAT_D:34 .= len (r1 ^ r2) by FINSEQ_1:22 ; consider i being Element of NAT such that A13: i = (len r1) + 1 ; i <= len ((r1 ^ r2) ^ r3) by A2, A11, A13, FINSEQ_1:22; hence ( len r2 > 0 implies ex i being Element of NAT st ( 1 <= i & i <= len ((r1 ^ r2) ^ r3) & mid (((r1 ^ r2) ^ r3),i,((i -' 1) + (len r2))) = r2 ) ) by A10, A9, A13, A12; ::_thesis: verum end; hence r2 is_substring_of f,1 by A1, FINSEQ_8:def_7; ::_thesis: verum end; suppose len r2 <= 0 ; ::_thesis: r2 is_substring_of f,1 hence r2 is_substring_of f,1 by FINSEQ_8:def_7; ::_thesis: verum end; end; end; f = r1 ^ (r2 ^ r3) by A1, FINSEQ_1:32; hence ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) by A1, A4, Th34; ::_thesis: verum end; theorem Th36: :: FILEREC1:36 for D being non empty set for CR, r1, r2 being File of D st r1 is_terminated_by CR & r2 is_terminated_by CR holds CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1 proof let D be non empty set ; ::_thesis: for CR, r1, r2 being File of D st r1 is_terminated_by CR & r2 is_terminated_by CR holds CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1 let CR, r1, r2 be File of D; ::_thesis: ( r1 is_terminated_by CR & r2 is_terminated_by CR implies CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1 ) assume that A1: r1 is_terminated_by CR and A2: r2 is_terminated_by CR ; ::_thesis: CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1 r2 = addcr (r2,CR) by A2, Th28; then r2 = ovlcon (r2,CR) by FINSEQ_8:def_11; then A3: r2 = r2 ^ (CR /^ (len (ovlpart (r2,CR)))) by FINSEQ_8:def_3; r1 = addcr (r1,CR) by A1, Th28; then r1 = ovlcon (r1,CR) by FINSEQ_8:def_11; then A4: r1 ^ r2 = ((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ CR) ^ (r2 ^ (CR /^ (len (ovlpart (r2,CR))))) by A3, FINSEQ_8:11; addcr ((r1 ^ r2),CR) = ovlcon ((r1 ^ r2),CR) by FINSEQ_8:def_11 .= (r1 ^ r2) ^ (CR /^ (len (ovlpart ((r1 ^ r2),CR)))) by FINSEQ_8:def_3 .= (((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ (CR ^ r2)) ^ (CR /^ (len (ovlpart (r2,CR))))) ^ (CR /^ (len (ovlpart ((r1 ^ r2),CR)))) by A4, Th1 .= ((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ (CR ^ r2)) ^ ((CR /^ (len (ovlpart (r2,CR)))) ^ (CR /^ (len (ovlpart ((r1 ^ r2),CR))))) by FINSEQ_1:32 ; hence CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1 by Th35; ::_thesis: verum end; theorem Th37: :: FILEREC1:37 for D being non empty set for f, g being File of D for n being Element of NAT st 0 < n & g = {} holds instr (n,f,g) = n proof let D be non empty set ; ::_thesis: for f, g being File of D for n being Element of NAT st 0 < n & g = {} holds instr (n,f,g) = n let f, g be File of D; ::_thesis: for n being Element of NAT st 0 < n & g = {} holds instr (n,f,g) = n let n be Element of NAT ; ::_thesis: ( 0 < n & g = {} implies instr (n,f,g) = n ) assume that A1: 0 < n and A2: g = {} ; ::_thesis: instr (n,f,g) = n A3: len g = 0 by A2; instr (n,f,g) <> 0 proof assume instr (n,f,g) = 0 ; ::_thesis: contradiction then not g is_substring_of f,n by FINSEQ_8:def_10; hence contradiction by A3, FINSEQ_8:def_7; ::_thesis: verum end; then A4: n <= instr (n,f,g) by FINSEQ_8:def_10; f /^ (n -' 1) is_preposition_of by A3, FINSEQ_8:def_8; then n >= instr (n,f,g) by A1, FINSEQ_8:def_10; hence instr (n,f,g) = n by A4, XXREAL_0:1; ::_thesis: verum end; theorem :: FILEREC1:38 for D being non empty set for f, g being File of D for n being Element of NAT st 0 < n & n <= len f holds instr (n,f,g) <= len f proof let D be non empty set ; ::_thesis: for f, g being File of D for n being Element of NAT st 0 < n & n <= len f holds instr (n,f,g) <= len f let f, g be File of D; ::_thesis: for n being Element of NAT st 0 < n & n <= len f holds instr (n,f,g) <= len f let n be Element of NAT ; ::_thesis: ( 0 < n & n <= len f implies instr (n,f,g) <= len f ) assume A1: ( 0 < n & n <= len f ) ; ::_thesis: instr (n,f,g) <= len f assume A2: instr (n,f,g) > len f ; ::_thesis: contradiction then instr (n,f,g) >= (len f) + 1 by NAT_1:13; then (instr (n,f,g)) - 1 >= ((len f) + 1) - 1 by XREAL_1:9; then (instr (n,f,g)) -' 1 >= len f by XREAL_0:def_2; then f /^ ((instr (n,f,g)) -' 1) = {} by FINSEQ_5:32; then A3: len (f /^ ((instr (n,f,g)) -' 1)) < 1 ; instr (n,f,g) > 0 by A2, NAT_1:2; then ( len g >= 0 & f /^ ((instr (n,f,g)) -' 1) is_preposition_of ) by FINSEQ_8:def_10, NAT_1:2; then g = {} by A3, FINSEQ_8:def_8; hence contradiction by A1, A2, Th37; ::_thesis: verum end; theorem Th39: :: FILEREC1:39 for D being non empty set for f, CR being File of D holds CR is_substring_of ovlcon (f,CR),1 proof let D be non empty set ; ::_thesis: for f, CR being File of D holds CR is_substring_of ovlcon (f,CR),1 let f, CR be File of D; ::_thesis: CR is_substring_of ovlcon (f,CR),1 percases ( len CR > 0 or len CR <= 0 ) ; supposeA1: len CR > 0 ; ::_thesis: CR is_substring_of ovlcon (f,CR),1 set i3 = (len f) -' (len (ovlpart (f,CR))); A2: len CR >= 0 + 1 by A1, NAT_1:13; then A3: ((len f) -' (len (ovlpart (f,CR)))) + 1 <= ((len f) -' (len (ovlpart (f,CR)))) + (len CR) by XREAL_1:6; then A4: ((((len f) -' (len (ovlpart (f,CR)))) + (len CR)) -' (((len f) -' (len (ovlpart (f,CR)))) + 1)) + 1 = ((((len f) -' (len (ovlpart (f,CR)))) + (len CR)) - (((len f) -' (len (ovlpart (f,CR)))) + 1)) + 1 by XREAL_1:233 .= len CR ; 1 - (len (ovlpart (f,CR))) <= (len CR) - (len (ovlpart (f,CR))) by A2, XREAL_1:9; then (1 - (len (ovlpart (f,CR)))) + (len f) <= ((len CR) - (len (ovlpart (f,CR)))) + (len f) by XREAL_1:7; then A5: ( (len f) - (len (ovlpart (f,CR))) >= 0 & ((len f) - (len (ovlpart (f,CR)))) + 1 <= (len f) + ((len CR) - (len (ovlpart (f,CR)))) ) by FINSEQ_8:10, XREAL_1:48; len (ovlpart (f,CR)) <= len CR by FINSEQ_8:def_2; then A6: (len CR) - (len (ovlpart (f,CR))) >= 0 by XREAL_1:48; set i4 = ((len f) -' (len (ovlpart (f,CR)))) + 1; A7: (len f) -' (len (ovlpart (f,CR))) <= len (f | ((len f) -' (len (ovlpart (f,CR))))) by FINSEQ_1:59, NAT_D:35; A8: (f | ((len f) -' (len (ovlpart (f,CR))))) /^ ((len f) -' (len (ovlpart (f,CR)))) = (f /^ ((len f) -' (len (ovlpart (f,CR))))) | (((len f) -' (len (ovlpart (f,CR)))) -' ((len f) -' (len (ovlpart (f,CR))))) by FINSEQ_5:80 .= (f /^ ((len f) -' (len (ovlpart (f,CR))))) | 0 by XREAL_1:232 .= {} ; len (CR /^ (len (ovlpart (f,CR)))) = (len CR) -' (len (ovlpart (f,CR))) by RFINSEQ:29 .= (len CR) - (len (ovlpart (f,CR))) by A6, XREAL_0:def_2 ; then ( ovlcon (f,CR) = f ^ (CR /^ (len (ovlpart (f,CR)))) & ((len f) -' (len (ovlpart (f,CR)))) + 1 <= (len f) + (len (CR /^ (len (ovlpart (f,CR))))) ) by A5, FINSEQ_8:def_3, XREAL_0:def_2; then A9: ( 1 <= ((len f) -' (len (ovlpart (f,CR)))) + 1 & ((len f) -' (len (ovlpart (f,CR)))) + 1 <= len (ovlcon (f,CR)) ) by FINSEQ_1:22, NAT_1:11; mid ((ovlcon (f,CR)),(((len f) -' (len (ovlpart (f,CR)))) + 1),(((((len f) -' (len (ovlpart (f,CR)))) + 1) -' 1) + (len CR))) = mid (((f | ((len f) -' (len (ovlpart (f,CR))))) ^ CR),(((len f) -' (len (ovlpart (f,CR)))) + 1),(((((len f) -' (len (ovlpart (f,CR)))) + 1) -' 1) + (len CR))) by FINSEQ_8:11 .= mid (((f | ((len f) -' (len (ovlpart (f,CR))))) ^ CR),(((len f) -' (len (ovlpart (f,CR)))) + 1),(((len f) -' (len (ovlpart (f,CR)))) + (len CR))) by NAT_D:34 .= (((f | ((len f) -' (len (ovlpart (f,CR))))) ^ CR) /^ ((((len f) -' (len (ovlpart (f,CR)))) + 1) -' 1)) | (((((len f) -' (len (ovlpart (f,CR)))) + (len CR)) -' (((len f) -' (len (ovlpart (f,CR)))) + 1)) + 1) by A3, FINSEQ_6:def_3 .= (((f | ((len f) -' (len (ovlpart (f,CR))))) ^ CR) /^ ((len f) -' (len (ovlpart (f,CR))))) | (len CR) by A4, NAT_D:34 .= (((f | ((len f) -' (len (ovlpart (f,CR))))) /^ ((len f) -' (len (ovlpart (f,CR))))) ^ CR) | (len CR) by A7, GENEALG1:1 .= CR | (len CR) by A8, FINSEQ_1:34 .= CR by Th2 ; hence CR is_substring_of ovlcon (f,CR),1 by A9, FINSEQ_8:def_7; ::_thesis: verum end; suppose len CR <= 0 ; ::_thesis: CR is_substring_of ovlcon (f,CR),1 hence CR is_substring_of ovlcon (f,CR),1 by FINSEQ_8:def_7; ::_thesis: verum end; end; end; theorem Th40: :: FILEREC1:40 for D being non empty set for f, CR being File of D holds CR is_substring_of addcr (f,CR),1 proof let D be non empty set ; ::_thesis: for f, CR being File of D holds CR is_substring_of addcr (f,CR),1 let f, CR be File of D; ::_thesis: CR is_substring_of addcr (f,CR),1 addcr (f,CR) = ovlcon (f,CR) by FINSEQ_8:def_11; hence CR is_substring_of addcr (f,CR),1 by Th39; ::_thesis: verum end; theorem Th41: :: FILEREC1:41 for D being non empty set for f, g being FinSequence of D for n being Element of NAT st g is_substring_of f | n,1 & len g > 0 holds g is_substring_of f,1 proof let D be non empty set ; ::_thesis: for f, g being FinSequence of D for n being Element of NAT st g is_substring_of f | n,1 & len g > 0 holds g is_substring_of f,1 let f, g be FinSequence of D; ::_thesis: for n being Element of NAT st g is_substring_of f | n,1 & len g > 0 holds g is_substring_of f,1 let n be Element of NAT ; ::_thesis: ( g is_substring_of f | n,1 & len g > 0 implies g is_substring_of f,1 ) assume that A1: g is_substring_of f | n,1 and A2: len g > 0 ; ::_thesis: g is_substring_of f,1 consider i2 being Element of NAT such that A3: 1 <= i2 and A4: i2 <= len (f | n) and A5: mid ((f | n),i2,((i2 -' 1) + (len g))) = g by A1, A2, FINSEQ_8:def_7; len g >= 0 + 1 by A2, NAT_1:13; then (len g) - 1 >= 0 by XREAL_1:48; then A6: ((len g) - 1) + i2 >= 0 + i2 by XREAL_1:7; then A7: (i2 - 1) + (len g) >= i2 ; percases ( len f >= n or len f < n ) ; supposeA8: len f >= n ; ::_thesis: g is_substring_of f,1 (i2 -' 1) + (len g) = (i2 - 1) + (len g) by A3, XREAL_1:233; then A9: (((i2 -' 1) + (len g)) -' i2) + 1 = (((i2 - 1) + (len g)) - i2) + 1 by A6, XREAL_1:233 .= len g ; i2 - 1 >= 0 by A3, XREAL_1:48; then A10: i2 <= (i2 -' 1) + (len g) by A7, XREAL_0:def_2; then A11: g = ((f | n) /^ (i2 -' 1)) | ((((i2 -' 1) + (len g)) -' i2) + 1) by A5, FINSEQ_6:def_3 .= ((f /^ (i2 -' 1)) | (n -' (i2 -' 1))) | (len g) by A9, FINSEQ_5:80 ; now__::_thesis:_not_n_-'_(i2_-'_1)_<_len_g A12: len (f /^ (i2 -' 1)) = (len f) -' (i2 -' 1) by RFINSEQ:29; assume A13: n -' (i2 -' 1) < len g ; ::_thesis: contradiction then g = (f /^ (i2 -' 1)) | (n -' (i2 -' 1)) by A11, FINSEQ_5:77; hence contradiction by A8, A13, A12, FINSEQ_1:59, NAT_D:42; ::_thesis: verum end; then A14: g = (f /^ (i2 -' 1)) | (len g) by A11, FINSEQ_5:77 .= mid (f,i2,((i2 -' 1) + (len g))) by A10, A9, FINSEQ_6:def_3 ; len (f | n) <= len f by FINSEQ_5:16; then i2 <= len f by A4, XXREAL_0:2; hence g is_substring_of f,1 by A3, A14, FINSEQ_8:def_7; ::_thesis: verum end; suppose len f < n ; ::_thesis: g is_substring_of f,1 hence g is_substring_of f,1 by A1, FINSEQ_1:58; ::_thesis: verum end; end; end; theorem :: FILEREC1:42 for D being non empty set for f, CR being File of D ex r being File of D st r is_a_record_of f,CR proof let D be non empty set ; ::_thesis: for f, CR being File of D ex r being File of D st r is_a_record_of f,CR let f, CR be File of D; ::_thesis: ex r being File of D st r is_a_record_of f,CR set i0 = instr (1,(addcr (f,CR)),CR); A1: instr (1,(addcr (f,CR)),CR) <> 0 proof assume instr (1,(addcr (f,CR)),CR) = 0 ; ::_thesis: contradiction then not CR is_substring_of addcr (f,CR),1 by FINSEQ_8:def_10; hence contradiction by Th40; ::_thesis: verum end; then instr (1,(addcr (f,CR)),CR) > 0 by NAT_1:3; then A2: instr (1,(addcr (f,CR)),CR) >= 0 + 1 by NAT_1:13; then (instr (1,(addcr (f,CR)),CR)) - 1 >= 0 by XREAL_1:48; then A3: (instr (1,(addcr (f,CR)),CR)) -' 1 = (instr (1,(addcr (f,CR)),CR)) - 1 by XREAL_0:def_2; percases ( len f = 0 or len f <> 0 ) ; suppose len f = 0 ; ::_thesis: ex r being File of D st r is_a_record_of f,CR then f = <*> D ; hence ex r being File of D st r is_a_record_of f,CR by Th22; ::_thesis: verum end; supposeA4: len f <> 0 ; ::_thesis: ex r being File of D st r is_a_record_of f,CR set r = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1); A5: (addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) is_preposition_of by A1, FINSEQ_8:def_10; now__::_thesis:_(addcr_(f,CR))_|_(((instr_(1,(addcr_(f,CR)),CR))_+_(len_CR))_-'_1)_is_a_record_of_f,CR percases ( len CR <= 0 or len CR > 0 ) ; supposeA6: len CR <= 0 ; ::_thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR then A7: CR = <*> D by NAT_1:2; then CR /^ (len (ovlpart (f,CR))) = CR by FINSEQ_6:80; then f ^ (CR /^ (len (ovlpart (f,CR)))) = f by A7, FINSEQ_1:34; then A8: ovlcon (f,CR) = f by FINSEQ_8:def_3; len f > 0 by A4, NAT_1:3; then A9: len f >= 0 + 1 by NAT_1:13; A10: ( len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0 implies ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) ) proof assume len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0 ; ::_thesis: ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) then A11: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= 0 + 1 by NAT_1:13; percases ( len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 or len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 ) ; supposeA12: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 ; ::_thesis: ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) = ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by FINSEQ_1:58 .= (addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by A12, FINSEQ_5:77 .= f | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by A8, FINSEQ_8:def_11 .= mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) by A11, FINSEQ_6:116 ; hence ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) by A9; ::_thesis: verum end; supposeA13: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 ; ::_thesis: ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) A14: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) <= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 by FINSEQ_5:17; mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = f | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by A11, FINSEQ_6:116 .= (addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by A8, FINSEQ_8:def_11 ; hence ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) by A9, A13, A14, XXREAL_0:1; ::_thesis: verum end; end; end; A15: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR by A6, FINSEQ_8:def_12; addcr (f,CR) = f by A8, FINSEQ_8:def_11; then addcr (f,CR) is_preposition_of by A10, FINSEQ_8:def_8; hence (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR by A15, Def1; ::_thesis: verum end; supposeA16: len CR > 0 ; ::_thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR (addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) is_preposition_of by A1, FINSEQ_8:def_10; then A17: len CR <= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) by NAT_1:43; then (instr (1,(addcr (f,CR)),CR)) -' 1 <= len (addcr (f,CR)) by A16, CARD_1:27, RFINSEQ:def_1; then len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) = (len (addcr (f,CR))) - ((instr (1,(addcr (f,CR)),CR)) -' 1) by RFINSEQ:def_1; then A18: (len CR) + ((instr (1,(addcr (f,CR)),CR)) -' 1) <= len (addcr (f,CR)) by A17, XREAL_1:19; A19: len CR >= 0 + 1 by A16, NAT_1:13; mid (((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,(len CR)) = CR by A5, A16, FINSEQ_8:def_8; then ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR) = CR by A19, FINSEQ_6:116; then A20: len CR <= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) by FINSEQ_5:16; A21: len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) <= len (addcr (f,CR)) by FINSEQ_5:25; A22: now__::_thesis:_len_((addcr_(f,CR))_|_(((instr_(1,(addcr_(f,CR)),CR))_+_(len_CR))_-'_1))_>=_len_CR percases ( ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 >= len (addcr (f,CR)) or ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 < len (addcr (f,CR)) ) ; suppose ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 >= len (addcr (f,CR)) ; ::_thesis: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR then (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) = addcr (f,CR) by FINSEQ_1:58; hence len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR by A20, A21, XXREAL_0:2; ::_thesis: verum end; supposeA23: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 < len (addcr (f,CR)) ; ::_thesis: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR (instr (1,(addcr (f,CR)),CR)) - 1 >= 0 by A2, XREAL_1:48; then A24: (len CR) + ((instr (1,(addcr (f,CR)),CR)) - 1) >= (len CR) + 0 by XREAL_1:7; then ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 = ((len CR) + (instr (1,(addcr (f,CR)),CR))) - 1 by A16, XREAL_0:def_2; hence len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR by A23, A24, FINSEQ_1:59; ::_thesis: verum end; end; end; ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A2, NAT_1:12, XREAL_1:48; then A25: ((len CR) + (instr (1,(addcr (f,CR)),CR))) -' 1 <= len (addcr (f,CR)) by A3, A18, XREAL_0:def_2; then A26: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) = ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 by FINSEQ_1:59; ( ( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0 implies ( 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of holds j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) ) ) & ( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0 implies not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 ) ) proof thus ( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0 implies ( 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of holds j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) ) ) ::_thesis: ( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0 implies not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 ) proof assume ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0 ; ::_thesis: ( 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of holds j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) ) then 0 + 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) by NAT_1:13; hence 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ; ::_thesis: ( ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of holds j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) ) set f2 = ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1); A27: instr (1,(addcr (f,CR)),CR) <= (instr (1,(addcr (f,CR)),CR)) + (len CR) by NAT_1:12; (instr (1,(addcr (f,CR)),CR)) - 1 >= 0 by A2, XREAL_1:48; then A28: (instr (1,(addcr (f,CR)),CR)) -' 1 = (instr (1,(addcr (f,CR)),CR)) - 1 by XREAL_0:def_2; A29: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48; then ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 = ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 by XREAL_0:def_2; then (instr (1,(addcr (f,CR)),CR)) -' 1 <= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) by A3, A26, A27, XREAL_1:9; then A30: len (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) = (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) - ((instr (1,(addcr (f,CR)),CR)) -' 1) by RFINSEQ:def_1 .= (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1) by A25, FINSEQ_1:59 .= (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) - ((instr (1,(addcr (f,CR)),CR)) - 1) by A29, A28, XREAL_0:def_2 .= len CR ; A31: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48; (instr (1,(addcr (f,CR)),CR)) + (len CR) >= instr (1,(addcr (f,CR)),CR) by NAT_1:12; then (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1) >= 0 by NAT_D:42, XREAL_1:48; then (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) -' ((instr (1,(addcr (f,CR)),CR)) -' 1) = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1) by XREAL_0:def_2 .= (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) - ((instr (1,(addcr (f,CR)),CR)) - 1) by A3, A31, XREAL_0:def_2 .= len CR ; then A32: ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) = ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR) by FINSEQ_5:80; mid (((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,(len CR)) = CR by A5, A16, FINSEQ_8:def_8; then ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) = CR by A19, A32, FINSEQ_6:116; then (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR) = CR by FINSEQ_1:58; then A33: mid ((((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,(len CR)) = CR by A19, FINSEQ_6:116; ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48; then A34: (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1 by XREAL_0:def_2 .= (instr (1,(addcr (f,CR)),CR)) + (len CR) ; ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A2, NAT_1:12, XREAL_1:48; then (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1 = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1 by A26, XREAL_0:def_2; then A35: ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = instr (1,(addcr (f,CR)),CR) by NAT_D:34; ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0 by NAT_1:2; then A36: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,(addcr (f,CR)),CR) by XREAL_0:def_2; (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1 by A31, XREAL_0:def_2 .= (instr (1,(addcr (f,CR)),CR)) + (len CR) ; then ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) = ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) by A3, A18, A36, FINSEQ_1:59; hence ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) is_preposition_of by A16, A30, A33, FINSEQ_8:def_8; ::_thesis: for j being Element of NAT st j >= 1 & j > 0 & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of holds j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0 by NAT_1:2; then A37: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,(addcr (f,CR)),CR) by XREAL_0:def_2; ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48; then A38: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 = ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 by XREAL_0:def_2; thus for j being Element of NAT st j >= 1 & j > 0 & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of holds j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ::_thesis: verum proof let j be Element of NAT ; ::_thesis: ( j >= 1 & j > 0 & ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of implies j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) assume that A39: j >= 1 and j > 0 and A40: ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of ; ::_thesis: j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) A41: (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (len CR) = (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (((j -' 1) + (len CR)) -' (j -' 1)) by NAT_D:34 .= (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | ((len CR) + (j -' 1))) /^ (j -' 1) by FINSEQ_5:80 ; A42: mid ((((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)),1,(len CR)) = (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (len CR) by A19, FINSEQ_6:116; A43: j - 1 >= 0 by A39, XREAL_1:48; now__::_thesis:_not_j_<_((len_((addcr_(f,CR))_|_(((instr_(1,(addcr_(f,CR)),CR))_+_(len_CR))_-'_1)))_+_1)_-'_(len_CR) assume A44: j < ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ; ::_thesis: contradiction then j < instr (1,(addcr (f,CR)),CR) by A3, A18, A34, A37, FINSEQ_1:59; then j -' 1 < (instr (1,(addcr (f,CR)),CR)) -' 1 by A39, NAT_D:56; then A45: len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) <= len ((addcr (f,CR)) /^ (j -' 1)) by Th4; A46: (j + (len CR)) - 1 >= 0 by A39, NAT_1:12, XREAL_1:48; then A47: (j + (len CR)) -' 1 = (len CR) + (j - 1) by XREAL_0:def_2 .= (len CR) + (j -' 1) by A43, XREAL_0:def_2 ; j < ((((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1) -' (len CR) by A25, A44, FINSEQ_1:59; then j + (len CR) < (instr (1,(addcr (f,CR)),CR)) + (len CR) by A34, A37, XREAL_1:8; then (j + (len CR)) - 1 < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 by XREAL_1:9; then A48: (j + (len CR)) -' 1 < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 by A38, A46, XREAL_0:def_2; ((addcr (f,CR)) /^ (j -' 1)) | (len CR) = ((addcr (f,CR)) /^ (j -' 1)) | (((j -' 1) + (len CR)) -' (j -' 1)) by NAT_D:34 .= ((addcr (f,CR)) | ((len CR) + (j -' 1))) /^ (j -' 1) by FINSEQ_5:80 .= (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | ((j + (len CR)) -' 1)) /^ (j -' 1) by A47, A48, FINSEQ_5:77 .= CR by A16, A40, A42, A41, A47, FINSEQ_8:def_8 ; then A49: mid (((addcr (f,CR)) /^ (j -' 1)),1,(len CR)) = CR by A19, FINSEQ_6:116; 1 <= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) by A5, A16, FINSEQ_8:def_8; then 1 <= len ((addcr (f,CR)) /^ (j -' 1)) by A45, XXREAL_0:2; then (addcr (f,CR)) /^ (j -' 1) is_preposition_of by A49, FINSEQ_8:def_8; hence contradiction by A35, A39, A44, FINSEQ_8:def_10; ::_thesis: verum end; hence j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ; ::_thesis: verum end; end; ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0 by NAT_1:2; then A50: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,(addcr (f,CR)),CR) by XREAL_0:def_2; ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48; then A51: (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1 by XREAL_0:def_2 .= (instr (1,(addcr (f,CR)),CR)) + (len CR) ; assume ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0 ; ::_thesis: not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 then instr (1,(addcr (f,CR)),CR) = 0 by A3, A18, A51, A50, FINSEQ_1:59; then not CR is_substring_of addcr (f,CR),1 by FINSEQ_8:def_10; hence not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 by A16, Th41; ::_thesis: verum end; then A52: instr (1,((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)),CR) = ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) by FINSEQ_8:def_10; percases ( 1 <= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) or 1 > len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) ) ; supposeA53: 1 <= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) ; ::_thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR ( (addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) & len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) <= len (addcr (f,CR)) ) by A25, FINSEQ_1:59; then ( len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0 implies ( 1 <= len (addcr (f,CR)) & mid ((addcr (f,CR)),1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) ) by A53, FINSEQ_6:116, XXREAL_0:2; then A54: ( CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) is_substring_of addcr (f,CR),1 or addcr (f,CR) is_preposition_of ) by FINSEQ_8:def_8; (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR by A22, A52, FINSEQ_8:def_12; hence (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR by A54, Def1; ::_thesis: verum end; suppose 1 > len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) ; ::_thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR then A55: 0 + 1 >= (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1 by NAT_1:13; then A56: len CR <= 0 by A22, XREAL_1:6; then A57: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR by FINSEQ_8:def_12; 0 >= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) by A55, XREAL_1:6; then (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) = {} by NAT_1:2; then CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) = CR by FINSEQ_1:34; then CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) is_substring_of addcr (f,CR),1 by A56, FINSEQ_8:def_7; hence (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR by A57, Def1; ::_thesis: verum end; end; end; end; end; hence ex r being File of D st r is_a_record_of f,CR ; ::_thesis: verum end; end; end; theorem :: FILEREC1:43 for D being non empty set for f, CR, r being File of D st r is_a_record_of f,CR holds r is_a_record_of r,CR proof let D be non empty set ; ::_thesis: for f, CR, r being File of D st r is_a_record_of f,CR holds r is_a_record_of r,CR let f, CR, r be File of D; ::_thesis: ( r is_a_record_of f,CR implies r is_a_record_of r,CR ) assume r is_a_record_of f,CR ; ::_thesis: r is_a_record_of r,CR then A1: r is_terminated_by CR by Def1; then addcr (r,CR) is_preposition_of by Th28; hence r is_a_record_of r,CR by A1, Def1; ::_thesis: verum end; theorem :: FILEREC1:44 for D being non empty set for CR, r1, r2, f being File of D st r1 is_terminated_by CR & r2 is_terminated_by CR & f = r1 ^ r2 holds ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) proof let D be non empty set ; ::_thesis: for CR, r1, r2, f being File of D st r1 is_terminated_by CR & r2 is_terminated_by CR & f = r1 ^ r2 holds ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) let CR, r1, r2, f be File of D; ::_thesis: ( r1 is_terminated_by CR & r2 is_terminated_by CR & f = r1 ^ r2 implies ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) ) assume that A1: r1 is_terminated_by CR and A2: r2 is_terminated_by CR and A3: f = r1 ^ r2 ; ::_thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) percases ( ( len r1 <= 0 & len r2 <= 0 ) or ( len r1 <= 0 & len r2 > 0 ) or ( len r1 > 0 & len r2 <= 0 ) or ( len r1 > 0 & len r2 > 0 ) ) ; suppose ( len r1 <= 0 & len r2 <= 0 ) ; ::_thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) then ( addcr (f,CR) is_preposition_of & addcr (f,CR) is_preposition_of ) by FINSEQ_8:def_8; hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A2, Def1; ::_thesis: verum end; supposeA4: ( len r1 <= 0 & len r2 > 0 ) ; ::_thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) then A5: addcr (f,CR) is_preposition_of by FINSEQ_8:def_8; len r1 = 0 by A4, NAT_1:2; then A6: f = r2 by A3, Th3; then addcr (f,CR) is_preposition_of by A2, Th28; hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A2, A5, A6, Def1; ::_thesis: verum end; supposeA7: ( len r1 > 0 & len r2 <= 0 ) ; ::_thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) 0 <= len r2 by NAT_1:2; then 1 + 0 <= (len r1) + (len r2) by A7, NAT_1:13; then A8: 1 <= len f by A3, FINSEQ_1:22; 0 + 1 <= len r1 by A7, NAT_1:13; then A9: mid ((addcr (f,CR)),1,(len r1)) = (addcr (f,CR)) | (len r1) by FINSEQ_6:116 .= (ovlcon (f,CR)) | (len r1) by FINSEQ_8:def_11 .= (f ^ (CR /^ (len (ovlpart (f,CR))))) | (len r1) by FINSEQ_8:def_3 .= (r1 ^ (r2 ^ (CR /^ (len (ovlpart (f,CR)))))) | (len r1) by A3, FINSEQ_1:32 .= r1 | (len r1) by FINSEQ_5:22 .= r1 by FINSEQ_1:58 ; len f <= len (addcr (f,CR)) by Th30; then ( len r1 > 0 implies ( 1 <= len (addcr (f,CR)) & mid ((addcr (f,CR)),1,(len r1)) = r1 ) ) by A8, A9, XXREAL_0:2; then A10: addcr (f,CR) is_preposition_of by FINSEQ_8:def_8; addcr (f,CR) is_preposition_of by A7, FINSEQ_8:def_8; hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A2, A10, Def1; ::_thesis: verum end; supposeA11: ( len r1 > 0 & len r2 > 0 ) ; ::_thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) then 1 + 0 <= (len r1) + (len r2) by NAT_1:13; then A12: 1 <= len f by A3, FINSEQ_1:22; 0 + 1 <= len r1 by A11, NAT_1:13; then A13: mid ((addcr (f,CR)),1,(len r1)) = (addcr (f,CR)) | (len r1) by FINSEQ_6:116 .= (ovlcon (f,CR)) | (len r1) by FINSEQ_8:def_11 .= (f ^ (CR /^ (len (ovlpart (f,CR))))) | (len r1) by FINSEQ_8:def_3 .= (r1 ^ (r2 ^ (CR /^ (len (ovlpart (f,CR)))))) | (len r1) by A3, FINSEQ_1:32 .= r1 | (len r1) by FINSEQ_5:22 .= r1 by FINSEQ_1:58 ; len f <= len (addcr (f,CR)) by Th30; then ( len r1 > 0 implies ( 1 <= len (addcr (f,CR)) & mid ((addcr (f,CR)),1,(len r1)) = r1 ) ) by A12, A13, XXREAL_0:2; then A14: addcr (f,CR) is_preposition_of by FINSEQ_8:def_8; CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1 by A1, A2, Th36; hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A2, A3, A14, Def1; ::_thesis: verum end; end; end;