finseq_8.miz



    begin

    theorem :: FINSEQ_8:1

    for f,g be FinSequence st ( len f) >= 1 holds ( mid ((f ^ g),1,( len f))) = f

    proof

      let f,g be FinSequence;

      assume

       A1: ( len f) >= 1;

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

      then (( len f) - 1) = (( len f) -' 1) by XREAL_0:def 2;

      then

       A2: ((( len f) -' 1) + 1) = ( len f);

      (1 - 1) = 0 ;

      then

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

      ((f ^ g) | ( len f)) = f by FINSEQ_5: 23;

      then (((f ^ g) /^ 0 ) | ( len f)) = f by FINSEQ_5: 28;

      hence thesis by A1, A2, A3, FINSEQ_6:def 3;

    end;

    theorem :: FINSEQ_8:2

    

     Th2: for f be FinSequence, i be Nat st i >= ( len f) holds (f /^ i) = {}

    proof

      let f be FinSequence, i be Nat;

      assume

       A1: i >= ( len f);

      per cases by A1, XXREAL_0: 1;

        suppose i > ( len f);

        hence thesis by RFINSEQ:def 1;

      end;

        suppose

         A2: i = ( len f);

        

        then ( len (f /^ i)) = (( len f) - i) by RFINSEQ:def 1

        .= 0 by A2;

        hence thesis;

      end;

    end;

    theorem :: FINSEQ_8:3

    for D be non empty set, k1,k2 be Nat holds ( mid (( <*> D),k1,k2)) = ( <*> D)

    proof

      let D be non empty set, k1,k2 be Nat;

      per cases ;

        suppose k1 <= k2;

        

        hence ( mid (( <*> D),k1,k2)) = ((( <*> D) /^ (k1 -' 1)) | ((k2 -' k1) + 1)) by FINSEQ_6:def 3

        .= (( <*> D) | ((k2 -' k1) + 1)) by FINSEQ_6: 80

        .= ( <*> D) by FINSEQ_5: 78;

      end;

        suppose k1 > k2;

        

        hence ( mid (( <*> D),k1,k2)) = ( Rev ((( <*> D) /^ (k2 -' 1)) | ((k1 -' k2) + 1))) by FINSEQ_6:def 3

        .= ( Rev (( <*> D) | ((k1 -' k2) + 1))) by FINSEQ_6: 80

        .= ( Rev ( <*> D)) by FINSEQ_5: 78

        .= ( <*> D) by FINSEQ_5: 79;

      end;

    end;

    definition

      let f be FinSequence, k1,k2 be Nat;

      :: FINSEQ_8:def1

      func smid (f,k1,k2) -> FinSequence equals ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1));

      correctness ;

    end

    definition

      let D be set, f be FinSequence of D, k1,k2 be Nat;

      :: original: smid

      redefine

      func smid (f,k1,k2) -> FinSequence of D ;

      correctness

      proof

        ( smid (f,k1,k2)) = ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1));

        hence thesis;

      end;

    end

    theorem :: FINSEQ_8:4

    

     Th4: for f be FinSequence, k1,k2 be Nat st k1 <= k2 holds ( smid (f,k1,k2)) = ( mid (f,k1,k2))

    proof

      let f be FinSequence, k1,k2 be Nat;

      assume

       A1: k1 <= k2;

      

      then ((k2 -' k1) + 1) = ((k2 - k1) + 1) by XREAL_1: 233

      .= ((k2 + 1) - k1)

      .= ((k2 + 1) -' k1) by A1, NAT_1: 12, XREAL_1: 233;

      hence thesis by A1, FINSEQ_6:def 3;

    end;

    theorem :: FINSEQ_8:5

    

     Th5: for f be FinSequence, k2 be Nat holds ( smid (f,1,k2)) = (f | k2)

    proof

      let f be FinSequence, k2 be Nat;

      

      thus ( smid (f,1,k2)) = ((f /^ 0 ) | ((k2 + 1) -' 1)) by NAT_2: 8

      .= (f | ((k2 + 1) -' 1)) by FINSEQ_5: 28

      .= (f | k2) by NAT_D: 34;

    end;

    theorem :: FINSEQ_8:6

    

     Th6: for f be FinSequence, k2 be Nat st ( len f) <= k2 holds ( smid (f,1,k2)) = f

    proof

      let f be FinSequence, k2 be Nat;

      assume

       A1: ( len f) <= k2;

      

      thus ( smid (f,1,k2)) = (f | k2) by Th5

      .= f by A1, FINSEQ_1: 58;

    end;

    theorem :: FINSEQ_8:7

    

     Th7: for f be FinSequence, k1,k2 be Nat st k1 > k2 holds ( smid (f,k1,k2)) = {}

    proof

      let f be FinSequence, k1,k2 be Nat;

      assume

       A1: k1 > k2;

      set g = (f /^ (k1 -' 1));

      (k2 + 1) <= k1 by A1, NAT_1: 13;

      then ( smid (f,k1,k2)) = (g | 0 ) by NAT_2: 8;

      hence thesis;

    end;

    theorem :: FINSEQ_8:8

    for f be FinSequence, k2 be Nat holds ( smid (f, 0 ,k2)) = ( smid (f,1,(k2 + 1)))

    proof

      let f be FinSequence, k2 be Nat;

      

      thus ( smid (f, 0 ,k2)) = ((f /^ 0 ) | ((k2 + 1) -' 0 )) by NAT_2: 8

      .= (f | ((k2 + 1) -' 0 )) by FINSEQ_5: 28

      .= (f | (k2 + 1)) by NAT_D: 40

      .= (f | (((k2 + 1) + 1) -' 1)) by NAT_D: 34

      .= ((f /^ 0 ) | (((k2 + 1) + 1) -' 1)) by FINSEQ_5: 28

      .= ( smid (f,1,(k2 + 1))) by NAT_2: 8;

    end;

    theorem :: FINSEQ_8:9

    

     Th9: for f,g be FinSequence holds ( smid ((f ^ g),(( len f) + 1),(( len f) + ( len g)))) = g

    proof

      let f,g be FinSequence;

      (((( len g) + ( len f)) + 1) -' (( len f) + 1)) = ((( len g) + (( len f) + 1)) -' (( len f) + 1))

      .= ( len g) by NAT_D: 34;

      then (g | (((( len g) + ( len f)) + 1) -' (( len f) + 1))) = g by FINSEQ_1: 58;

      then (((f ^ g) /^ ( len f)) | (((( len f) + ( len g)) + 1) -' (( len f) + 1))) = g by FINSEQ_5: 37;

      hence thesis by NAT_D: 34;

    end;

    definition

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

      :: FINSEQ_8:def2

      func ovlpart (f,g) -> FinSequence of D means

      : Def2: ( len it ) <= ( len g) & it = ( smid (g,1,( len it ))) & it = ( smid (f,((( len f) -' ( len it )) + 1),( len f))) & for j be Nat st j <= ( len g) & ( smid (g,1,j)) = ( smid (f,((( len f) -' j) + 1),( len f))) holds j <= ( len it );

      existence

      proof

        defpred P[ Nat] means $1 <= ( len g) & ( smid (g,1,$1)) = ( smid (f,((( len f) -' $1) + 1),( len f)));

        

         A1: ( smid (g,1, 0 )) = {} by Th7;

        ((( len f) -' 0 ) + 1) = ((( len f) - 0 ) + 1) by XREAL_1: 233

        .= (( len f) + 1);

        then ( smid (f,((( len f) -' 0 ) + 1),( len f))) = {} by Th7, XREAL_1: 29;

        then

         A2: ex m be Nat st P[m] by A1;

        

         A3: for n be Nat st P[n] holds n <= ( len g);

        consider k be Nat such that

         A4: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A3, A2);

        reconsider k as Element of NAT by ORDINAL1:def 12;

        set b = ( smid (g,1,k));

        now

          per cases ;

            case

             A5: k > 0 ;

            then

             A6: ( 0 + 1) <= k by NAT_1: 13;

            then

             A7: b = ( mid (g,1,k)) by Th4;

            now

              per cases ;

                case ( len g) > 0 ;

                then ( 0 + 1) <= ( len g) by NAT_1: 13;

                

                hence ( len b) = ((k -' 1) + 1) by A4, A6, A7, FINSEQ_6: 118

                .= ((k - 1) + 1) by A6, XREAL_1: 233

                .= k;

              end;

                case ( len g) <= 0 ;

                hence contradiction by A4, A5;

              end;

            end;

            hence ( len b) = k;

          end;

            case

             A8: k <= 0 ;

            then b = {} by Th7;

            hence ( len b) = k by A8;

          end;

        end;

        hence thesis by A4;

      end;

      uniqueness

      proof

        let a,b be FinSequence of D;

        assume that

         A10: ( len a) <= ( len g) and

         A11: a = ( smid (g,1,( len a))) and

         A12: a = ( smid (f,((( len f) -' ( len a)) + 1),( len f))) and

         A13: for j be Nat st j <= ( len g) & ( smid (g,1,j)) = ( smid (f,((( len f) -' j) + 1),( len f))) holds j <= ( len a) and

         A14: ( len b) <= ( len g) and

         A15: b = ( smid (g,1,( len b))) and

         A16: b = ( smid (f,((( len f) -' ( len b)) + 1),( len f))) and

         A17: for j be Nat st j <= ( len g) & ( smid (g,1,j)) = ( smid (f,((( len f) -' j) + 1),( len f))) holds j <= ( len b);

        

         A18: ( len a) <= ( len b) by A10, A11, A12, A17;

        ( len b) <= ( len a) by A13, A14, A15, A16;

        hence thesis by A11, A15, A18, XXREAL_0: 1;

      end;

    end

    theorem :: FINSEQ_8:10

    

     Th10: for D be non empty set, f,g be FinSequence of D holds ( len ( ovlpart (f,g))) <= ( len f)

    proof

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

      now

        assume

         A1: ( len ( ovlpart (f,g))) > ( len f);

        then (( len f) - ( len ( ovlpart (f,g)))) < 0 by XREAL_1: 49;

        then (( len f) -' ( len ( ovlpart (f,g)))) = 0 by XREAL_0:def 2;

        then ( smid (f,((( len f) -' ( len ( ovlpart (f,g)))) + 1),( len f))) = f by Th6;

        hence contradiction by A1, Def2;

      end;

      hence thesis;

    end;

    definition

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

      :: FINSEQ_8:def3

      func ovlcon (f,g) -> FinSequence of D equals (f ^ (g /^ ( len ( ovlpart (f,g)))));

      coherence ;

    end

    theorem :: FINSEQ_8:11

    

     Th11: for D be non empty set, f,g be FinSequence of D holds ( ovlcon (f,g)) = ((f | (( len f) -' ( len ( ovlpart (f,g))))) ^ g)

    proof

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

      

       A1: (( len f) -' ( len ( ovlpart (f,g)))) = (( len f) - ( len ( ovlpart (f,g)))) by Th10, XREAL_1: 233;

      (( len f) + 1) <= ((( len f) + 1) + ( len ( ovlpart (f,g)))) by NAT_1: 12;

      then ((( len f) + 1) - ( len ( ovlpart (f,g)))) <= (((( len f) + 1) + ( len ( ovlpart (f,g)))) - ( len ( ovlpart (f,g)))) by XREAL_1: 9;

      

      then

       A2: ((( len f) + 1) -' ((( len f) -' ( len ( ovlpart (f,g)))) + 1)) = ((( len f) + 1) - ((( len f) -' ( len ( ovlpart (f,g)))) + 1)) by A1, XREAL_1: 233

      .= ( len ( ovlpart (f,g))) by A1;

      (( len f) -' ( len ( ovlpart (f,g)))) <= ( len f) by NAT_D: 35;

      

      then

       A3: ( len (f /^ (( len f) -' ( len ( ovlpart (f,g)))))) = (( len f) - (( len f) -' ( len ( ovlpart (f,g))))) by RFINSEQ:def 1

      .= ( 0 + ( len ( ovlpart (f,g)))) by A1;

      

       A4: ( ovlpart (f,g)) = ( smid (f,((( len f) -' ( len ( ovlpart (f,g)))) + 1),( len f))) by Def2

      .= ((f /^ (( len f) -' ( len ( ovlpart (f,g))))) | ( len ( ovlpart (f,g)))) by A2, NAT_D: 34

      .= (f /^ (( len f) -' ( len ( ovlpart (f,g))))) by A3, FINSEQ_1: 58;

      ( ovlpart (f,g)) = ( smid (g,1,( len ( ovlpart (f,g))))) by Def2

      .= ((g /^ (( 0 + 1) -' 1)) | ( len ( ovlpart (f,g)))) by NAT_D: 34

      .= ((g /^ 0 ) | ( len ( ovlpart (f,g)))) by NAT_D: 34

      .= (g | ( len ( ovlpart (f,g)))) by FINSEQ_5: 28;

      

      hence ( ovlcon (f,g)) = (((f | (( len f) -' ( len ( ovlpart (f,g))))) ^ (g | ( len ( ovlpart (f,g))))) ^ (g /^ ( len ( ovlpart (f,g))))) by A4, RFINSEQ: 8

      .= ((f | (( len f) -' ( len ( ovlpart (f,g))))) ^ ((g | ( len ( ovlpart (f,g)))) ^ (g /^ ( len ( ovlpart (f,g)))))) by FINSEQ_1: 32

      .= ((f | (( len f) -' ( len ( ovlpart (f,g))))) ^ g) by RFINSEQ: 8;

    end;

    definition

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

      :: FINSEQ_8:def4

      func ovlldiff (f,g) -> FinSequence of D equals (f | (( len f) -' ( len ( ovlpart (f,g)))));

      coherence ;

    end

    definition

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

      :: FINSEQ_8:def5

      func ovlrdiff (f,g) -> FinSequence of D equals (g /^ ( len ( ovlpart (f,g))));

      coherence ;

    end

    theorem :: FINSEQ_8:12

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

    proof

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

      (( ovlpart (f,g)) ^ (g /^ ( len ( ovlpart (f,g))))) = (( smid (g,1,( len ( ovlpart (f,g))))) ^ (g /^ ( len ( ovlpart (f,g))))) by Def2

      .= ((g | ( len ( ovlpart (f,g)))) ^ (g /^ ( len ( ovlpart (f,g))))) by Th5

      .= g by RFINSEQ: 8;

      

      hence ( ovlcon (f,g)) = ((f | (( len f) -' ( len ( ovlpart (f,g))))) ^ (( ovlpart (f,g)) ^ (g /^ ( len ( ovlpart (f,g)))))) by Th11

      .= ((( ovlldiff (f,g)) ^ ( ovlpart (f,g))) ^ ( ovlrdiff (f,g))) by FINSEQ_1: 32;

      hence thesis by FINSEQ_1: 32;

    end;

    theorem :: FINSEQ_8:13

    for D be non empty set, f be FinSequence of D holds ( ovlcon (f,f)) = f & ( ovlpart (f,f)) = f & ( ovlldiff (f,f)) = {} & ( ovlrdiff (f,f)) = {}

    proof

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

      

       A1: ( ovlpart (f,f)) = ( smid (f,1,( len ( ovlpart (f,f))))) by Def2;

      ((( len f) -' ( len f)) + 1) = ((( len f) - ( len f)) + 1) by XREAL_1: 233

      .= ( 0 + 1);

      then ( smid (f,1,( len f))) = ( smid (f,((( len f) -' ( len f)) + 1),( len f)));

      then

       A2: ( len f) <= ( len ( ovlpart (f,f))) by Def2;

      

      then

       A3: ( ovlcon (f,f)) = (f ^ ( <*> D)) by Th2

      .= f by FINSEQ_1: 34;

      

       A4: ( ovlldiff (f,f)) = (f | (( len f) -' ( len f))) by A1, A2, Th6

      .= (f | 0 ) by XREAL_1: 232

      .= {} ;

      ( ovlrdiff (f,f)) = {} by A2, Th2;

      hence thesis by A1, A2, A3, A4, Th6;

    end;

    theorem :: FINSEQ_8:14

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

    proof

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

      

       A1: ( len ( ovlpart ((f ^ g),g))) <= ( len g) by Def2;

      

       A2: ( smid (g,1,( len g))) = (g | ( len g)) by Th5

      .= g by FINSEQ_1: 58;

      ((( len (f ^ g)) -' ( len g)) + 1) = (((( len f) + ( len g)) -' ( len g)) + 1) by FINSEQ_1: 22

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

      

      then ( smid ((f ^ g),((( len (f ^ g)) -' ( len g)) + 1),( len (f ^ g)))) = ( smid ((f ^ g),(( len f) + 1),(( len f) + ( len g)))) by FINSEQ_1: 22

      .= g by Th9;

      then ( len g) <= ( len ( ovlpart ((f ^ g),g))) by A2, Def2;

      then

       A3: ( len g) = ( len ( ovlpart ((f ^ g),g))) by A1, XXREAL_0: 1;

      

       A4: ( ovlpart ((f ^ g),g)) = ( smid (g,1,( len ( ovlpart ((f ^ g),g))))) by Def2

      .= (g | ( len g)) by A3, Th5

      .= g by FINSEQ_1: 58;

      

       A5: ( len ( ovlpart (f,(f ^ g)))) <= ( len f) by Th10;

      ((( len f) -' ( len f)) + 1) = ( 0 + 1) by XREAL_1: 232

      .= 1;

      

      then

       A6: ( smid (f,((( len f) -' ( len f)) + 1),( len f))) = ((f /^ (( 0 + 1) -' 1)) | ( len f)) by NAT_D: 34

      .= ((f /^ 0 ) | ( len f)) by NAT_D: 34

      .= (f | ( len f)) by FINSEQ_5: 28

      .= f by FINSEQ_1: 58;

      ( len f) <= (( len f) + ( len g)) by NAT_1: 12;

      then

       A7: ( len f) <= ( len (f ^ g)) by FINSEQ_1: 22;

      ( smid ((f ^ g),1,( len f))) = ((f ^ g) | ( len f)) by Th5

      .= f by FINSEQ_5: 23;

      then ( len f) <= ( len ( ovlpart (f,(f ^ g)))) by A6, A7, Def2;

      then

       A8: ( len f) = ( len ( ovlpart (f,(f ^ g)))) by A5, XXREAL_0: 1;

      ( ovlpart (f,(f ^ g))) = ( smid ((f ^ g),1,( len ( ovlpart (f,(f ^ g)))))) by Def2

      .= ((f ^ g) | ( len f)) by A8, Th5

      .= f by FINSEQ_5: 23;

      hence thesis by A4;

    end;

    theorem :: FINSEQ_8:15

    

     Th15: for D be non empty set, f,g be FinSequence of D holds ( len ( ovlcon (f,g))) = ((( len f) + ( len g)) - ( len ( ovlpart (f,g)))) & ( len ( ovlcon (f,g))) = ((( len f) + ( len g)) -' ( len ( ovlpart (f,g)))) & ( len ( ovlcon (f,g))) = (( len f) + (( len g) -' ( len ( ovlpart (f,g)))))

    proof

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

      

       A1: ( len ( ovlpart (f,g))) <= ( len g) by Def2;

      

       A2: ( len ( ovlcon (f,g))) = (( len f) + ( len (g /^ ( len ( ovlpart (f,g)))))) by FINSEQ_1: 22

      .= (( len f) + (( len g) -' ( len ( ovlpart (f,g))))) by RFINSEQ: 29

      .= (( len f) + (( len g) - ( len ( ovlpart (f,g))))) by A1, XREAL_1: 233;

      hence

       A3: ( len ( ovlcon (f,g))) = ((( len f) + ( len g)) - ( len ( ovlpart (f,g))));

      

       A4: ( len ( ovlpart (f,g))) <= ( len g) by Def2;

      hence ( len ( ovlcon (f,g))) = ((( len f) + ( len g)) -' ( len ( ovlpart (f,g)))) by A3, NAT_1: 12, XREAL_1: 233;

      thus thesis by A2, A4, XREAL_1: 233;

    end;

    theorem :: FINSEQ_8:16

    

     Th16: for D be non empty set, f,g be FinSequence of D holds ( len ( ovlpart (f,g))) <= ( len f) & ( len ( ovlpart (f,g))) <= ( len g)

    proof

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

      now

        assume

         A1: ( len ( ovlpart (f,g))) > ( len f);

        ( ovlpart (f,g)) = ( smid (f,((( len f) -' ( len ( ovlpart (f,g)))) + 1),( len f))) by Def2

        .= ( smid (f,( 0 + 1),( len f))) by A1, NAT_2: 8

        .= f by Th6;

        hence contradiction by A1;

      end;

      hence thesis by Def2;

    end;

    definition

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

      :: FINSEQ_8:def6

      pred CR separates_uniquely means for f be FinSequence of D, i,j be Element of NAT st 1 <= i & i < j & ((j + ( len CR)) -' 1) <= ( len f) & ( smid (f,i,((i + ( len CR)) -' 1))) = ( smid (f,j,((j + ( len CR)) -' 1))) & ( smid (f,i,((i + ( len CR)) -' 1))) = CR holds (j -' i) >= ( len CR);

    end

    theorem :: FINSEQ_8:17

    for D be non empty set, CR be FinSequence of D holds CR separates_uniquely iff ( len ( ovlpart ((CR /^ 1),CR))) = 0

    proof

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

      set p = ( ovlpart ((CR /^ 1),CR));

       A1:

      now

        assume

         A2: CR separates_uniquely ;

        set f = ((CR | 1) ^ ( ovlcon ((CR /^ 1),CR)));

        

         A3: f = (((CR | 1) ^ (CR /^ 1)) ^ (CR /^ ( len ( ovlpart ((CR /^ 1),CR))))) by FINSEQ_1: 32

        .= (CR ^ (CR /^ ( len ( ovlpart ((CR /^ 1),CR))))) by RFINSEQ: 8;

        

         A4: f = ((CR | 1) ^ (((CR /^ 1) | (( len (CR /^ 1)) -' ( len ( ovlpart ((CR /^ 1),CR))))) ^ CR)) by Th11

        .= (((CR | 1) ^ ((CR /^ 1) | (( len (CR /^ 1)) -' ( len ( ovlpart ((CR /^ 1),CR)))))) ^ CR) by FINSEQ_1: 32;

        

         A5: ( len ((CR | 1) ^ ((CR /^ 1) | (( len (CR /^ 1)) -' ( len ( ovlpart ((CR /^ 1),CR))))))) = (( len (CR | 1)) + ( len ((CR /^ 1) | (( len (CR /^ 1)) -' ( len ( ovlpart ((CR /^ 1),CR))))))) by FINSEQ_1: 22

        .= (( len (CR | 1)) + (( len (CR /^ 1)) -' ( len ( ovlpart ((CR /^ 1),CR))))) by FINSEQ_1: 59, NAT_D: 35

        .= (( len (CR | 1)) + (( len (CR /^ 1)) - ( len ( ovlpart ((CR /^ 1),CR))))) by Th16, XREAL_1: 233

        .= ((( len (CR | 1)) + ( len (CR /^ 1))) - ( len ( ovlpart ((CR /^ 1),CR))))

        .= (( len ((CR | 1) ^ (CR /^ 1))) - ( len ( ovlpart ((CR /^ 1),CR)))) by FINSEQ_1: 22

        .= (( len CR) - ( len ( ovlpart ((CR /^ 1),CR)))) by RFINSEQ: 8;

        

         A6: (( len CR) - ( len ( ovlpart ((CR /^ 1),CR)))) = (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR)))) by Th16, XREAL_1: 233;

        

         A7: ((( len CR) + 1) -' 1) = ( len CR) by NAT_D: 34;

        

         A8: ( len ( ovlpart ((CR /^ 1),CR))) <= ( len CR) by Def2;

        

         A9: ( len f) = (( len (CR | 1)) + ( len ( ovlcon ((CR /^ 1),CR)))) by FINSEQ_1: 22

        .= (( len (CR | 1)) + ((( len (CR /^ 1)) + ( len CR)) - ( len ( ovlpart ((CR /^ 1),CR))))) by Th15

        .= ((( len (CR | 1)) + ( len (CR /^ 1))) + (( len CR) - ( len ( ovlpart ((CR /^ 1),CR)))))

        .= (( len ((CR | 1) ^ (CR /^ 1))) + (( len CR) - ( len ( ovlpart ((CR /^ 1),CR))))) by FINSEQ_1: 22

        .= (( len CR) + (( len CR) - ( len ( ovlpart ((CR /^ 1),CR))))) by RFINSEQ: 8;

        set j = ((( len CR) + 1) -' ( len ( ovlpart ((CR /^ 1),CR))));

        

         A10: ( len CR) < (( len CR) + 1) by XREAL_1: 29;

        

         A11: ( len ( ovlpart ((CR /^ 1),CR))) <= ( len CR) by Def2;

        

        then

         A12: j = ((1 + ( len CR)) - ( len ( ovlpart ((CR /^ 1),CR)))) by A10, XREAL_1: 233, XXREAL_0: 2

        .= (1 + (( len CR) - ( len ( ovlpart ((CR /^ 1),CR)))))

        .= (1 + (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR))))) by A11, XREAL_1: 233;

        then

         A13: 1 <= j by NAT_1: 12;

        

         A14: ( smid (f,1,((1 + ( len CR)) -' 1))) = ((f /^ (( 0 + 1) -' 1)) | ((( len CR) + 1) -' 1)) by NAT_D: 34

        .= ((f /^ 0 ) | ( len CR)) by A7, NAT_D: 34

        .= (f | ( len CR)) by FINSEQ_5: 28

        .= CR by A3, FINSEQ_5: 23;

        (((j + ( len CR)) -' 1) + 1) = (((j + ( len CR)) - 1) + 1) by A13, NAT_1: 12, XREAL_1: 233

        .= (j + ( len CR));

        

        then

         A15: ((((j + ( len CR)) -' 1) + 1) -' j) = ((j + ( len CR)) - j) by NAT_1: 12, XREAL_1: 233

        .= ( len CR);

        1 <= (1 + (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR))))) by NAT_1: 12;

        then 1 <= (1 + (( len CR) - ( len ( ovlpart ((CR /^ 1),CR))))) by A8, XREAL_1: 233;

        then 1 <= ((1 + ( len CR)) - ( len ( ovlpart ((CR /^ 1),CR))));

        then 1 <= ((( len CR) + 1) -' ( len ( ovlpart ((CR /^ 1),CR)))) by A8, NAT_1: 12, XREAL_1: 233;

        then (((( len CR) + 1) -' ( len ( ovlpart ((CR /^ 1),CR)))) -' 1) = (((( len CR) + 1) -' ( len ( ovlpart ((CR /^ 1),CR)))) - 1) by XREAL_1: 233;

        

        then (((( len CR) + 1) -' ( len ( ovlpart ((CR /^ 1),CR)))) -' 1) = (((( len CR) + 1) - ( len ( ovlpart ((CR /^ 1),CR)))) - 1) by A8, NAT_1: 12, XREAL_1: 233

        .= (((( len CR) + 1) - 1) - ( len ( ovlpart ((CR /^ 1),CR))))

        .= (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR)))) by A11, XREAL_1: 233;

        

        then

         A16: ( smid (f,j,((j + ( len CR)) -' 1))) = (CR | ( len CR)) by A4, A5, A6, A15, FINSEQ_5: 37

        .= ( smid (f,1,((1 + ( len CR)) -' 1))) by A14, FINSEQ_1: 58;

        ( len ( ovlpart ((CR /^ 1),CR))) <= ( len (CR /^ 1)) by Th10;

        then ( len ( ovlpart ((CR /^ 1),CR))) <= (( len CR) -' 1) by RFINSEQ: 29;

        then

         A17: ((( len CR) + 1) - ( len ( ovlpart ((CR /^ 1),CR)))) >= ((1 + ( len CR)) - (( len CR) -' 1)) by XREAL_1: 10;

        now

          per cases ;

            case ( len CR) >= 1;

            

            then ((1 + ( len CR)) - (( len CR) -' 1)) = ((1 + ( len CR)) - (( len CR) - 1)) by XREAL_1: 233

            .= (1 + 1);

            then 1 < ((( len CR) + 1) - ( len ( ovlpart ((CR /^ 1),CR)))) by A17, XXREAL_0: 2;

            then

             A18: 1 < j by A10, A11, XREAL_1: 233, XXREAL_0: 2;

            ((((( len CR) -' ( len ( ovlpart ((CR /^ 1),CR)))) + ( len CR)) + 1) -' 1) <= (( len CR) + (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR))))) by NAT_D: 34;

            then (((1 + (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR))))) + ( len CR)) -' 1) <= (( len CR) + (( len CR) - ( len ( ovlpart ((CR /^ 1),CR))))) by A11, XREAL_1: 233;

            then

             A19: (j -' 1) >= ( len CR) by A2, A9, A12, A14, A16, A18;

            

             A20: (j -' 1) = ((1 + (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR))))) - 1) by A12, NAT_1: 12, XREAL_1: 233

            .= (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR))));

            

             A21: (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR)))) <= ( len CR) by NAT_D: 35;

            (( len CR) -' ( len ( ovlpart ((CR /^ 1),CR)))) = (( len CR) - ( len ( ovlpart ((CR /^ 1),CR)))) by A11, XREAL_1: 233;

            then (( len CR) - ( len ( ovlpart ((CR /^ 1),CR)))) = ( len CR) by A19, A20, A21, XXREAL_0: 1;

            hence ( len ( ovlpart ((CR /^ 1),CR))) = 0 ;

          end;

            case ( len CR) < 1;

            then ( len CR) < ( 0 + 1);

            then ( len CR) <= 0 by NAT_1: 13;

            hence ( len ( ovlpart ((CR /^ 1),CR))) = 0 by Def2;

          end;

        end;

        hence ( len ( ovlpart ((CR /^ 1),CR))) = 0 ;

      end;

      now

        assume

         A22: ( len ( ovlpart ((CR /^ 1),CR))) = 0 ;

        for f be FinSequence of D, i,j be Element of NAT st 1 <= i & i < j & ((j + ( len CR)) -' 1) <= ( len f) & ( smid (f,i,((i + ( len CR)) -' 1))) = ( smid (f,j,((j + ( len CR)) -' 1))) & ( smid (f,i,((i + ( len CR)) -' 1))) = CR holds (j -' i) >= ( len CR)

        proof

          let f be FinSequence of D, i,j be Element of NAT ;

          assume that

           A23: 1 <= i and

           A24: i < j and

           A25: ((j + ( len CR)) -' 1) <= ( len f) and

           A26: ( smid (f,i,((i + ( len CR)) -' 1))) = ( smid (f,j,((j + ( len CR)) -' 1))) and

           A27: ( smid (f,i,((i + ( len CR)) -' 1))) = CR;

          

           A28: (j - i) > 0 by A24, XREAL_1: 50;

          then

           A29: (j -' i) = (j - i) by XREAL_0:def 2;

          

           A30: (i + (j -' i)) = ((j - i) + i) by A28, XREAL_0:def 2

          .= j;

          now

            per cases ;

              case ( len CR) <= 0 ;

              hence thesis;

            end;

              case

               A31: ( len CR) > 0 ;

              then

               A32: ( 0 + 1) <= ( len CR) by NAT_1: 13;

              then

               A33: (( len CR) -' 1) = (( len CR) - 1) by XREAL_1: 233;

              

               A34: ((i + ( len CR)) -' 1) = ((i + ( len CR)) - 1) by A32, NAT_1: 12, XREAL_1: 233;

              

               A35: i <= (i + (( len CR) -' 1)) by NAT_1: 12;

              then

               A36: 1 <= ((i + ( len CR)) -' 1) by A23, A33, A34, XXREAL_0: 2;

              set k = (j -' i);

              

               A37: ( 0 + 1) <= k by A24, XREAL_1: 50, A29, NAT_1: 13;

              then

               A38: (k - 1) = (k -' 1) by XREAL_1: 233;

              

               A39: (i + (k -' 1)) = (i + (k - 1)) by A37, XREAL_1: 233

              .= (i + ((j - i) - 1)) by A28, XREAL_0:def 2

              .= (j - 1);

              (i + 1) <= j by A24, NAT_1: 13;

              then

               A40: ((i + 1) - 1) <= (j - 1) by XREAL_1: 9;

              then

               A41: (j -' 1) = (j - 1) by XREAL_0:def 2;

              (j - i) > 0 by A24, XREAL_1: 50;

              then (j -' i) > 0 by XREAL_0:def 2;

              then

               A42: (j -' i) >= ( 0 + 1) by NAT_1: 13;

              

               A43: (j -' 1) <= ((j -' 1) + ( len CR)) by NAT_1: 12;

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

              then

               A44: i < (j + ( len CR)) by A24, XXREAL_0: 2;

              ((j -' 1) + ( len CR)) = ((j - 1) + ( len CR)) by A40, XREAL_0:def 2

              .= ((j + ( len CR)) - 1)

              .= ((j + ( len CR)) -' 1) by A23, A44, XREAL_1: 233, XXREAL_0: 2;

              then

               A45: (i + (k -' 1)) <= ( len f) by A25, A39, A41, A43, XXREAL_0: 2;

              now

                assume

                 A46: (j -' i) < ( len CR);

                then (k - 1) < (( len CR) - 1) by XREAL_1: 9;

                then (k -' 1) < (( len CR) - 1) by A42, XREAL_1: 233;

                then (k -' 1) < (( len CR) -' 1) by A32, XREAL_1: 233;

                then

                 A47: ((k -' 1) + 1) <= (( len CR) -' 1) by NAT_1: 13;

                

                 A48: (k - k) < (( len CR) - k) by A46, XREAL_1: 9;

                then 0 < (( len CR) -' k) by XREAL_0:def 2;

                then

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

                

                 A50: (( len CR) -' k) = (( len CR) - k) by A48, XREAL_0:def 2;

                1 < ( len CR) by A37, A46, XXREAL_0: 2;

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

                then

                 A51: ((1 + 1) - 1) <= (( len CR) - 1) by XREAL_1: 9;

                

                 A52: (( len CR) -' 1) = (( len CR) - 1) by A37, A46, XREAL_1: 233, XXREAL_0: 2;

                then

                 A53: (( len CR) -' k) <= (( len CR) -' 1) by A37, A50, XREAL_1: 10;

                i <= (i + (k -' 1)) by NAT_1: 12;

                then

                 A54: i <= ( len f) by A45, XXREAL_0: 2;

                ((j + ( len CR)) -' 1) = ((j + ( len CR)) - 1) by A23, A44, XREAL_1: 233, XXREAL_0: 2

                .= (j + (( len CR) - 1))

                .= (j + (( len CR) -' 1)) by A32, XREAL_1: 233;

                then j <= ((j + ( len CR)) -' 1) by NAT_1: 12;

                then

                 A55: j <= ( len f) by A25, XXREAL_0: 2;

                (i + 1) <= j by A24, NAT_1: 13;

                then ((i + 1) + ( len CR)) <= (j + ( len CR)) by XREAL_1: 7;

                then

                 A56: (((i + 1) + ( len CR)) - 1) <= ((j + ( len CR)) - 1) by XREAL_1: 9;

                

                 A57: 1 < j by A23, A24, XXREAL_0: 2;

                

                 A58: j < (j + ( len CR)) by A31, XREAL_1: 29;

                then

                 A59: 1 < (j + ( len CR)) by A57, XXREAL_0: 2;

                

                 A60: ((j + ( len CR)) -' 1) = ((j + ( len CR)) - 1) by A57, A58, XREAL_1: 233, XXREAL_0: 2;

                then

                 A61: (((i + 1) - 1) + ( len CR)) <= ( len f) by A25, A56, XXREAL_0: 2;

                (i + ( len CR)) <= ((i + ( len CR)) + 1) by NAT_1: 12;

                then ((i + ( len CR)) -' 1) <= (i + ( len CR)) by A34, XREAL_1: 20;

                then

                 A62: ((i + ( len CR)) -' 1) <= ( len f) by A61, XXREAL_0: 2;

                

                 A63: ( 0 + 1) <= ((j + ( len CR)) -' 1) by A60, NAT_1: 13, A59, XREAL_1: 50;

                (j + 1) <= (j + ( len CR)) by A58, NAT_1: 13;

                then

                 A64: ((j + 1) - 1) <= ((j + ( len CR)) - 1) by XREAL_1: 9;

                

                 A65: ( len CR) <= (( len CR) + k) by NAT_1: 12;

                then

                 A66: (( len CR) - k) <= ( len CR) by XREAL_1: 20;

                

                 A67: (( len CR) -' k) <= ( len CR) by A50, A65, XREAL_1: 20;

                

                 A68: ( len ( smid (CR,1,(( len CR) -' k)))) = ( len ( mid (CR,1,(( len CR) -' k)))) by A49, Th4;

                

                 A69: ( len ( mid (CR,1,(( len CR) -' k)))) = (((( len CR) -' k) -' 1) + 1) by A32, A49, A50, A66, FINSEQ_6: 118

                .= (((( len CR) -' k) - 1) + 1) by A49, XREAL_1: 233

                .= (( len CR) -' k);

                

                 A70: ((( len (CR /^ 1)) -' (( len CR) -' k)) + 1) = (((( len CR) -' 1) -' (( len CR) -' k)) + 1) by RFINSEQ: 29

                .= (((( len CR) -' 1) - (( len CR) -' k)) + 1) by A53, XREAL_1: 233

                .= (((( len CR) - 1) - (( len CR) - k)) + 1) by A37, A46, A50, XREAL_1: 233, XXREAL_0: 2

                .= k;

                

                 A71: ( len (CR /^ 1)) = (( len CR) -' 1) by RFINSEQ: 29;

                then

                 A72: ( smid ((CR /^ 1),((( len (CR /^ 1)) -' (( len CR) -' k)) + 1),( len (CR /^ 1)))) = ( mid ((CR /^ 1),k,(( len CR) -' 1))) by A38, A47, A70, Th4;

                

                 A73: ( len ( mid ((CR /^ 1),k,(( len CR) -' 1)))) = (((( len CR) -' 1) -' k) + 1) by A37, A38, A47, A51, A52, A71, FINSEQ_6: 118

                .= (((( len CR) -' 1) - k) + 1) by A38, A47, XREAL_1: 233

                .= (((( len CR) - 1) - k) + 1) by A37, A46, XREAL_1: 233, XXREAL_0: 2

                .= (( len CR) -' k) by A48, XREAL_0:def 2;

                for jj be Nat st 1 <= jj & jj <= (( len CR) -' k) holds (( smid (CR,1,(( len CR) -' k))) . jj) = (( smid ((CR /^ 1),((( len (CR /^ 1)) -' (( len CR) -' k)) + 1),( len (CR /^ 1)))) . jj)

                proof

                  let jj be Nat;

                  assume that

                   A74: 1 <= jj and

                   A75: jj <= (( len CR) -' k);

                  

                   A76: (jj + k) <= ((( len CR) -' k) + k) by A75, XREAL_1: 7;

                  then

                   A77: ((jj + k) - 1) <= (( len CR) - 1) by A50, XREAL_1: 9;

                  reconsider j1 = jj as Element of NAT by ORDINAL1:def 12;

                  

                   A78: ( len ( mid (f,i,((i + ( len CR)) -' 1)))) = ((((i + ( len CR)) -' 1) -' i) + 1) by A23, A33, A34, A35, A36, A54, A62, FINSEQ_6: 118

                  .= ((((i + ( len CR)) - 1) - i) + 1) by A33, A34, A35, XREAL_1: 233

                  .= ( len CR);

                  (( len CR) -' k) <= ( len CR) by NAT_D: 35;

                  then

                   A79: jj <= ( len CR) by A75, XXREAL_0: 2;

                  

                   A80: 1 <= (jj + (k -' 1)) by A74, NAT_1: 12;

                  

                   A81: (jj + (k -' 1)) = (jj + (k - 1)) by A37, XREAL_1: 233

                  .= ((jj + k) - 1)

                  .= ((jj + k) -' 1) by A74, NAT_1: 12, XREAL_1: 233;

                  

                   A82: 1 <= (jj + k) by A74, NAT_1: 12;

                  ((jj + k) -' 1) <= (( len CR) - 1) by A74, A77, NAT_1: 12, XREAL_1: 233;

                  then ((jj + k) -' 1) <= (( len CR) -' 1) by A32, XREAL_1: 233;

                  then ((jj + k) -' 1) in ( Seg ( len (CR /^ 1))) by A71, A80, A81;

                  then

                   A83: ((jj + k) -' 1) in ( dom (CR /^ 1)) by FINSEQ_1:def 3;

                  

                   A84: ( smid (f,j,((j + ( len CR)) -' 1))) = ( mid (f,j,((j + ( len CR)) -' 1))) by A60, A64, Th4;

                  

                  thus (( smid ((CR /^ 1),((( len (CR /^ 1)) -' (( len CR) -' k)) + 1),( len (CR /^ 1)))) . jj) = ((CR /^ 1) . ((j1 + k) -' 1)) by A37, A38, A47, A51, A52, A71, A72, A73, A74, A75, FINSEQ_6: 118

                  .= (( smid (f,i,((i + ( len CR)) -' 1))) . (((jj + k) -' 1) + 1)) by A27, A32, A83, RFINSEQ:def 1

                  .= (( mid (f,i,((i + ( len CR)) -' 1))) . (((jj + k) -' 1) + 1)) by A33, A34, A35, Th4

                  .= (( mid (f,i,((i + ( len CR)) -' 1))) . (((jj + k) - 1) + 1)) by A74, NAT_1: 12, XREAL_1: 233

                  .= (f . ((i + (j1 + k)) -' 1)) by A23, A33, A34, A35, A36, A50, A54, A62, A76, A78, A82, FINSEQ_6: 118

                  .= (f . (((i + k) + j1) -' 1))

                  .= (CR . jj) by A25, A26, A27, A30, A55, A57, A60, A63, A64, A74, A79, A84, FINSEQ_6: 118

                  .= (CR . ((j1 + 1) -' 1)) by NAT_D: 34

                  .= (( mid (CR,1,(( len CR) -' k))) . j1) by A32, A49, A50, A66, A69, A74, A75, FINSEQ_6: 118

                  .= (( smid (CR,1,(( len CR) -' k))) . jj) by A49, Th4;

                end;

                then ( smid (CR,1,(( len CR) -' k))) = ( smid ((CR /^ 1),((( len (CR /^ 1)) -' (( len CR) -' k)) + 1),( len (CR /^ 1)))) by A68, A69, A72, A73;

                then (( len CR) -' k) <= ( len p) by A67, Def2;

                hence contradiction by A22, A48, XREAL_0:def 2;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence CR separates_uniquely ;

      end;

      hence thesis by A1;

    end;

    definition

      let f,g be FinSequence, n be Nat;

      :: FINSEQ_8:def7

      pred g is_substring_of f,n means ( len g) > 0 implies ex i be Nat st n <= i & i <= ( len f) & ( mid (f,i,((i -' 1) + ( len g)))) = g;

    end

    theorem :: FINSEQ_8:18

    for f,g be FinSequence, n,m be Nat st m >= n & g is_substring_of (f,m) holds g is_substring_of (f,n)

    proof

      let f,g be FinSequence, n,m be Nat;

      assume that

       A1: m >= n and

       A2: g is_substring_of (f,m);

      now

        per cases ;

          case ( len g) > 0 ;

          then

          consider i be Nat such that

           A3: m <= i and

           A4: i <= ( len f) and

           A5: ( mid (f,i,((i -' 1) + ( len g)))) = g by A2;

          n <= i by A1, A3, XXREAL_0: 2;

          hence thesis by A4, A5;

        end;

          case ( len g) <= 0 ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINSEQ_8:19

    

     Th19: for f be FinSequence st 1 <= ( len f) holds f is_substring_of (f,1)

    proof

      let f be FinSequence;

      assume

       A1: 1 <= ( len f);

      ((1 -' 1) + ( len f)) = ( 0 + ( len f)) by NAT_2: 8

      .= ( len f);

      then ( mid (f,1,((1 -' 1) + ( len f)))) = f by A1, FINSEQ_6: 120;

      hence thesis by A1;

    end;

    theorem :: FINSEQ_8:20

    

     Th20: for f,g be FinSequence st g is_substring_of (f, 0 ) holds g is_substring_of (f,1)

    proof

      let f,g be FinSequence;

      assume

       A1: g is_substring_of (f, 0 );

      now

        per cases ;

          case

           A2: ( len g) > 0 ;

          then

          consider i be Nat such that 0 <= i and

           A3: i <= ( len f) and

           A4: ( mid (f,i,((i -' 1) + ( len g)))) = g by A1;

          

           A5: ( len g) >= ( 0 + 1) by A2, NAT_1: 13;

          now

            per cases ;

              case

               A6: i = 0 ;

              ( 0 - 1) < 0 ;

              then

               A7: (i -' 1) = 0 by A6, XREAL_0:def 2;

              then

               A8: ((f /^ ( 0 -' 1)) | ((( len g) -' 0 ) + 1)) = g by A4, A6, FINSEQ_6:def 3;

              (( len g) -' 0 ) = (( len g) - 0 ) by XREAL_0:def 2

              .= ( len g);

              then

               A9: (f | (( len g) + 1)) = g by A6, A7, A8, FINSEQ_5: 28;

              now

                per cases ;

                  case (( len g) + 1) >= ( len f);

                  then f = g by A9, FINSEQ_1: 58;

                  hence thesis by A5, Th19;

                end;

                  case

                   A10: (( len g) + 1) < ( len f);

                  ( dom (f | ( Seg (( len g) + 1)))) = (( dom f) /\ ( Seg (( len g) + 1))) by RELAT_1: 61

                  .= (( Seg ( len f)) /\ ( Seg (( len g) + 1))) by FINSEQ_1:def 3

                  .= ( Seg (( len g) + 1)) by A10, FINSEQ_1: 7;

                  then ( len g) = (( len g) + 1) by A9, FINSEQ_1:def 3;

                  hence contradiction;

                end;

              end;

              hence thesis;

            end;

              case i <> 0 ;

              then i >= ( 0 + 1) by NAT_1: 13;

              hence thesis by A3, A4;

            end;

          end;

          hence thesis;

        end;

          case ( len g) <= 0 ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    notation

      let g,f be FinSequence;

      synonym g is_preposition_of f for g c= f;

    end

    definition

      let g,f be FinSequence;

      :: original: c=

      redefine

      :: FINSEQ_8:def8

      pred g c= f means ( len g) > 0 implies 1 <= ( len f) & ( mid (f,1,( len g))) = g;

      compatibility

      proof

        thus g c= f implies (( len g) > 0 implies 1 <= ( len f) & ( mid (f,1,( len g))) = g)

        proof

          assume that

           A1: g c= f and

           A2: ( len g) > 0 ;

          

           A3: ( 0 + 1) <= ( len g) by A2, NAT_1: 13;

          ( len g) <= ( len f) by A1, FINSEQ_1: 63;

          hence 1 <= ( len f) by A3, XXREAL_0: 2;

          

          thus ( mid (f,1,( len g))) = ((f /^ (1 -' 1)) | ((( len g) -' 1) + 1)) by A3, FINSEQ_6:def 3

          .= ((f /^ (1 -' 1)) | ( len g)) by A3, XREAL_1: 235

          .= ((f /^ 0 ) | ( len g)) by XREAL_1: 232

          .= (f | ( len g)) by FINSEQ_5: 28

          .= g by A1, FINSEQ_3: 113;

        end;

        assume

         A4: ( len g) > 0 implies 1 <= ( len f) & ( mid (f,1,( len g))) = g;

        per cases by A4;

          suppose ( len g) <= 0 ;

          then g = {} ;

          hence thesis by XBOOLE_1: 2;

        end;

          suppose that

           A5: ( len g) > 0 and

           A6: ( mid (f,1,( len g))) = g;

          ( 0 + 1) <= ( len g) by A5, NAT_1: 13;

          then g = (f | ( len g)) by A6, FINSEQ_6: 116;

          hence thesis by RELAT_1: 59;

        end;

      end;

    end

    theorem :: FINSEQ_8:21

    for f,g be FinSequence st ( len g) > 0 & g is_preposition_of f holds (g . 1) = (f . 1)

    proof

      let f,g be FinSequence;

      assume that

       A1: ( len g) > 0 and

       A2: g is_preposition_of f;

      

       A4: ( len g) <= ( len f) by A2, FINSEQ_1: 63;

      ( 0 + 1) <= ( len g) by A1, NAT_1: 13;

      hence thesis by A2, A4, FINSEQ_6: 123;

    end;

    definition

      let f,g be FinSequence;

      :: FINSEQ_8:def9

      pred g is_postposition_of f means ( Rev g) is_preposition_of ( Rev f);

      correctness ;

    end

    theorem :: FINSEQ_8:22

    

     Th22: for f,g be FinSequence st ( len g) = 0 holds g is_postposition_of f

    proof

      let f,g be FinSequence;

      assume ( len g) = 0 ;

      then ( Rev g) is_preposition_of ( Rev f) by FINSEQ_5:def 3;

      hence thesis;

    end;

    theorem :: FINSEQ_8:23

    

     Th23: for D be non empty set, f,g be FinSequence of D st g is_postposition_of f holds ( len g) <= ( len f)

    proof

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

      assume

       a1: g is_postposition_of f;

      

       A2: ( len ( Rev g)) = ( len g) by FINSEQ_5:def 3;

      ( len ( Rev f)) = ( len f) by FINSEQ_5:def 3;

      hence thesis by a1, A2, FINSEQ_1: 63;

    end;

    theorem :: FINSEQ_8:24

    for D be non empty set, f,g be FinSequence of D st g is_postposition_of f holds ( len g) > 0 implies ( len g) <= ( len f) & ( mid (f,((( len f) + 1) -' ( len g)),( len f))) = g

    proof

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

      assume

       A1: g is_postposition_of f;

      then

       A2: ( Rev g) is_preposition_of ( Rev f);

      then

       A3: ( len ( Rev g)) > 0 implies 1 <= ( len ( Rev f)) & ( mid (( Rev f),1,( len ( Rev g)))) = ( Rev g);

      

       A5: ( len ( Rev f)) = ( len f) by FINSEQ_5:def 3;

      now

        assume

         A6: ( len g) > 0 ;

        then

         A7: 1 <= ( len f) by A2, FINSEQ_5:def 3;

        

         A8: ( mid (( Rev f),1,( len g))) = ( Rev g) by A2, FINSEQ_5:def 3, A6;

        

         A9: (( len f) - 1) >= 0 by A3, A5, A6, FINSEQ_5:def 3, XREAL_1: 48;

        

         A10: ( len g) <= ( len f) by A1, Th23;

        

         A11: (( len f) - ( len g)) >= 0 by A1, Th23, XREAL_1: 48;

        ( len f) < (( len f) + 1) by XREAL_1: 29;

        then ( len g) < (( len f) + 1) by A10, XXREAL_0: 2;

        then

         A12: ((( len f) + 1) - ( len g)) > 0 by XREAL_1: 50;

        

         A13: ( 0 + 1) <= ( len g) by A6, NAT_1: 13;

        

         A14: g = ( Rev ( Rev g))

        .= ( mid (( Rev ( Rev f)),((( len f) -' ( len g)) + 1),((( len f) -' 1) + 1))) by A5, A7, A8, A10, A13, FINSEQ_6: 113

        .= ( mid (f,((( len f) -' ( len g)) + 1),((( len f) -' 1) + 1)));

        

         A15: ((( len f) -' ( len g)) + 1) = ((( len f) - ( len g)) + 1) by A11, XREAL_0:def 2

        .= ((( len f) + 1) -' ( len g)) by A12, XREAL_0:def 2;

        ((( len f) -' 1) + 1) = ((( len f) - 1) + 1) by A9, XREAL_0:def 2

        .= ( len f);

        hence ( len g) <= ( len f) & ( mid (f,((( len f) + 1) -' ( len g)),( len f))) = g by A1, A14, A15, Th23;

      end;

      hence thesis;

    end;

    theorem :: FINSEQ_8:25

    for D be non empty set, f,g be FinSequence of D st (( len g) > 0 implies ( len g) <= ( len f) & ( mid (f,((( len f) + 1) -' ( len g)),( len f))) = g) holds g is_postposition_of f

    proof

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

      assume

       A1: ( len g) > 0 implies ( len g) <= ( len f) & ( mid (f,((( len f) + 1) -' ( len g)),( len f))) = g;

      

       A2: ( len ( Rev f)) = ( len f) by FINSEQ_5:def 3;

      now

        per cases ;

          case

           A3: ( len g) > 0 ;

          then

           A4: ( 0 + 1) <= ( len g) by NAT_1: 13;

          then

           A5: (( len g) - 1) >= 0 by XREAL_1: 48;

          ( len f) < (( len f) + 1) by XREAL_1: 29;

          then

           a6: ( len g) < (( len f) + 1) by A1, XXREAL_0: 2;

          then

           A6: ((( len f) + 1) - ( len g)) > 0 by XREAL_1: 50;

          then ((( len f) + 1) -' ( len g)) = ((( len f) + 1) - ( len g)) by XREAL_0:def 2;

          then

           A7: ( 0 + 1) <= ((( len f) + 1) -' ( len g)) by a6, NAT_1: 13, XREAL_1: 50;

          

           A8: ((( len f) + 1) -' ( len g)) = (( len f) - (( len g) - 1)) by A6, XREAL_0:def 2;

          (( len f) + 0 ) <= (( len f) + (( len g) - 1)) by A5, XREAL_1: 7;

          then

           A9: (( len f) - (( len g) - 1)) <= ( len f) by XREAL_1: 20;

          

           A10: 1 <= ( len f) by A1, A4, XXREAL_0: 2;

          

           A11: ((( len f) -' ( len f)) + 1) = ((( len f) - ( len f)) + 1) by XREAL_0:def 2

          .= 1;

          ( len f) < (( len f) + 1) by XREAL_1: 29;

          then ( len g) <= (( len f) + 1) by A1, XXREAL_0: 2;

          

          then

           A12: (( len f) - ((( len f) + 1) -' ( len g))) = (( len f) - ((( len f) + 1) - ( len g))) by XREAL_0:def 2, XREAL_1: 48

          .= (( len g) - 1);

          then

           A13: ((( len f) -' ((( len f) + 1) -' ( len g))) + 1) = ((( len f) - ((( len f) + 1) -' ( len g))) + 1) by A5, XREAL_0:def 2;

          ( Rev g) = ( mid (( Rev f),((( len f) -' ( len f)) + 1),((( len f) -' ((( len f) + 1) -' ( len g))) + 1))) by A1, A3, A7, A8, A9, A10, FINSEQ_6: 113

          .= ( mid (( Rev f),1,( len ( Rev g)))) by A11, A12, A13, FINSEQ_5:def 3;

          then ( Rev g) is_preposition_of ( Rev f) by A1, A2, A4, XXREAL_0: 2;

          hence thesis;

        end;

          case ( len g) <= 0 ;

          then ( len g) = 0 ;

          hence thesis by Th22;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINSEQ_8:26

    for f,g be FinSequence st 1 <= ( len f) & g is_preposition_of f holds g is_substring_of (f,1)

    proof

      let f,g be FinSequence;

      assume that

       A1: 1 <= ( len f) and

       A2: g is_preposition_of f;

      now

        per cases ;

          case

           A3: ( len g) > 0 ;

          ( mid (f,1,((1 -' 1) + ( len g)))) = ( mid (f,1,( 0 + ( len g)))) by NAT_2: 8

          .= g by A2, A3;

          hence thesis by A1;

        end;

          case ( len g) <= 0 ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINSEQ_8:27

    

     Th27: for D be non empty set, f,g be FinSequence of D, n be Nat st not g is_substring_of (f,n) holds for i be Element of NAT st n <= i & 0 < i holds ( mid (f,i,((i -' 1) + ( len g)))) <> g

    proof

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

      assume

       A1: not g is_substring_of (f,n);

      now

        let i be Element of NAT ;

        assume that

         A2: n <= i and

         A3: 0 < i;

        now

          per cases ;

            case i <= ( len f);

            hence ( mid (f,i,((i -' 1) + ( len g)))) <> g by A1, A2;

          end;

            case

             A4: i > ( len f);

            now

              per cases ;

                case

                 A5: i <= ((i -' 1) + ( len g));

                then

                 A6: ( mid (f,i,((i -' 1) + ( len g)))) = ((f /^ (i -' 1)) | ((((i -' 1) + ( len g)) -' i) + 1)) by FINSEQ_6:def 3;

                now

                  per cases ;

                    case

                     A7: (i -' 1) <= ( len f);

                    i >= (( len f) + 1) by A4, NAT_1: 13;

                    then

                     A8: (i - 1) >= ((( len f) + 1) - 1) by XREAL_1: 9;

                    ( 0 + 1) <= i by A3, NAT_1: 13;

                    then (i -' 1) = (i - 1) by XREAL_0:def 2, XREAL_1: 48;

                    then

                     A9: (i -' 1) = ( len f) by A7, A8, XXREAL_0: 1;

                    ( len (f /^ (i -' 1))) = (( len f) - (i -' 1)) by A7, RFINSEQ:def 1;

                    hence ( len (f /^ (i -' 1))) = 0 by A9;

                  end;

                    case (i -' 1) > ( len f);

                    then (f /^ (i -' 1)) = ( <*> D) by RFINSEQ:def 1;

                    hence ( len (f /^ (i -' 1))) = 0 ;

                  end;

                end;

                then

                 A10: ((f /^ (i -' 1)) | ((((i -' 1) + ( len g)) -' i) + 1)) = ( <*> D) by FINSEQ_1: 58;

                now

                  assume

                   A11: ( mid (f,i,((i -' 1) + ( len g)))) = g;

                  

                   a12: ( 0 + 1) <= i by A3, NAT_1: 13;

                  (i - 1) < ((i + 1) - 1) by XREAL_1: 9, XREAL_1: 29;

                  hence contradiction by A5, A6, A10, A11, a12, XREAL_0:def 2;

                end;

                hence ( mid (f,i,((i -' 1) + ( len g)))) <> g;

              end;

                case

                 A13: i > ((i -' 1) + ( len g));

                now

                  assume ( len g) > 0 ;

                  then ( len g) >= ( 0 + 1) by NAT_1: 13;

                  then

                   A14: ((i -' 1) + ( len g)) >= ((i -' 1) + 1) by XREAL_1: 7;

                  ( 0 + 1) <= i by A3, NAT_1: 13;

                  then (i -' 1) = (i - 1) by XREAL_0:def 2, XREAL_1: 48;

                  hence contradiction by A13, A14;

                end;

                hence contradiction by A1;

              end;

            end;

            hence ( mid (f,i,((i -' 1) + ( len g)))) <> g;

          end;

        end;

        hence ( mid (f,i,((i -' 1) + ( len g)))) <> g;

      end;

      hence thesis;

    end;

    definition

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

      :: FINSEQ_8:def10

      func instr (n,f,g) -> Element of NAT means

      : Def10: (it <> 0 implies n <= it & g is_preposition_of (f /^ (it -' 1)) & for j be Element of NAT st j >= n & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= it ) & (it = 0 implies not g is_substring_of (f,n));

      existence

      proof

        

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

        now

          per cases ;

            case

             A2: g is_substring_of (f,n);

            now

              per cases ;

                case

                 A3: ( len g) > 0 ;

                

                 A5: ( 0 + 1) <= ( len g) by A3, NAT_1: 13;

                now

                  per cases ;

                    case

                     A6: n > 0 ;

                    defpred P[ Nat] means n <= $1 & $1 <= ( len f) & ( mid (f,$1,(($1 -' 1) + ( len g)))) = g;

                    

                     A7: ex i be Nat st P[i] by A2, A3;

                    ex k be Nat st P[k] & for m be Nat st P[m] holds m >= k from NAT_1:sch 5( A7);

                    then

                    consider k0 be Nat such that

                     A8: n <= k0 and

                     A9: k0 <= ( len f) and

                     A10: ( mid (f,k0,((k0 -' 1) + ( len g)))) = g and

                     A11: for m be Nat st n <= m & m <= ( len f) & ( mid (f,m,((m -' 1) + ( len g)))) = g holds m >= k0;

                    reconsider k0 as Element of NAT by ORDINAL1:def 12;

                    ( 0 + 1) <= k0 by A6, A8, NAT_1: 13;

                    then

                     A12: (k0 -' 1) = (k0 - 1) by XREAL_0:def 2, XREAL_1: 48;

                    (k0 - 1) < ((k0 + 1) - 1) by XREAL_1: 9, XREAL_1: 29;

                    then (k0 -' 1) < ( len f) by A9, A12, XXREAL_0: 2;

                    then

                     A13: ( len (f /^ (k0 -' 1))) = (( len f) - (k0 -' 1)) by RFINSEQ:def 1;

                    (( len f) - k0) >= 0 by A9, XREAL_1: 48;

                    then

                     A14: ((( len f) - k0) + 1) >= ( 0 + 1) by XREAL_1: 7;

                    

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

                    

                     A16: ( 0 + 1) <= ( len g) by A3, NAT_1: 13;

                    then

                     A17: ((k0 -' 1) + 1) <= ((k0 -' 1) + ( len g)) by XREAL_1: 7;

                    

                     A18: (( len g) - 1) >= 0 by A16, XREAL_1: 48;

                    then (((( - 1) + ( len g)) + k0) - k0) >= 0 ;

                    

                    then

                     A19: ((((k0 -' 1) + ( len g)) -' k0) + 1) = ((( len g) - 1) + 1) by A12, XREAL_0:def 2

                    .= ((( len g) -' 1) + 1) by A18, XREAL_0:def 2;

                    ( mid ((f /^ (k0 -' 1)),1,( len g))) = (((f /^ (k0 -' 1)) /^ (1 -' 1)) | ((( len g) -' 1) + 1)) by A5, FINSEQ_6:def 3

                    .= ((f /^ (k0 -' 1)) | ((((k0 -' 1) + ( len g)) -' k0) + 1)) by A15, A19, FINSEQ_5: 28

                    .= ( mid (f,k0,((k0 -' 1) + ( len g)))) by A12, A17, FINSEQ_6:def 3;

                    then

                     A20: g is_preposition_of (f /^ (k0 -' 1)) by A10, A12, A13, A14;

                    for j be Element of NAT st j >= n & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= k0

                    proof

                      let j be Element of NAT ;

                      assume that

                       A21: j >= n and

                       A22: j > 0 and

                       A23: g is_preposition_of (f /^ (j -' 1));

                      

                       A24: ( mid ((f /^ (j -' 1)),1,( len g))) = g by A3, A23;

                      now

                        per cases ;

                          case

                           A25: j <= ( len f);

                          ( 0 + 1) <= j by A22, NAT_1: 13;

                          then

                           A26: (j -' 1) = (j - 1) by XREAL_0:def 2, XREAL_1: 48;

                          (((( - 1) + ( len g)) + j) - j) >= 0 by A18;

                          

                          then

                           A27: ((((j -' 1) + ( len g)) -' j) + 1) = ((( len g) - 1) + 1) by A26, XREAL_0:def 2

                          .= ((( len g) -' 1) + 1) by A18, XREAL_0:def 2;

                          

                           A28: ((j -' 1) + 1) <= ((j -' 1) + ( len g)) by A16, XREAL_1: 7;

                          ( mid ((f /^ (j -' 1)),1,( len g))) = (((f /^ (j -' 1)) /^ (1 -' 1)) | ((( len g) -' 1) + 1)) by A5, FINSEQ_6:def 3

                          .= ((f /^ (j -' 1)) | ((((j -' 1) + ( len g)) -' j) + 1)) by A15, A27, FINSEQ_5: 28

                          .= ( mid (f,j,((j -' 1) + ( len g)))) by A26, A28, FINSEQ_6:def 3;

                          hence thesis by A11, A21, A24, A25;

                        end;

                          case j > ( len f);

                          hence thesis by A9, XXREAL_0: 2;

                        end;

                      end;

                      hence thesis;

                    end;

                    hence thesis by A6, A8, A20;

                  end;

                    case

                     A29: n = 0 ;

                    then

                     A30: g is_substring_of (f,1) by A2, Th20;

                    reconsider n2 = 1 as Element of NAT ;

                    defpred P[ Nat] means n2 <= $1 & $1 <= ( len f) & ( mid (f,$1,(($1 -' 1) + ( len g)))) = g;

                    

                     A32: ex i be Nat st P[i] by A3, A30;

                    ex k be Nat st P[k] & for m be Nat st P[m] holds m >= k from NAT_1:sch 5( A32);

                    then

                    consider k0 be Nat such that

                     A33: n2 <= k0 and

                     A34: k0 <= ( len f) and

                     A35: ( mid (f,k0,((k0 -' 1) + ( len g)))) = g and

                     A36: for m be Nat st n2 <= m & m <= ( len f) & ( mid (f,m,((m -' 1) + ( len g)))) = g holds m >= k0;

                    reconsider k0 as Element of NAT by ORDINAL1:def 12;

                    

                     A37: (k0 -' 1) = (k0 - 1) by XREAL_0:def 2, A33, XREAL_1: 48;

                    (k0 - 1) < ((k0 + 1) - 1) by XREAL_1: 9, XREAL_1: 29;

                    then (k0 -' 1) < ( len f) by A34, A37, XXREAL_0: 2;

                    then

                     A38: ( len (f /^ (k0 -' 1))) = (( len f) - (k0 -' 1)) by RFINSEQ:def 1;

                    (( len f) - k0) >= 0 by A34, XREAL_1: 48;

                    then

                     A39: ((( len f) - k0) + 1) >= ( 0 + 1) by XREAL_1: 7;

                    

                     A40: ( 0 + 1) <= ( len g) by A3, NAT_1: 13;

                    then

                     A41: ((k0 -' 1) + 1) <= ((k0 -' 1) + ( len g)) by XREAL_1: 7;

                    

                     A42: (( len g) - 1) >= 0 by A40, XREAL_1: 48;

                    then (((( - 1) + ( len g)) + k0) - k0) >= 0 ;

                    

                    then

                     A43: ((((k0 -' 1) + ( len g)) -' k0) + 1) = ((( len g) - 1) + 1) by A37, XREAL_0:def 2

                    .= ((( len g) -' 1) + 1) by A42, XREAL_0:def 2;

                    ( mid ((f /^ (k0 -' 1)),1,( len g))) = (((f /^ (k0 -' 1)) /^ (1 -' 1)) | ((( len g) -' 1) + 1)) by A5, FINSEQ_6:def 3

                    .= ((f /^ (k0 -' 1)) | ((((k0 -' 1) + ( len g)) -' k0) + 1)) by A1, A43, FINSEQ_5: 28

                    .= ( mid (f,k0,((k0 -' 1) + ( len g)))) by A37, A41, FINSEQ_6:def 3;

                    then

                     A44: g is_preposition_of (f /^ (k0 -' 1)) by A35, A37, A38, A39;

                    

                     A45: for j be Element of NAT st j >= n2 & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= k0

                    proof

                      let j be Element of NAT ;

                      assume that

                       A46: j >= n2 and j > 0 and

                       A47: g is_preposition_of (f /^ (j -' 1));

                      

                       A48: ( mid ((f /^ (j -' 1)),1,( len g))) = g by A3, A47;

                      now

                        per cases ;

                          case

                           A49: j <= ( len f);

                          

                           A50: (j -' 1) = (j - 1) by XREAL_0:def 2, A46, XREAL_1: 48;

                          (((( - 1) + ( len g)) + j) - j) >= 0 by A42;

                          

                          then

                           A51: ((((j -' 1) + ( len g)) -' j) + 1) = ((( len g) - 1) + 1) by A50, XREAL_0:def 2

                          .= ((( len g) -' 1) + 1) by A42, XREAL_0:def 2;

                          

                           A52: ((j -' 1) + 1) <= ((j -' 1) + ( len g)) by A40, XREAL_1: 7;

                          ( mid ((f /^ (j -' 1)),1,( len g))) = (((f /^ (j -' 1)) /^ (1 -' 1)) | ((( len g) -' 1) + 1)) by A5, FINSEQ_6:def 3

                          .= ((f /^ (j -' 1)) | ((((j -' 1) + ( len g)) -' j) + 1)) by A1, A51, FINSEQ_5: 28

                          .= ( mid (f,j,((j -' 1) + ( len g)))) by A50, A52, FINSEQ_6:def 3;

                          hence thesis by A36, A46, A48, A49;

                        end;

                          case j > ( len f);

                          hence thesis by A34, XXREAL_0: 2;

                        end;

                      end;

                      hence thesis;

                    end;

                    for j be Element of NAT st j >= n & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= k0

                    proof

                      let j be Element of NAT ;

                      assume that j >= n and

                       A53: j > 0 and

                       A54: g is_preposition_of (f /^ (j -' 1));

                      j >= ( 0 + n2) by A53, NAT_1: 13;

                      hence thesis by A45, A54;

                    end;

                    hence thesis by A29, A33, A44;

                  end;

                end;

                hence thesis;

              end;

                case

                 A55: ( len g) <= 0 ;

                reconsider nn = ( max (n,1)) as Element of NAT by ORDINAL1:def 12;

                

                 A56: nn >= n by XXREAL_0: 25;

                

                 A57: nn >= ( 0 + 1) by XXREAL_0: 25;

                

                 A58: g is_preposition_of (f /^ (nn -' 1)) by A55;

                for j be Element of NAT st j >= n & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= nn

                proof

                  let j be Element of NAT ;

                  assume that

                   A59: j >= n and

                   A60: j > 0 and g is_preposition_of (f /^ (j -' 1));

                  j >= ( 0 + 1) by A60, NAT_1: 13;

                  hence thesis by A59, XXREAL_0: 28;

                end;

                hence thesis by A56, A57, A58;

              end;

            end;

            hence thesis;

          end;

            case not g is_substring_of (f,n);

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        

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

        thus for k1,k2 be Element of NAT st (k1 <> 0 implies n <= k1 & g is_preposition_of (f /^ (k1 -' 1)) & for j be Element of NAT st j >= n & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= k1) & (k1 = 0 implies not g is_substring_of (f,n)) & (k2 <> 0 implies n <= k2 & g is_preposition_of (f /^ (k2 -' 1)) & for j be Element of NAT st j >= n & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= k2) & (k2 = 0 implies not g is_substring_of (f,n)) holds k1 = k2

        proof

          let k1,k2 be Element of NAT ;

          assume that

           A62: k1 <> 0 implies n <= k1 & g is_preposition_of (f /^ (k1 -' 1)) & for j be Element of NAT st j >= n & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= k1 and

           A63: k1 = 0 implies not g is_substring_of (f,n) and

           A64: k2 <> 0 implies n <= k2 & g is_preposition_of (f /^ (k2 -' 1)) & for j be Element of NAT st j >= n & j > 0 & g is_preposition_of (f /^ (j -' 1)) holds j >= k2 and

           A65: k2 = 0 implies not g is_substring_of (f,n);

          now

            per cases ;

              case ( len g) > 0 ;

              then

               A66: ( 0 + 1) <= ( len g) by NAT_1: 13;

              then

               A67: (( len g) - 1) >= 0 by XREAL_1: 48;

              now

                per cases ;

                  case

                   A68: k1 <> 0 & k2 <> 0 ;

                  then

                   A69: k2 >= k1 by A62, A64;

                  k1 >= k2 by A62, A64, A68;

                  hence thesis by A69, XXREAL_0: 1;

                end;

                  case

                   A70: k1 <> 0 & k2 = 0 ;

                  for i be Element of NAT st n <= i & 0 < i holds not g is_preposition_of (f /^ (i -' 1))

                  proof

                    let i be Element of NAT ;

                    assume that

                     A72: n <= i and

                     A73: 0 < i;

                    ( 0 + 1) <= i by A73, NAT_1: 13;

                    then

                     A74: (i -' 1) = (i - 1) by XREAL_0:def 2, XREAL_1: 48;

                    (((( - 1) + ( len g)) + i) - i) >= 0 by A67;

                    

                    then

                     A75: ((((i -' 1) + ( len g)) -' i) + 1) = ((( len g) - 1) + 1) by A74, XREAL_0:def 2

                    .= ((( len g) -' 1) + 1) by A67, XREAL_0:def 2;

                    

                     A76: ((i -' 1) + 1) <= ((i -' 1) + ( len g)) by A66, XREAL_1: 7;

                    ( mid ((f /^ (i -' 1)),1,( len g))) = (((f /^ (i -' 1)) /^ (1 -' 1)) | ((( len g) -' 1) + 1)) by A66, FINSEQ_6:def 3

                    .= ((f /^ (i -' 1)) | ((((i -' 1) + ( len g)) -' i) + 1)) by A61, A75, FINSEQ_5: 28

                    .= ( mid (f,i,((i -' 1) + ( len g)))) by A74, A76, FINSEQ_6:def 3;

                    hence thesis by A65, A70, A72, A73, Th27;

                  end;

                  hence contradiction by A62, A70;

                end;

                  case

                   A77: k1 = 0 & k2 <> 0 ;

                  for i be Element of NAT st n <= i & 0 < i holds not g is_preposition_of (f /^ (i -' 1))

                  proof

                    let i be Element of NAT ;

                    assume that

                     A79: n <= i and

                     A80: 0 < i;

                    ( 0 + 1) <= i by A80, NAT_1: 13;

                    then

                     A81: (i -' 1) = (i - 1) by XREAL_0:def 2, XREAL_1: 48;

                    (((( - 1) + ( len g)) + i) - i) >= 0 by A67;

                    

                    then

                     A82: ((((i -' 1) + ( len g)) -' i) + 1) = ((( len g) - 1) + 1) by A81, XREAL_0:def 2

                    .= ((( len g) -' 1) + 1) by A67, XREAL_0:def 2;

                    

                     A83: ((i -' 1) + 1) <= ((i -' 1) + ( len g)) by A66, XREAL_1: 7;

                    ( mid ((f /^ (i -' 1)),1,( len g))) = (((f /^ (i -' 1)) /^ (1 -' 1)) | ((( len g) -' 1) + 1)) by A66, FINSEQ_6:def 3

                    .= ((f /^ (i -' 1)) | ((((i -' 1) + ( len g)) -' i) + 1)) by A61, A82, FINSEQ_5: 28

                    .= ( mid (f,i,((i -' 1) + ( len g)))) by A81, A83, FINSEQ_6:def 3;

                    hence thesis by A63, A77, A79, A80, Th27;

                  end;

                  hence contradiction by A64, A77;

                end;

                  case k1 = 0 & k2 = 0 ;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

              case

               A84: ( len g) <= 0 ;

              now

                per cases ;

                  case

                   A85: k1 <> 0 & k2 <> 0 ;

                  then

                   A86: k2 >= k1 by A62, A64;

                  k1 >= k2 by A62, A64, A85;

                  hence thesis by A86, XXREAL_0: 1;

                end;

                  case k1 <> 0 & k2 = 0 ;

                  hence contradiction by A65, A84;

                end;

                  case k1 = 0 & k2 <> 0 ;

                  hence contradiction by A63, A84;

                end;

                  case k1 = 0 & k2 = 0 ;

                  hence contradiction by A63, A84;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    definition

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

      :: FINSEQ_8:def11

      func addcr (f,CR) -> FinSequence of D equals ( ovlcon (f,CR));

      correctness ;

    end

    definition

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

      :: FINSEQ_8:def12

      pred r is_terminated_by CR means ( len CR) > 0 implies ( len r) >= ( len CR) & ( instr (1,r,CR)) = ((( len r) + 1) -' ( len CR));

      correctness ;

    end

    theorem :: FINSEQ_8:28

    for D be non empty set, f be FinSequence of D holds f is_terminated_by f

    proof

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

      

       A1: ((( len f) + 1) -' ( len f)) = ((( len f) + 1) - ( len f)) by XREAL_0:def 2;

      (1 -' 1) = (( 0 + 1) -' 1)

      .= 0 by NAT_D: 34;

      then

       A2: (f /^ (1 -' 1)) = f by FINSEQ_5: 28;

      for j be Element of NAT st j >= 1 & j > 0 & f is_preposition_of (f /^ (j -' 1)) holds j >= 1;

      hence thesis by A1, A2, Def10;

    end;

    theorem :: FINSEQ_8:29

    for f be FinSequence, k1,k2 be Nat st k1 in ( dom f) & k2 in ( dom f) holds ( smid (f,k1,k2)) = ((k1,k2) -cut f)

    proof

      let f be FinSequence, k1,k2 be Nat;

      set ff = ((k1,k2) -cut f);

      set g = ( smid (f,k1,k2));

      reconsider af = f as FinSequence of ( rng f) by FINSEQ_1:def 4;

      assume k1 in ( dom f) & k2 in ( dom f);

      then

       S0: 1 <= k1 <= ( len f) & 1 <= k2 <= ( len f) by FINSEQ_3: 25;

      per cases ;

        suppose

         A0: k1 <= k2;

        then

         WW: ( smid (f,k1,k2)) = ( mid (f,k1,k2)) by Th4;

        (( len ff) + k1) = (k2 + 1) by A0, S0, FINSEQ_6:def 4;

        

        then

         S2: ( len ff) = ((k2 + 1) - k1)

        .= ((k2 + 1) -' k1) by A0, NAT_D: 37;

        k2 <= (k2 + 1) by NAT_1: 13;

        then

         W4: ((k2 + 1) - k1) = ((k2 + 1) -' k1) by XREAL_1: 233, A0, XXREAL_0: 2;

        (k1 -' 1) <= k1 by NAT_D: 35;

        then (k1 -' 1) <= ( len f) by XXREAL_0: 2, S0;

        then

         S3: ( len (f /^ (k1 -' 1))) = (( len f) - (k1 -' 1)) by RFINSEQ:def 1;

        

         W3: (( len f) - (k1 -' 1)) = (( len f) - (k1 - 1)) by S0, XREAL_1: 233

        .= ((( len f) + 1) - k1);

        (k2 + 1) <= (( len f) + 1) by S0, XREAL_1: 6;

        then ((k2 + 1) -' k1) <= ( len (f /^ (k1 -' 1))) by S3, W3, W4, XREAL_1: 9;

        then

         A1: ( len ff) = ( len g) by S2, FINSEQ_1: 59;

        for k be Nat st 1 <= k <= ( len ff) holds (ff . k) = (g . k)

        proof

          let k be Nat;

          assume

           Z0: 1 <= k <= ( len ff);

          then

           ZZ: ((k -' 1) + 1) = k by XREAL_1: 235;

          (k -' 1) < ( len ff)

          proof

            per cases by Z0, XXREAL_0: 1;

              suppose k > 1;

              then 1 <= (k -' 1) by NAT_D: 49;

              then (k -' 1) < k by NAT_D: 51;

              hence thesis by Z0, XXREAL_0: 2;

            end;

              suppose k = 1;

              then (k -' 1) < k by NAT_D: 51;

              hence thesis by Z0, XXREAL_0: 2;

            end;

          end;

          then

           Z2: (ff . k) = (f . (k1 + (k -' 1))) by ZZ, FINSEQ_6:def 4, A0, S0;

          

           P1: k <= ( len ( mid (af,k1,k2))) by WW, A1, Z0;

          (k1 + k) >= k by NAT_1: 11;

          then

           P2: 1 <= (k1 + k) by XXREAL_0: 2, Z0;

          (g . k) = (( mid (f,k1,k2)) . k) by Th4, A0

          .= (af . ((k + k1) -' 1)) by Z0, FINSEQ_6: 118, A0, P1, S0

          .= (af . ((k1 + k) - 1)) by P2, XREAL_1: 233

          .= (af . (k1 + (k - 1)))

          .= (af . (k1 + (k -' 1))) by Z0, XREAL_1: 233;

          hence thesis by Z2;

        end;

        hence thesis by A1;

      end;

        suppose

         A1: k1 > k2;

        then ((k1,k2) -cut f) = {} by FINSEQ_6:def 4;

        hence thesis by A1, Th7;

      end;

    end;