filerec1.miz



    begin

    reserve a,b,c for set;

    theorem :: FILEREC1:1

    

     Th1: for p,q,r,s be FinSequence 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 p,q,r,s be FinSequence;

      (((p ^ q) ^ r) ^ s) = ((p ^ q) ^ (r ^ s)) by FINSEQ_1: 32;

      hence thesis by FINSEQ_1: 32;

    end;

    theorem :: FILEREC1:2

    

     Th2: for f be FinSequence holds (f | ( len f)) = f

    proof

      let f be FinSequence;

      (f | ( len f)) = (f | ( Seg ( len f))) by FINSEQ_1:def 15;

      hence thesis by FINSEQ_2: 20;

    end;

    theorem :: FILEREC1:3

    

     Th3: for p,q be FinSequence st ( len p) = 0 holds q = (p ^ q)

    proof

      let p,q be FinSequence;

      assume ( len p) = 0 ;

      then p = {} ;

      hence thesis by FINSEQ_1: 34;

    end;

    theorem :: FILEREC1:4

    

     Th4: for D be non empty set, f be FinSequence of D, n,m be Element of NAT st n <= m holds ( len (f /^ m)) <= ( len (f /^ n))

    proof

      let D be non empty set, f be FinSequence of D, n,m be Element of NAT ;

      

       A1: ( len (f /^ m)) = (( len f) -' m) by RFINSEQ: 29;

      assume

       A2: n <= m;

      then

       A3: (n - n) <= (m - n) by XREAL_1: 9;

      now

        per cases ;

          suppose

           A4: ( len f) <= n;

          

          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;

        end;

          suppose

           A5: ( len f) > n;

          per cases ;

            suppose ( len f) <= m;

            

            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;

          end;

            suppose ( len f) > m;

            

            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;

          end;

        end;

      end;

      then ((( len (f /^ n)) - ( len (f /^ m))) + ( len (f /^ m))) >= ( 0 + ( len (f /^ m))) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: FILEREC1:5

    

     Th5: for D be non empty set, f,g be 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, f,g be FinSequence of D;

      assume

       A1: ( len g) >= 1;

      

       A2: (g | ( len g)) = (g | ( Seg ( len g))) by FINSEQ_1:def 15;

      per cases ;

        suppose

         A3: (( len f) + 1) <= (( len f) + ( len 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;

        hence thesis by A2, FINSEQ_2: 20;

      end;

        suppose (( len f) + 1) > (( len f) + ( len g));

        then ((( len f) + 1) - ( len f)) > ((( len f) + ( len g)) - ( len f)) by XREAL_1: 14;

        hence thesis by A1;

      end;

    end;

    theorem :: FILEREC1:6

    

     Th6: for D be non empty set, f,g be FinSequence of D, i,j be 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, f,g be FinSequence of D, i,j be Element of NAT ;

      assume that

       A1: 1 <= i and

       A2: i <= j and

       A3: j <= ( len f);

      

       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 thesis by A2, FINSEQ_6:def 3;

    end;

    theorem :: FILEREC1:7

    for D be non empty set, f be FinSequence of D, i,j,n be 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, f be FinSequence of D, i,j,n be Element of NAT ;

      assume that

       A1: 1 <= i and

       A2: i <= j and

       A3: i <= ( len (f | n)) and

       A4: j <= ( len (f | n));

      

       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 thesis by A2, FINSEQ_6:def 3;

    end;

    theorem :: FILEREC1:8

    for D be non empty set, f be FinSequence of D st f = <*a*> holds a in D

    proof

      let D be non empty set, f be FinSequence of D;

      

       A1: f is Function of ( dom f), D by FINSEQ_2: 26;

      assume

       A2: f = <*a*>;

      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 thesis by A3, A1, FUNCT_2: 5;

    end;

    theorem :: FILEREC1:9

    for D be non empty set, f be FinSequence of D st f = <*a, b*> holds a in D & b in D

    proof

      let D be non empty set, f be FinSequence of D;

      

       A1: f is Function of ( dom f), D by FINSEQ_2: 26;

      assume

       A2: f = <*a, 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;

      hence thesis by A3, A1, FUNCT_2: 5;

    end;

    theorem :: FILEREC1:10

    

     Th10: for D be non empty set, f be FinSequence of D st f = <*a, b, c*> holds a in D & b in D & c in D

    proof

      let D be non empty set, f be FinSequence of D;

      

       A1: f is Function of ( dom f), D by FINSEQ_2: 26;

      assume

       A2: f = <*a, b, c*>;

      then

       A3: (f . 3) = c & 1 in ( dom f) by FINSEQ_1: 45, FINSEQ_1: 81;

      

       A4: 2 in ( dom f) & 3 in ( dom f) by A2, FINSEQ_1: 81;

      (f . 1) = a & (f . 2) = b by A2, FINSEQ_1: 45;

      hence thesis by A3, A4, A1, FUNCT_2: 5;

    end;

    theorem :: FILEREC1:11

    for f be FinSequence st f = <*a*> holds (f | 1) = <*a*>

    proof

      let f be FinSequence;

      assume

       A1: f = <*a*>;

      then ( len f) <= 1 by FINSEQ_1: 40;

      hence thesis by A1, FINSEQ_1: 58;

    end;

    theorem :: FILEREC1:12

    for D be non empty set, f be FinSequence of D st f = <*a, b*> holds (f /^ 1) = <*b*>

    proof

      let D be non empty set, f be FinSequence of D;

      

       A1: f is Function of ( dom f), D by FINSEQ_2: 26;

      assume

       A2: f = <*a, 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 thesis;

    end;

    theorem :: FILEREC1:13

    for D be non empty set, f be FinSequence of D st f = <*a, b, c*> holds (f | 1) = <*a*>

    proof

      let D be non empty set, f be FinSequence of D;

      assume

       A1: f = <*a, b, c*>;

      (f | 1) = (f | ( Seg 1)) by FINSEQ_1:def 15

      .= <*a*> by A1, FINSEQ_6: 4;

      hence thesis;

    end;

    theorem :: FILEREC1:14

    

     Th14: for D be non empty set, f be FinSequence of D st f = <*a, b, c*> holds (f | 2) = <*a, b*>

    proof

      let D be non empty set, f be FinSequence of D;

      assume

       A1: f = <*a, b, c*>;

      (f | 2) = (f | ( Seg 2)) by FINSEQ_1:def 15

      .= <*a, b*> by A1, FINSEQ_6: 5;

      hence thesis;

    end;

    theorem :: FILEREC1:15

    for D be non empty set, f be FinSequence of D st f = <*a, b, c*> holds (f /^ 1) = <*b, c*>

    proof

      let D be non empty set, f be FinSequence of D;

      assume

       A1: f = <*a, 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 thesis by A1, A2, FINSEQ_6: 47;

    end;

    theorem :: FILEREC1:16

    for D be non empty set, f be FinSequence of D st f = <*a, b, c*> holds (f /^ 2) = <*c*>

    proof

      let D be non empty set, f be FinSequence of D;

      assume

       A1: f = <*a, b, 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 thesis;

    end;

    theorem :: FILEREC1:17

    for f be FinSequence st ( len f) = 0 holds ( Rev f) = f

    proof

      let f be FinSequence;

      assume ( len f) = 0 ;

      then f = {} ;

      hence thesis;

    end;

    theorem :: FILEREC1:18

    

     Th18: for D be non empty set, r be FinSequence of D, i be Element of NAT st i <= ( len r) holds ( Rev (r /^ i)) = (( Rev r) | (( len r) -' i))

    proof

      let D be non empty set, r be FinSequence of D, i be Element of NAT ;

      set s = ( Rev r);

      (( len r) -' i) <= ( len r) by NAT_D: 50;

      then (( len r) -' i) <= ( len s) by FINSEQ_5:def 3;

      then

       A1: (( len s) -' i) <= ( len s) by FINSEQ_5:def 3;

      

       A2: ( len (s | (( len r) -' i))) = ( len (s | (( len s) -' i))) by FINSEQ_5:def 3

      .= (( len s) -' i) by A1, FINSEQ_1: 59;

      assume

       A3: i <= ( len r);

      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 be Nat st 1 <= k & k <= ( len ( Rev (r /^ i))) holds (( Rev (r /^ i)) . k) = ((s | (( len r) -' i)) . k)

      proof

        let k be Nat;

        assume that

         A6: 1 <= k and

         A7: k <= ( len ( Rev (r /^ i)));

        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;

        (( 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 + 1) by A11, NAT_1: 13;

        then

         A13: ((( len r) - k) + 1) in ( dom r) by A11, A12, FINSEQ_3: 25;

        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: ((s | (( 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, FINSEQ_5: 27

        .= (r . ((( len r) - k) + 1)) by A20, A13, PARTFUN1:def 6;

        hence thesis by A8, A19;

      end;

      ( len ( Rev (r /^ i))) = ( len (r /^ i)) by FINSEQ_5:def 3

      .= (( len r) -' i) by RFINSEQ: 29

      .= ( len (s | (( len r) -' i))) by A2, FINSEQ_5:def 3;

      hence thesis by A5, FINSEQ_1: 14;

    end;

    theorem :: FILEREC1:19

    

     Th19: for D be non empty set, f,CR be 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, f,CR be FinSequence of D;

      assume that

       A1: not CR is_substring_of (f,1) and

       A2: CR separates_uniquely ;

      

       A3: ( len CR) > 0 by A1, FINSEQ_8:def 7;

      then

       A4: ( len CR) >= ( 0 + 1) by NAT_1: 13;

      

       A5: for j be Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((f ^ CR) /^ (j -' 1)) holds j >= (( len f) + 1)

      proof

        set i0 = (( len f) + 1), j0 = ((i0 + ( len CR)) -' 1);

        let j be Element of NAT ;

        assume that

         A6: j >= 1 and j > 0 and

         A7: CR is_preposition_of ((f ^ CR) /^ (j -' 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: ((i0 + ( len CR)) -' 1) = (((( len f) + ( len CR)) + 1) -' 1)

        .= (( len f) + ( len CR)) by NAT_D: 34;

        j0 = (((( len CR) + ( len f)) + 1) -' 1)

        .= (( len CR) + ( len f)) by NAT_D: 34;

        then ( mid ((f ^ CR),i0,((i0 + ( len CR)) -' 1))) = CR by A4, Th5;

        then

         A16: ( smid ((f ^ CR),i0,((i0 + ( 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

          assume

           A24: j < i0;

          then (i0 - j) > 0 by XREAL_1: 50;

          then

           A25: (i0 -' j) = ((( len f) + 1) - j) by XREAL_0:def 2;

          ((i0 + ( len CR)) -' 1) <= ( len (f ^ CR)) by A15, FINSEQ_1: 22;

          then (i0 -' 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;

        end;

        hence thesis;

      end;

      ((f ^ CR) /^ ( len f)) = CR;

      then (( len f) + 1) <> 0 implies 1 <= (( len f) + 1) & CR is_preposition_of ((f ^ CR) /^ ((( len f) + 1) -' 1)) & for j be Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((f ^ CR) /^ (j -' 1)) holds j >= (( len f) + 1) by A5, NAT_1: 11, NAT_D: 34;

      hence thesis by FINSEQ_8:def 10;

    end;

    theorem :: FILEREC1:20

    for D be non empty set, f,CR be 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, f,CR be FinSequence of D;

      

       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 ;

      then ( instr (1,(f ^ CR),CR)) = ((( len (f ^ CR)) + 1) -' ( len CR)) by A1, Th19;

      hence thesis by A2, FINSEQ_8:def 12;

    end;

    notation

      let D be set;

      synonym File of D for FinSequence of D;

    end

    definition

      let D be non empty set, r,f,CR be File of D;

      :: FILEREC1:def1

      pred r is_a_record_of f,CR means ((CR ^ r) is_substring_of (( addcr (f,CR)),1) or r is_preposition_of ( addcr (f,CR))) & r is_terminated_by CR;

    end

    theorem :: FILEREC1:21

    

     Th21: for D be non empty set, r be FinSequence of D holds ( ovlpart (( <*> D),r)) = ( <*> D) & ( ovlpart (r,( <*> D))) = ( <*> D)

    proof

      let D be non empty set, r be FinSequence of D;

      (( <*> D) ^ r) = r & (r ^ ( <*> D)) = r by FINSEQ_1: 34;

      hence thesis by FINSEQ_8: 14;

    end;

    theorem :: FILEREC1:22

    

     Th22: for D be non empty set, CR be FinSequence of D holds CR is_a_record_of (( <*> D),CR)

    proof

      let D be non empty set, CR be FinSequence of D;

      

       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;

      hence thesis by A1;

    end;

    theorem :: FILEREC1:23

    for D be non empty set, a,b be set, f,r,CR be 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, a,b be set, f,r,CR be File of D;

      assume that

       A1: a <> b and

       A2: CR = <*b*> and

       A3: f = <*b, a, b*> and

       A4: r = <*a, b*>;

      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 FINSEQ_6: 167;

      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)

      .= ( <*b2, a2, b2*> | ( Seg 1)) by A3, FINSEQ_1:def 15

      .= CR by A2, FINSEQ_6: 4;

      then CR is_preposition_of f by A8, FINSEQ_8:def 8;

      then

       A11: CR is_preposition_of ( addcr (f,CR)) by A6, FINSEQ_8:def 11;

      (r /^ (1 -' 1)) = (r /^ (( 0 + 1) -' 1))

      .= (r /^ 0 ) by NAT_D: 34

      .= r;

      then ((r /^ (1 -' 1)) . 1) = a by A4, FINSEQ_1: 44;

      then

       A12: not CR is_preposition_of (r /^ (1 -' 1)) by A1, A5, FINSEQ_8: 21;

      

       A13: for j be Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (r /^ (j -' 1)) holds j >= 2

      proof

        let j be Element of NAT ;

        assume that

         A14: j >= 1 and j > 0 and

         A15: CR is_preposition_of (r /^ (j -' 1));

        j > 1 by A12, A14, A15, XXREAL_0: 1;

        then (1 + 1) <= j by NAT_1: 13;

        hence thesis;

      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 thesis by A11, A9;

    end;

    theorem :: FILEREC1:24

    

     Th24: for D be non empty set, f,CR be File of D holds f is_preposition_of (f ^ CR)

    proof

      let D be non empty set, f,CR be File of D;

      per cases ;

        suppose

         A1: ( len f) > 0 ;

        ( 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 thesis by A2, FINSEQ_8:def 8;

      end;

        suppose ( len f) <= 0 ;

        hence thesis by FINSEQ_8:def 8;

      end;

    end;

    theorem :: FILEREC1:25

    for D be non empty set, f,CR be File of D holds f is_preposition_of ( addcr (f,CR))

    proof

      let D be non empty set, f,CR be File of D;

      ( addcr (f,CR)) = ( ovlcon (f,CR)) by FINSEQ_8:def 11

      .= (f ^ (CR /^ ( len ( ovlpart (f,CR))))) by FINSEQ_8:def 3;

      hence thesis by Th24;

    end;

    theorem :: FILEREC1:26

    

     Th26: for D be non empty set, r,CR be File of D st CR is_postposition_of r holds 0 <= (( len r) - ( len CR))

    proof

      let D be non empty set, f,g be File of D;

      assume g is_postposition_of f;

      then ( len g) <= ( len f) by FINSEQ_8: 23;

      then (( len g) - ( len g)) <= (( len f) - ( len g)) by XREAL_1: 9;

      hence thesis;

    end;

    theorem :: FILEREC1:27

    

     Th27: for D be non empty set, CR,r be File of D st CR is_postposition_of r holds r = ( addcr (r,CR))

    proof

      let D be non empty set, CR,r be File of D;

      

       A1: ( len r) = ( len ( Rev r)) by FINSEQ_5:def 3;

      assume

       A2: CR is_postposition_of r;

      then

       A3: ( len CR) = ( len ( Rev CR)) & ( Rev CR) is_preposition_of ( Rev r) 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;

      per cases ;

        suppose

         A5: ( len CR) > 0 ;

        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

          per cases ;

            case

             A9: ( len CR) > 1;

            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)))

            .= (( 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, FINSEQ_6: 167

            .= r by FINSEQ_1: 34;

            hence thesis by FINSEQ_8:def 11;

          end;

            case ( len CR) <= 1;

            

            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 FINSEQ_6: 167;

            ( 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 thesis by FINSEQ_8:def 11;

          end;

        end;

        hence thesis;

      end;

        suppose ( len CR) <= 0 ;

        then

         A15: CR = {} ;

        

        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

        .= r by A15, FINSEQ_1: 34;

      end;

    end;

    theorem :: FILEREC1:28

    

     Th28: for D be non empty set, CR,r be File of D st r is_terminated_by CR holds r = ( addcr (r,CR))

    proof

      let D be non empty set, CR,r be File of D;

      assume

       A1: r is_terminated_by CR;

      per cases ;

        suppose ( len CR) <= 0 ;

        then ( len CR) = 0 ;

        then ( len ( Rev CR)) = 0 by FINSEQ_5:def 3;

        then ( Rev CR) is_preposition_of ( Rev r) by FINSEQ_8:def 8;

        then CR is_postposition_of r by FINSEQ_8:def 9;

        hence thesis by Th27;

      end;

        suppose

         A2: ( len CR) > 0 ;

        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, 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 RFINSEQ: 29, XREAL_0:def 2;

        ( instr (1,r,CR)) = ((( len r) + 1) -' ( len CR)) by A1, A2, FINSEQ_8:def 12;

        then CR is_preposition_of (r /^ (((( len r) + 1) -' ( len CR)) -' 1)) 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;

        ( 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

        .= ( 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 CR) is_preposition_of ( Rev r) by A3, FINSEQ_8:def 8;

        then CR is_postposition_of r by FINSEQ_8:def 9;

        hence thesis by Th27;

      end;

    end;

    theorem :: FILEREC1:29

    for D be non empty set, f,g be File of D st f is_terminated_by g holds ( len g) <= ( len f) by FINSEQ_8:def 12;

    theorem :: FILEREC1:30

    

     Th30: for D be non empty set, f,CR be File of D holds ( len ( addcr (f,CR))) >= ( len f) & ( len ( addcr (f,CR))) >= ( len CR)

    proof

      let D be non empty set, f,CR be File of D;

      

       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;

      ( 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 thesis by A1, NAT_1: 12;

    end;

    theorem :: FILEREC1:31

    

     Th31: for D be non empty set, f,g be FinSequence of D holds g = (( ovlpart (f,g)) ^ ( ovlrdiff (f,g)))

    proof

      let D be non empty set, f,g be FinSequence of D;

      ( 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 thesis;

    end;

    theorem :: FILEREC1:32

    for D be non empty set, f,g be FinSequence of D holds ( ovlcon (f,g)) = (( ovlldiff (f,g)) ^ g)

    proof

      let D be non empty set, f,g be FinSequence of D;

      ( ovlcon (f,g)) = (( ovlldiff (f,g)) ^ (( ovlpart (f,g)) ^ ( ovlrdiff (f,g)))) by FINSEQ_8: 12;

      hence thesis by Th31;

    end;

    theorem :: FILEREC1:33

    for D be non empty set, CR,r be File of D holds ( addcr (r,CR)) = (( ovlldiff (r,CR)) ^ CR)

    proof

      let D be non empty set, CR,r be File of D;

      

      thus ( 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;

    end;

    theorem :: FILEREC1:34

    

     Th34: for D be non empty set, r1,r2,f be 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, r1,r2,f be File of D;

      

       A1: ( len (r1 ^ r2)) = (( len r1) + ( len r2)) by FINSEQ_1: 22;

      assume

       A2: f = (r1 ^ r2);

       A3:

      now

        per cases ;

          suppose

           A4: ( len r2) > 0 ;

          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 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

          .= r2 by A6, FINSEQ_2: 20;

          ( len r2) > 0 implies ex i be Element of NAT st 1 <= i & i <= ( len (r1 ^ r2)) & ( mid ((r1 ^ r2),i,((i -' 1) + ( len r2)))) = r2

          proof

            consider i be 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;

            1 <= i by A8, A10, XREAL_1: 6;

            hence thesis by A9, A10, A12, A11;

          end;

          hence r2 is_substring_of (f,1) by A2, FINSEQ_8:def 7;

        end;

          suppose ( len r2) <= 0 ;

          hence r2 is_substring_of (f,1) by FINSEQ_8:def 7;

        end;

      end;

      

       A13: ( len r2) >= 0 & ( len (r1 ^ r2)) = (( len r1) + ( len r2)) by FINSEQ_1: 22;

      now

        per cases ;

          suppose ( len r1) > 0 ;

          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))

          .= r1 by FINSEQ_5: 23;

          ( len r1) > 0 implies ex i be 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);

            i <= ( len (r1 ^ r2)) by A13, A14, XREAL_1: 7;

            hence thesis by A15, A16;

          end;

          hence r1 is_substring_of (f,1) by A2, FINSEQ_8:def 7;

        end;

          suppose ( len r1) <= 0 ;

          hence r1 is_substring_of (f,1) by FINSEQ_8:def 7;

        end;

      end;

      hence thesis by A3;

    end;

    theorem :: FILEREC1:35

    

     Th35: for D be non empty set, r1,r2,r3,f be 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, r1,r2,r3,f be File of D;

      assume

       A1: f = ((r1 ^ r2) ^ r3);

      

       A2: ( len (r1 ^ r2)) = (( len r1) + ( len r2)) by FINSEQ_1: 22;

       A3:

      now

        per cases ;

          suppose

           A4: ( len r2) > 0 ;

          

           A5: ((( len r1) + ( len r2)) -' ( len r1)) = ((( len r1) + ( len r2)) - ( len r1)) by XREAL_0:def 2

          .= ( len r2);

          

           A6: (( len r1) + ( len r2)) > (( len r1) + 0 ) by A4, XREAL_1: 8;

          ( len r2) >= ( 0 + 1) by A4, NAT_1: 13;

          then

           A7: (( len r1) + 1) <= ( len (r1 ^ r2)) by A2, XREAL_1: 6;

          

          then

           A8: ( 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 A6, NAT_2: 7

          .= (((r1 ^ (r2 ^ r3)) /^ ( len r1)) | ( len r2)) by A5, FINSEQ_1: 32

          .= ((r2 ^ r3) | ( len r2))

          .= r2 by FINSEQ_5: 23;

          

           A9: (( len r1) + 1) >= ( 0 + 1) by XREAL_1: 6;

          

           A10: ((( len r1) + 1) + 0 ) <= ((( len r1) + ( len r2)) + ( len r3)) by A2, A7, XREAL_1: 7;

          ( len r2) > 0 implies ex i be Element of NAT st 1 <= i & i <= ( len ((r1 ^ r2) ^ r3)) & ( mid (((r1 ^ r2) ^ r3),i,((i -' 1) + ( len r2)))) = r2

          proof

            

             A11: (((( len r1) + 1) -' 1) + ( len r2)) = (( len r1) + ( len r2)) by NAT_D: 34

            .= ( len (r1 ^ r2)) by FINSEQ_1: 22;

            consider i be Element of NAT such that

             A12: i = (( len r1) + 1);

            i <= ( len ((r1 ^ r2) ^ r3)) by A2, A10, A12, FINSEQ_1: 22;

            hence thesis by A9, A8, A12, A11;

          end;

          hence r2 is_substring_of (f,1) by A1, FINSEQ_8:def 7;

        end;

          suppose ( len r2) <= 0 ;

          hence r2 is_substring_of (f,1) by FINSEQ_8:def 7;

        end;

      end;

      f = (r1 ^ (r2 ^ r3)) by A1, FINSEQ_1: 32;

      hence thesis by A1, A3, Th34;

    end;

    theorem :: FILEREC1:36

    

     Th36: for D be non empty set, CR,r1,r2 be 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, CR,r1,r2 be File of D;

      assume that

       A1: r1 is_terminated_by CR and

       A2: r2 is_terminated_by CR;

      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 thesis by Th35;

    end;

    theorem :: FILEREC1:37

    

     Th37: for D be non empty set, f,g be File of D, n be Element of NAT st 0 < n & g = {} holds ( instr (n,f,g)) = n

    proof

      let D be non empty set, f,g be File of D, n be Element of NAT ;

      assume that

       A1: 0 < n and

       A2: g = {} ;

      

       A3: ( len g) = 0 by A2;

      ( instr (n,f,g)) <> 0

      proof

        assume ( instr (n,f,g)) = 0 ;

        then not g is_substring_of (f,n) by FINSEQ_8:def 10;

        hence contradiction by A3, FINSEQ_8:def 7;

      end;

      then

       A4: n <= ( instr (n,f,g)) by FINSEQ_8:def 10;

      g is_preposition_of (f /^ (n -' 1)) by A3, FINSEQ_8:def 8;

      then n >= ( instr (n,f,g)) by A1, FINSEQ_8:def 10;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: FILEREC1:38

    for D be non empty set, f,g be File of D, n be Element of NAT st 0 < n & n <= ( len f) holds ( instr (n,f,g)) <= ( len f)

    proof

      let D be non empty set, f,g be File of D, n be Element of NAT ;

      assume

       A1: 0 < n & n <= ( len f);

      assume

       A2: ( instr (n,f,g)) > ( len f);

      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;

      then ( len g) >= 0 & g is_preposition_of (f /^ (( instr (n,f,g)) -' 1)) by FINSEQ_8:def 10;

      then g = {} by A3, FINSEQ_8:def 8;

      hence thesis by A1, A2, Th37;

    end;

    theorem :: FILEREC1:39

    

     Th39: for D be non empty set, f,CR be File of D holds CR is_substring_of (( ovlcon (f,CR)),1)

    proof

      let D be non empty set, f,CR be File of D;

      per cases ;

        suppose

         A1: ( len CR) > 0 ;

        set i3 = (( len f) -' ( len ( ovlpart (f,CR))));

        

         A2: ( len CR) >= ( 0 + 1) by A1, NAT_1: 13;

        then

         A3: (i3 + 1) <= (i3 + ( len CR)) by XREAL_1: 6;

        

        then

         A4: (((i3 + ( len CR)) -' (i3 + 1)) + 1) = (((i3 + ( len CR)) - (i3 + 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: i3 <= ( len (f | i3)) by FINSEQ_1: 59, NAT_D: 35;

        

         A8: ((f | i3) /^ i3) = ((f /^ i3) | (i3 -' i3)) by FINSEQ_5: 80

        .= ((f /^ i3) | 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 <= i4 & i4 <= ( len ( ovlcon (f,CR))) by FINSEQ_1: 22, NAT_1: 11;

        ( mid (( ovlcon (f,CR)),i4,((i4 -' 1) + ( len CR)))) = ( mid (((f | i3) ^ CR),i4,((i4 -' 1) + ( len CR)))) by FINSEQ_8: 11

        .= ( mid (((f | i3) ^ CR),(i3 + 1),(i3 + ( len CR)))) by NAT_D: 34

        .= ((((f | i3) ^ CR) /^ ((i3 + 1) -' 1)) | (((i3 + ( len CR)) -' (i3 + 1)) + 1)) by A3, FINSEQ_6:def 3

        .= ((((f | i3) ^ CR) /^ i3) | ( len CR)) by A4, NAT_D: 34

        .= ((((f | i3) /^ i3) ^ CR) | ( len CR)) by A7, GENEALG1: 1

        .= (CR | ( len CR)) by A8, FINSEQ_1: 34

        .= CR by Th2;

        hence thesis by A9, FINSEQ_8:def 7;

      end;

        suppose ( len CR) <= 0 ;

        hence thesis by FINSEQ_8:def 7;

      end;

    end;

    theorem :: FILEREC1:40

    

     Th40: for D be non empty set, f,CR be File of D holds CR is_substring_of (( addcr (f,CR)),1)

    proof

      let D be non empty set, f,CR be File of D;

      ( addcr (f,CR)) = ( ovlcon (f,CR)) by FINSEQ_8:def 11;

      hence thesis by Th39;

    end;

    theorem :: FILEREC1:41

    

     Th41: for D be non empty set, f,g be FinSequence of D, n be 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, f,g be FinSequence of D, n be Element of NAT ;

      assume that

       A1: g is_substring_of ((f | n),1) and

       A2: ( len g) > 0 ;

      consider i2 be 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;

      per cases ;

        suppose

         A8: ( len f) >= n;

        ((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

          

           A12: ( len (f /^ (i2 -' 1))) = (( len f) -' (i2 -' 1)) by RFINSEQ: 29;

          assume

           A13: (n -' (i2 -' 1)) < ( len g);

          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;

        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 thesis by A3, A14, FINSEQ_8:def 7;

      end;

        suppose ( len f) < n;

        hence thesis by A1, FINSEQ_1: 58;

      end;

    end;

    theorem :: FILEREC1:42

    for D be non empty set, f,CR be File of D holds ex r be File of D st r is_a_record_of (f,CR)

    proof

      let D be non empty set, f,CR be File of D;

      set i0 = ( instr (1,( addcr (f,CR)),CR));

      

       A1: i0 <> 0

      proof

        assume i0 = 0 ;

        then not CR is_substring_of (( addcr (f,CR)),1) by FINSEQ_8:def 10;

        hence contradiction by Th40;

      end;

      then i0 > 0 ;

      then

       A2: i0 >= ( 0 + 1) by NAT_1: 13;

      then (i0 - 1) >= 0 by XREAL_1: 48;

      then

       A3: (i0 -' 1) = (i0 - 1) by XREAL_0:def 2;

      per cases ;

        suppose ( len f) = 0 ;

        then f = ( <*> D);

        hence thesis by Th22;

      end;

        suppose

         A4: ( len f) <> 0 ;

        set r = (( addcr (f,CR)) | ((i0 + ( len CR)) -' 1));

        

         A5: CR is_preposition_of (( addcr (f,CR)) /^ (i0 -' 1)) by A1, FINSEQ_8:def 10;

        now

          per cases ;

            suppose

             A6: ( len CR) <= 0 ;

            then

             A7: CR = ( <*> D);

            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;

            then

             A9: ( len f) >= ( 0 + 1) by NAT_1: 13;

            

             A10: ( len r) > 0 implies 1 <= ( len f) & ( mid (f,1,( len r))) = r

            proof

              assume ( len r) > 0 ;

              then

               A11: ( len r) >= ( 0 + 1) by NAT_1: 13;

              per cases ;

                suppose

                 A12: ( len r) < ((i0 + ( len CR)) -' 1);

                r = ((( addcr (f,CR)) | ((i0 + ( len CR)) -' 1)) | ( len r)) by FINSEQ_1: 58

                .= (( addcr (f,CR)) | ( len r)) by A12, FINSEQ_5: 77

                .= (f | ( len r)) by A8, FINSEQ_8:def 11

                .= ( mid (f,1,( len r))) by A11, FINSEQ_6: 116;

                hence thesis by A9;

              end;

                suppose

                 A13: ( len r) >= ((i0 + ( len CR)) -' 1);

                

                 A14: ( len r) <= ((i0 + ( len CR)) -' 1) by FINSEQ_5: 17;

                ( mid (f,1,( len r))) = (f | ( len r)) by A11, FINSEQ_6: 116

                .= (( addcr (f,CR)) | ( len r)) by A8, FINSEQ_8:def 11;

                hence thesis by A9, A13, A14, XXREAL_0: 1;

              end;

            end;

            

             A15: r is_terminated_by CR by A6, FINSEQ_8:def 12;

            ( addcr (f,CR)) = f by A8, FINSEQ_8:def 11;

            then r is_preposition_of ( addcr (f,CR)) by A10, FINSEQ_8:def 8;

            hence r is_a_record_of (f,CR) by A15;

          end;

            suppose

             A16: ( len CR) > 0 ;

            CR is_preposition_of (( addcr (f,CR)) /^ (i0 -' 1)) by A1, FINSEQ_8:def 10;

            then

             A17: ( len CR) <= ( len (( addcr (f,CR)) /^ (i0 -' 1))) by NAT_1: 43;

            then (i0 -' 1) <= ( len ( addcr (f,CR))) by A16, CARD_1: 27, RFINSEQ:def 1;

            then ( len (( addcr (f,CR)) /^ (i0 -' 1))) = (( len ( addcr (f,CR))) - (i0 -' 1)) by RFINSEQ:def 1;

            then

             A18: (( len CR) + (i0 -' 1)) <= ( len ( addcr (f,CR))) by A17, XREAL_1: 19;

            

             A19: ( len CR) >= ( 0 + 1) by A16, NAT_1: 13;

            ( mid ((( addcr (f,CR)) /^ (i0 -' 1)),1,( len CR))) = CR by A5, A16, FINSEQ_8:def 8;

            then ((( addcr (f,CR)) /^ (i0 -' 1)) | ( len CR)) = CR by A19, FINSEQ_6: 116;

            then

             A20: ( len CR) <= ( len (( addcr (f,CR)) /^ (i0 -' 1))) by FINSEQ_5: 16;

            

             A21: ( len (( addcr (f,CR)) /^ (i0 -' 1))) <= ( len ( addcr (f,CR))) by FINSEQ_5: 25;

             A22:

            now

              per cases ;

                suppose ((i0 + ( len CR)) -' 1) >= ( len ( addcr (f,CR)));

                then (( addcr (f,CR)) | ((i0 + ( len CR)) -' 1)) = ( addcr (f,CR)) by FINSEQ_1: 58;

                hence ( len (( addcr (f,CR)) | ((i0 + ( len CR)) -' 1))) >= ( len CR) by A20, A21, XXREAL_0: 2;

              end;

                suppose

                 A23: ((i0 + ( len CR)) -' 1) < ( len ( addcr (f,CR)));

                (i0 - 1) >= 0 by A2, XREAL_1: 48;

                then

                 A24: (( len CR) + (i0 - 1)) >= (( len CR) + 0 ) by XREAL_1: 7;

                then ((i0 + ( len CR)) -' 1) = ((( len CR) + i0) - 1) by XREAL_0:def 2;

                hence ( len (( addcr (f,CR)) | ((i0 + ( len CR)) -' 1))) >= ( len CR) by A23, A24, FINSEQ_1: 59;

              end;

            end;

            ((i0 + ( len CR)) - 1) >= 0 by A2, NAT_1: 12, XREAL_1: 48;

            then

             A25: ((( len CR) + i0) -' 1) <= ( len ( addcr (f,CR))) by A3, A18, XREAL_0:def 2;

            then

             A26: ( len r) = ((i0 + ( len CR)) -' 1) by FINSEQ_1: 59;

            (((( len r) + 1) -' ( len CR)) <> 0 implies 1 <= ((( len r) + 1) -' ( len CR)) & CR is_preposition_of (r /^ (((( len r) + 1) -' ( len CR)) -' 1)) & for j be Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (r /^ (j -' 1)) holds j >= ((( len r) + 1) -' ( len CR))) & (((( len r) + 1) -' ( len CR)) = 0 implies not CR is_substring_of (r,1))

            proof

              thus ((( len r) + 1) -' ( len CR)) <> 0 implies 1 <= ((( len r) + 1) -' ( len CR)) & CR is_preposition_of (r /^ (((( len r) + 1) -' ( len CR)) -' 1)) & for j be Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (r /^ (j -' 1)) holds j >= ((( len r) + 1) -' ( len CR))

              proof

                assume ((( len r) + 1) -' ( len CR)) <> 0 ;

                then ( 0 + 1) <= ((( len r) + 1) -' ( len CR)) by NAT_1: 13;

                hence 1 <= ((( len r) + 1) -' ( len CR));

                set f2 = ((( addcr (f,CR)) | ((i0 + ( len CR)) -' 1)) /^ (i0 -' 1));

                

                 A27: i0 <= (i0 + ( len CR)) by NAT_1: 12;

                (i0 - 1) >= 0 by A2, XREAL_1: 48;

                then

                 A28: (i0 -' 1) = (i0 - 1) by XREAL_0:def 2;

                

                 A29: ((i0 + ( len CR)) - 1) >= 0 by A19, NAT_1: 12, XREAL_1: 48;

                then ((i0 + ( len CR)) -' 1) = ((i0 + ( len CR)) - 1) by XREAL_0:def 2;

                then (i0 -' 1) <= ( len r) by A3, A26, A27, XREAL_1: 9;

                

                then

                 A30: ( len f2) = (( len r) - (i0 -' 1)) by RFINSEQ:def 1

                .= (((i0 + ( len CR)) -' 1) - (i0 -' 1)) by A25, FINSEQ_1: 59

                .= (((i0 + ( len CR)) - 1) - (i0 - 1)) by A29, A28, XREAL_0:def 2

                .= ( len CR);

                

                 A31: ((i0 + ( len CR)) - 1) >= 0 by A19, NAT_1: 12, XREAL_1: 48;

                (i0 + ( len CR)) >= i0 by NAT_1: 12;

                then (((i0 + ( len CR)) -' 1) - (i0 -' 1)) >= 0 by NAT_D: 42, XREAL_1: 48;

                

                then (((i0 + ( len CR)) -' 1) -' (i0 -' 1)) = (((i0 + ( len CR)) -' 1) - (i0 -' 1)) by XREAL_0:def 2

                .= (((i0 + ( len CR)) - 1) - (i0 - 1)) by A3, A31, XREAL_0:def 2

                .= ( len CR);

                then

                 A32: ((( addcr (f,CR)) | ((i0 + ( len CR)) -' 1)) /^ (i0 -' 1)) = ((( addcr (f,CR)) /^ (i0 -' 1)) | ( len CR)) by FINSEQ_5: 80;

                ( mid ((( addcr (f,CR)) /^ (i0 -' 1)),1,( len CR))) = CR by A5, A16, FINSEQ_8:def 8;

                then f2 = CR by A19, A32, FINSEQ_6: 116;

                then (f2 | ( len CR)) = CR by FINSEQ_1: 58;

                then

                 A33: ( mid (f2,1,( len CR))) = CR by A19, FINSEQ_6: 116;

                ((i0 + ( len CR)) - 1) >= 0 by A19, NAT_1: 12, XREAL_1: 48;

                

                then

                 A34: (((i0 + ( len CR)) -' 1) + 1) = (((i0 + ( len CR)) - 1) + 1) by XREAL_0:def 2

                .= (i0 + ( len CR));

                ((i0 + ( len CR)) - 1) >= 0 by A2, NAT_1: 12, XREAL_1: 48;

                then (( len r) + 1) = (((i0 + ( len CR)) - 1) + 1) by A26, XREAL_0:def 2;

                then

                 A35: ((( len r) + 1) -' ( len CR)) = i0 by NAT_D: 34;

                ((i0 + ( len CR)) - ( len CR)) >= 0 ;

                then

                 A36: ((i0 + ( len CR)) -' ( len CR)) = i0 by XREAL_0:def 2;

                (((i0 + ( len CR)) -' 1) + 1) = (((i0 + ( len CR)) - 1) + 1) by A31, XREAL_0:def 2

                .= (i0 + ( len CR));

                then (r /^ (((( len r) + 1) -' ( len CR)) -' 1)) = ((( addcr (f,CR)) | ((i0 + ( len CR)) -' 1)) /^ (i0 -' 1)) by A3, A18, A36, FINSEQ_1: 59;

                hence CR is_preposition_of (r /^ (((( len r) + 1) -' ( len CR)) -' 1)) by A16, A30, A33, FINSEQ_8:def 8;

                ((i0 + ( len CR)) - ( len CR)) >= 0 ;

                then

                 A37: ((i0 + ( len CR)) -' ( len CR)) = i0 by XREAL_0:def 2;

                ((i0 + ( len CR)) - 1) >= 0 by A19, NAT_1: 12, XREAL_1: 48;

                then

                 A38: ((i0 + ( len CR)) -' 1) = ((i0 + ( len CR)) - 1) by XREAL_0:def 2;

                thus for j be Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (r /^ (j -' 1)) holds j >= ((( len r) + 1) -' ( len CR))

                proof

                  let j be Element of NAT ;

                  assume that

                   A39: j >= 1 and j > 0 and

                   A40: CR is_preposition_of (r /^ (j -' 1));

                  

                   A41: ((r /^ (j -' 1)) | ( len CR)) = ((r /^ (j -' 1)) | (((j -' 1) + ( len CR)) -' (j -' 1))) by NAT_D: 34

                  .= ((r | (( len CR) + (j -' 1))) /^ (j -' 1)) by FINSEQ_5: 80;

                  

                   A42: ( mid ((r /^ (j -' 1)),1,( len CR))) = ((r /^ (j -' 1)) | ( len CR)) by A19, FINSEQ_6: 116;

                  

                   A43: (j - 1) >= 0 by A39, XREAL_1: 48;

                  now

                    assume

                     A44: j < ((( len r) + 1) -' ( len CR));

                    then j < i0 by A3, A18, A34, A37, FINSEQ_1: 59;

                    then (j -' 1) < (i0 -' 1) by A39, NAT_D: 56;

                    then

                     A45: ( len (( addcr (f,CR)) /^ (i0 -' 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 < ((((i0 + ( len CR)) -' 1) + 1) -' ( len CR)) by A25, A44, FINSEQ_1: 59;

                    then (j + ( len CR)) < (i0 + ( len CR)) by A34, A37, XREAL_1: 8;

                    then ((j + ( len CR)) - 1) < ((i0 + ( len CR)) - 1) by XREAL_1: 9;

                    then

                     A48: ((j + ( len CR)) -' 1) < ((i0 + ( 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)) | ((i0 + ( 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)) /^ (i0 -' 1))) by A5, A16, FINSEQ_8:def 8;

                    then 1 <= ( len (( addcr (f,CR)) /^ (j -' 1))) by A45, XXREAL_0: 2;

                    then CR is_preposition_of (( addcr (f,CR)) /^ (j -' 1)) by A49, FINSEQ_8:def 8;

                    hence contradiction by A35, A39, A44, FINSEQ_8:def 10;

                  end;

                  hence thesis;

                end;

              end;

              ((i0 + ( len CR)) - ( len CR)) >= 0 ;

              then

               A50: ((i0 + ( len CR)) -' ( len CR)) = i0 by XREAL_0:def 2;

              ((i0 + ( len CR)) - 1) >= 0 by A19, NAT_1: 12, XREAL_1: 48;

              

              then

               A51: (((i0 + ( len CR)) -' 1) + 1) = (((i0 + ( len CR)) - 1) + 1) by XREAL_0:def 2

              .= (i0 + ( len CR));

              assume ((( len r) + 1) -' ( len CR)) = 0 ;

              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 thesis by A16, Th41;

            end;

            then

             A52: ( instr (1,r,CR)) = ((( len r) + 1) -' ( len CR)) by FINSEQ_8:def 10;

            per cases ;

              suppose

               A53: 1 <= ( len r);

              (( addcr (f,CR)) | ( len r)) = r & ( len (( addcr (f,CR)) | ((i0 + ( len CR)) -' 1))) <= ( len ( addcr (f,CR))) by A25, FINSEQ_1: 59;

              then ( len r) > 0 implies 1 <= ( len ( addcr (f,CR))) & ( mid (( addcr (f,CR)),1,( len r))) = r by A53, FINSEQ_6: 116, XXREAL_0: 2;

              then

               A54: (CR ^ r) is_substring_of (( addcr (f,CR)),1) or r is_preposition_of ( addcr (f,CR)) by FINSEQ_8:def 8;

              r is_terminated_by CR by A22, A52, FINSEQ_8:def 12;

              hence r is_a_record_of (f,CR) by A54;

            end;

              suppose 1 > ( len r);

              then

               A55: ( 0 + 1) >= (( len r) + 1) by NAT_1: 13;

              then

               A56: ( len CR) <= 0 by A22, XREAL_1: 6;

              then

               A57: r is_terminated_by CR by FINSEQ_8:def 12;

               0 >= ( len r) by A55, XREAL_1: 6;

              then r = {} ;

              then (CR ^ r) = CR by FINSEQ_1: 34;

              then (CR ^ r) is_substring_of (( addcr (f,CR)),1) by A56, FINSEQ_8:def 7;

              hence r is_a_record_of (f,CR) by A57;

            end;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: FILEREC1:43

    for D be non empty set, f,CR,r be File of D st r is_a_record_of (f,CR) holds r is_a_record_of (r,CR) by Th28;

    theorem :: FILEREC1:44

    for D be non empty set, CR,r1,r2,f be 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, CR,r1,r2,f be File of D;

      assume that

       A1: r1 is_terminated_by CR and

       A2: r2 is_terminated_by CR and

       A3: f = (r1 ^ r2);

      per cases ;

        suppose ( len r1) <= 0 & ( len r2) <= 0 ;

        then r1 is_preposition_of ( addcr (f,CR)) & r2 is_preposition_of ( addcr (f,CR)) by FINSEQ_8:def 8;

        hence thesis by A1, A2;

      end;

        suppose

         A4: ( len r1) <= 0 & ( len r2) > 0 ;

        then

         A5: r1 is_preposition_of ( addcr (f,CR)) by FINSEQ_8:def 8;

        ( len r1) = 0 by A4;

        then

         A6: f = r2 by A3, Th3;

        then f is_preposition_of ( addcr (f,CR)) by A2, Th28;

        hence thesis by A1, A2, A5, A6;

      end;

        suppose

         A7: ( len r1) > 0 & ( len r2) <= 0 ;

        (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: r1 is_preposition_of ( addcr (f,CR)) by FINSEQ_8:def 8;

        r2 is_preposition_of ( addcr (f,CR)) by A7, FINSEQ_8:def 8;

        hence thesis by A1, A2, A10;

      end;

        suppose

         A11: ( len r1) > 0 & ( len r2) > 0 ;

        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: r1 is_preposition_of ( addcr (f,CR)) by FINSEQ_8:def 8;

        (CR ^ r2) is_substring_of (( addcr ((r1 ^ r2),CR)),1) by A1, A2, Th36;

        hence thesis by A1, A2, A3, A14;

      end;

    end;