calcul_2.miz



    begin

    reserve Al for QC-alphabet;

    reserve p,q,p1,p2,q1 for Element of ( CQC-WFF Al),

k,m,n,i for Element of NAT ,

f,f1,f2,g for FinSequence of ( CQC-WFF Al),

a,b,b1,b2,c for Nat;

    definition

      let m,n be Nat;

      :: CALCUL_2:def1

      func seq (m,n) -> set equals { k : (1 + m) <= k & k <= (n + m) };

      coherence ;

    end

    definition

      let m,n be Nat;

      :: original: seq

      redefine

      func seq (m,n) -> Subset of NAT ;

      coherence

      proof

        set X = ( seq (m,n));

        X c= NAT

        proof

          let x be object;

          assume x in X;

          then ex i st x = i & (1 + m) <= i & i <= (n + m);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: CALCUL_2:1

    

     Th1: c in ( seq (a,b)) iff (1 + a) <= c & c <= (b + a)

    proof

      

       A1: c in { m : (1 + a) <= m & m <= (b + a) } iff ex m st c = m & (1 + a) <= m & m <= (b + a);

      c is Element of NAT by ORDINAL1:def 12;

      hence thesis by A1;

    end;

    theorem :: CALCUL_2:2

    

     Th2: ( seq (a, 0 )) = {}

    proof

      hereby

        set x = the Element of ( seq (a, 0 ));

        assume

         A1: ( seq (a, 0 )) <> {} ;

        then

        reconsider x as Element of NAT by TARSKI:def 3;

        (1 + a) <= x & x <= ( 0 + a) by A1, Th1;

        hence contradiction by NAT_1: 13;

      end;

    end;

    theorem :: CALCUL_2:3

    

     Th3: b = 0 or (b + a) in ( seq (a,b))

    proof

      assume b <> 0 ;

      then ex c be Nat st b = (c + 1) by NAT_1: 6;

      then 1 <= b by NAT_1: 11;

      then (b + a) is Element of NAT & (1 + a) <= (b + a) by ORDINAL1:def 12, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: CALCUL_2:4

    

     Th4: b1 <= b2 iff ( seq (a,b1)) c= ( seq (a,b2))

    proof

      thus b1 <= b2 implies ( seq (a,b1)) c= ( seq (a,b2))

      proof

        assume b1 <= b2;

        then

         A1: (b1 + a) <= (b2 + a) by XREAL_1: 6;

        let b be object such that

         A2: b in ( seq (a,b1));

        reconsider c = b as Element of NAT by A2;

        c <= (b1 + a) by A2, Th1;

        then

         A3: c <= (b2 + a) by A1, XXREAL_0: 2;

        (1 + a) <= c by A2, Th1;

        hence thesis by A3;

      end;

      assume

       A4: ( seq (a,b1)) c= ( seq (a,b2));

      now

        assume b1 <> 0 ;

        then (b1 + a) in ( seq (a,b1)) by Th3;

        then (b1 + a) <= (b2 + a) by A4, Th1;

        hence thesis by XREAL_1: 6;

      end;

      hence thesis;

    end;

    theorem :: CALCUL_2:5

    

     Th5: (( seq (a,b)) \/ {((a + b) + 1)}) = ( seq (a,(b + 1)))

    proof

      thus (( seq (a,b)) \/ {((a + b) + 1)}) c= ( seq (a,(b + 1)))

      proof

        (b + 0 ) <= (b + 1) by XREAL_1: 7;

        then

         A1: ( seq (a,b)) c= ( seq (a,(b + 1))) by Th4;

        let x be object;

        assume x in (( seq (a,b)) \/ {((a + b) + 1)});

        then x in ( seq (a,b)) or x in {((a + b) + 1)} by XBOOLE_0:def 3;

        then x in ( seq (a,(b + 1))) or x = (a + (b + 1)) by A1, TARSKI:def 1;

        hence thesis by Th3;

      end;

      let x be object such that

       A2: x in ( seq (a,(b + 1)));

      reconsider x as Element of NAT by A2;

      x <= ((b + 1) + a) by A2, Th1;

      then

       A3: x <= (a + b) or x = ((a + b) + 1) by NAT_1: 8;

      (1 + a) <= x by A2, Th1;

      then x in ( seq (a,b)) or x in {((a + b) + 1)} by A3, TARSKI:def 1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: CALCUL_2:6

    

     Th6: (( seq (m,n)),n) are_equipotent

    proof

      defpred P[ Nat] means (( seq (m,$1)),$1) are_equipotent ;

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A2: (( seq (m,n)),n) are_equipotent ;

        reconsider i = (m + n) as Nat;

        

         A3: ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

         A4:

        now

          assume ( seq (m,n)) meets {(i + 1)};

          then

          consider x be object such that

           A5: x in ( seq (m,n)) and

           A6: x in {(i + 1)} by XBOOLE_0: 3;

          

           A7: not (i + 1) <= i by NAT_1: 13;

          x = (i + 1) by A6, TARSKI:def 1;

          hence contradiction by A5, A7, Th1;

        end;

         A8:

        now

          assume n meets {n};

          then

          consider x be object such that

           A9: x in n and

           A10: x in {n} by XBOOLE_0: 3;

          

           A: x = n by A10, TARSKI:def 1;

          reconsider x as set by TARSKI: 1;

           not x in x;

          hence contradiction by A, A9;

        end;

        ( seq (m,(n + 1))) = (( seq (m,n)) \/ {(i + 1)}) & ( {(i + 1)}, {n}) are_equipotent by Th5, CARD_1: 28;

        hence thesis by A2, A3, A8, A4, CARD_1: 31;

      end;

      

       A11: P[ 0 ] by Th2;

      for n be Nat holds P[n] from NAT_1:sch 2( A11, A1);

      hence thesis;

    end;

    registration

      let m, n;

      cluster ( seq (m,n)) -> finite;

      coherence

      proof

        n is finite & (n,( seq (m,n))) are_equipotent by Th6;

        hence thesis by CARD_1: 38;

      end;

    end

    registration

      let Al;

      let f;

      cluster ( len f) -> finite;

      coherence ;

    end

    theorem :: CALCUL_2:7

    

     Th7: ( seq (m,n)) c= ( Seg (m + n))

    proof

      let x be object;

      

       A1: 1 <= (1 + m) by NAT_1: 11;

      assume

       A2: x in ( seq (m,n));

      then

      reconsider x as Element of NAT ;

      (1 + m) <= x by A2, Th1;

      then

       A3: 1 <= x by A1, XXREAL_0: 2;

      x <= (n + m) by A2, Th1;

      hence thesis by A3, FINSEQ_1: 1;

    end;

    theorem :: CALCUL_2:8

    ( Seg n) misses ( seq (n,m))

    proof

      assume ( Seg n) meets ( seq (n,m));

      then

      consider a be object such that

       A1: a in ( Seg n) and

       A2: a in ( seq (n,m)) by XBOOLE_0: 3;

      reconsider i = a as Element of NAT by A1;

      i <= n & (n + 1) <= i by A1, A2, Th1, FINSEQ_1: 1;

      hence contradiction by NAT_1: 13;

    end;

    theorem :: CALCUL_2:9

    for f,g be FinSequence holds ( dom (f ^ g)) = (( dom f) \/ ( seq (( len f),( len g))))

    proof

      let f,g be FinSequence;

      now

        let a be object such that

         A1: a in ( dom (f ^ g));

        reconsider i = a as Element of NAT by A1;

        

         A2: 1 <= i by A1, FINSEQ_3: 25;

        

         A3: i <= ( len (f ^ g)) by A1, FINSEQ_3: 25;

        per cases ;

          suppose

           A4: i <= ( len f);

          

           A5: ( dom f) c= (( dom f) \/ ( seq (( len f),( len g)))) by XBOOLE_1: 7;

          i in ( dom f) by A2, A4, FINSEQ_3: 25;

          hence a in (( dom f) \/ ( seq (( len f),( len g)))) by A5;

        end;

          suppose

           A6: ( len f) < i;

          

           A7: ( seq (( len f),( len g))) c= (( dom f) \/ ( seq (( len f),( len g)))) by XBOOLE_1: 7;

          

           A8: i <= (( len f) + ( len g)) by A3, FINSEQ_1: 22;

          (( len f) + 1) <= i by A6, NAT_1: 13;

          then a in ( seq (( len f),( len g))) by A8;

          hence a in (( dom f) \/ ( seq (( len f),( len g)))) by A7;

        end;

      end;

      hence ( dom (f ^ g)) c= (( dom f) \/ ( seq (( len f),( len g))));

      let a be object such that

       A9: a in (( dom f) \/ ( seq (( len f),( len g))));

      per cases by A9, XBOOLE_0:def 3;

        suppose

         A10: a in ( dom f);

        then

        reconsider i = a as Element of NAT ;

        

         A11: 1 <= i by A10, FINSEQ_3: 25;

        

         A12: ( len f) <= ( len (f ^ g)) by CALCUL_1: 6;

        i <= ( len f) by A10, FINSEQ_3: 25;

        then i <= ( len (f ^ g)) by A12, XXREAL_0: 2;

        hence thesis by A11, FINSEQ_3: 25;

      end;

        suppose

         A13: a in ( seq (( len f),( len g)));

        then

        reconsider i = a as Element of NAT ;

        i <= (( len g) + ( len f)) by A13, Th1;

        then

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

        

         A15: 1 <= (1 + ( len f)) by NAT_1: 11;

        (1 + ( len f)) <= i by A13, Th1;

        then 1 <= i by A15, XXREAL_0: 2;

        hence thesis by A14, FINSEQ_3: 25;

      end;

    end;

    theorem :: CALCUL_2:10

    

     Th10: ( len ( Sgm ( seq (( len g),( len f))))) = ( len f)

    proof

      (( seq (( len g),( len f))),( len f)) are_equipotent by Th6;

      then

       A1: ( card ( seq (( len g),( len f)))) = ( card ( len f)) by CARD_1: 5;

      ( seq (( len g),( len f))) c= ( Seg (( len g) + ( len f))) by Th7;

      hence thesis by A1, FINSEQ_3: 39;

    end;

    theorem :: CALCUL_2:11

    

     Th11: ( dom ( Sgm ( seq (( len g),( len f))))) = ( dom f)

    proof

      ( len ( Sgm ( seq (( len g),( len f))))) = ( len f) by Th10;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: CALCUL_2:12

    

     Th12: ( rng ( Sgm ( seq (( len g),( len f))))) = ( seq (( len g),( len f)))

    proof

      ( seq (( len g),( len f))) c= ( Seg (( len g) + ( len f))) by Th7;

      hence thesis by FINSEQ_1:def 13;

    end;

    theorem :: CALCUL_2:13

    

     Th13: i in ( dom ( Sgm ( seq (( len g),( len f))))) implies (( Sgm ( seq (( len g),( len f)))) . i) = (( len g) + i)

    proof

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies for i be Nat st 1 <= i & i <= $1 holds (( Sgm ( seq (( len g),( len f)))) . i) = (( len g) + i);

      assume

       A1: i in ( dom ( Sgm ( seq (( len g),( len f)))));

      then i in ( dom f) by Th11;

      then

       A2: i <= ( len f) by FINSEQ_3: 25;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A4: P[k];

        assume that

         A5: 1 <= (k + 1) and

         A6: (k + 1) <= ( len f);

        let n be Nat such that

         A7: 1 <= n and

         A8: n <= (k + 1);

         A9:

        now

          assume

           A10: n = (k + 1);

          ( dom ( Sgm ( seq (( len g),( len f))))) = ( dom f) by Th11;

          then n in ( dom ( Sgm ( seq (( len g),( len f))))) by A5, A6, A10, FINSEQ_3: 25;

          then (( Sgm ( seq (( len g),( len f)))) . n) in ( rng ( Sgm ( seq (( len g),( len f))))) by FUNCT_1: 3;

          then

          reconsider i = (( Sgm ( seq (( len g),( len f)))) . n) as Element of NAT ;

           A11:

          now

            assume

             A12: i < (( len g) + (k + 1));

             A13:

            now

              assume k <> 0 ;

              then

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

              then

               A15: (( Sgm ( seq (( len g),( len f)))) . k) = (( len g) + k) by A4, A6, NAT_1: 13;

              then

              reconsider j = (( Sgm ( seq (( len g),( len f)))) . k) as Nat;

              

               A16: ( seq (( len g),( len f))) c= ( Seg (( len g) + ( len f))) by Th7;

              

               A17: k < (k + 1) & (k + 1) <= ( len ( Sgm ( seq (( len g),( len f))))) by A6, Th10, NAT_1: 13;

              i < ((( len g) + k) + 1) by A12;

              then i <= j by A15, NAT_1: 13;

              hence contradiction by A10, A14, A17, A16, FINSEQ_1:def 13;

            end;

            now

              1 <= ( len f) by A5, A6, XXREAL_0: 2;

              then 1 in ( dom f) by FINSEQ_3: 25;

              then

               A18: 1 in ( dom ( Sgm ( seq (( len g),( len f))))) by Th11;

              assume

               A19: k = 0 ;

              then not i in ( seq (( len g),( len f))) by A12, Th1;

              then not i in ( rng ( Sgm ( seq (( len g),( len f))))) by Th12;

              hence contradiction by A10, A19, A18, FUNCT_1: 3;

            end;

            hence contradiction by A13;

          end;

          now

            (1 + ( len g)) <= ((1 + ( len g)) + k) & (( len g) + (k + 1)) <= (( len f) + ( len g)) by A6, NAT_1: 11, XREAL_1: 6;

            then (( len g) + (k + 1)) in ( seq (( len g),( len f)));

            then (( len g) + (k + 1)) in ( rng ( Sgm ( seq (( len g),( len f))))) by Th12;

            then

            consider l be Nat such that

             A20: l in ( dom ( Sgm ( seq (( len g),( len f))))) and

             A21: (( Sgm ( seq (( len g),( len f)))) . l) = (( len g) + (k + 1)) by FINSEQ_2: 10;

            assume

             A22: i > (( len g) + (k + 1));

             A23:

            now

               A24:

              now

                assume

                 A25: l <= k;

                now

                  assume 1 <= l;

                  then (( len g) + (k + 1)) = (( len g) + l) by A4, A6, A21, A25, NAT_1: 13, XXREAL_0: 2;

                  hence contradiction by A25, NAT_1: 13;

                end;

                hence contradiction by A20, FINSEQ_3: 25;

              end;

              assume l <= (k + 1);

              hence contradiction by A10, A22, A21, A24, NAT_1: 8;

            end;

            

             A26: 1 <= n & ( seq (( len g),( len f))) c= ( Seg (( len g) + ( len f))) by A10, Th7, NAT_1: 11;

            l <= ( len ( Sgm ( seq (( len g),( len f))))) by A20, FINSEQ_3: 25;

            hence contradiction by A10, A22, A21, A23, A26, FINSEQ_1:def 13;

          end;

          hence thesis by A10, A11, XXREAL_0: 1;

        end;

        n <= k implies thesis by A4, A6, A7, NAT_1: 13, XXREAL_0: 2;

        hence thesis by A8, A9, NAT_1: 8;

      end;

      

       A27: P[ 0 ];

      

       A28: for n be Nat holds P[n] from NAT_1:sch 2( A27, A3);

      1 <= i by A1, FINSEQ_3: 25;

      hence thesis by A2, A28;

    end;

    theorem :: CALCUL_2:14

    

     Th14: ( seq (( len g),( len f))) c= ( dom (g ^ f))

    proof

      let a be object such that

       A1: a in ( seq (( len g),( len f)));

      reconsider n = a as Element of NAT by A1;

      n <= (( len f) + ( len g)) by A1, Th1;

      then

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

      

       A3: 1 <= (1 + ( len g)) by NAT_1: 11;

      (1 + ( len g)) <= n by A1, Th1;

      then 1 <= n by A3, XXREAL_0: 2;

      hence a in ( dom (g ^ f)) by A2, FINSEQ_3: 25;

    end;

    theorem :: CALCUL_2:15

    

     Th15: ( dom ((g ^ f) | ( seq (( len g),( len f))))) = ( seq (( len g),( len f)))

    proof

      ( dom ((g ^ f) | ( seq (( len g),( len f))))) = (( dom (g ^ f)) /\ ( seq (( len g),( len f)))) by RELAT_1: 61;

      hence thesis by Th14, XBOOLE_1: 28;

    end;

    theorem :: CALCUL_2:16

    

     Th16: ( Seq ((g ^ f) | ( seq (( len g),( len f))))) = (( Sgm ( seq (( len g),( len f)))) * (g ^ f))

    proof

      reconsider gf = ((g ^ f) | ( seq (( len g),( len f)))) as FinSubsequence;

      ( Seq gf) = (gf * ( Sgm ( dom gf))) by FINSEQ_1:def 14

      .= (gf * ( Sgm ( seq (( len g),( len f))))) by Th15

      .= (((g ^ f) | ( rng ( Sgm ( seq (( len g),( len f)))))) qua Function * ( Sgm ( seq (( len g),( len f)))) qua Function) by Th12

      .= ((g ^ f) qua Function * ( Sgm ( seq (( len g),( len f)))) qua Function) by FUNCT_4: 2;

      hence thesis;

    end;

    theorem :: CALCUL_2:17

    

     Th17: ( dom ( Seq ((g ^ f) | ( seq (( len g),( len f)))))) = ( dom f)

    proof

      ( rng ( Sgm ( seq (( len g),( len f))))) = ( seq (( len g),( len f))) by Th12;

      then

       A1: ( rng ( Sgm ( seq (( len g),( len f))))) c= ( dom (g ^ f)) by Th14;

      ( dom ( Seq ((g ^ f) | ( seq (( len g),( len f)))))) = ( dom (( Sgm ( seq (( len g),( len f)))) * (g ^ f))) by Th16;

      then ( dom ( Seq ((g ^ f) | ( seq (( len g),( len f)))))) = ( dom ( Sgm ( seq (( len g),( len f))))) by A1, RELAT_1: 27;

      hence thesis by Th11;

    end;

    theorem :: CALCUL_2:18

    

     Th18: f is_Subsequence_of (g ^ f)

    proof

      

       A1: for i be Nat st i in ( dom ( Seq ((g ^ f) | ( seq (( len g),( len f)))))) holds (( Seq ((g ^ f) | ( seq (( len g),( len f))))) . i) = (f . i)

      proof

        let i be Nat;

        assume i in ( dom ( Seq ((g ^ f) | ( seq (( len g),( len f))))));

        then

         A2: i in ( dom f) by Th17;

        then

         A3: i in ( dom ( Sgm ( seq (( len g),( len f))))) by Th11;

        (( Seq ((g ^ f) | ( seq (( len g),( len f))))) . i) = ((( Sgm ( seq (( len g),( len f)))) * (g ^ f)) . i) by Th16;

        then (( Seq ((g ^ f) | ( seq (( len g),( len f))))) . i) = ((g ^ f) . (( Sgm ( seq (( len g),( len f)))) . i)) by A3, FUNCT_1: 13;

        then (( Seq ((g ^ f) | ( seq (( len g),( len f))))) . i) = ((g ^ f) . (( len g) + i)) by A3, Th13;

        hence thesis by A2, FINSEQ_1:def 7;

      end;

      ( dom ( Seq ((g ^ f) | ( seq (( len g),( len f)))))) = ( dom f) by Th17;

      then ( Seq ((g ^ f) | ( seq (( len g),( len f))))) = f by A1, FINSEQ_1: 13;

      hence thesis by CALCUL_1:def 4;

    end;

    definition

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

      let P be Permutation of ( dom f);

      :: CALCUL_2:def2

      func Per (f,P) -> FinSequence of D equals (P * f);

      coherence

      proof

        

         A1: ( rng P) = ( dom f) by FUNCT_2:def 3;

        then ( dom (P * f)) = ( dom P) by RELAT_1: 27;

        then ( dom (P * f)) = ( dom f) by FUNCT_2: 52;

        then ex n be Nat st ( dom (P * f)) = ( Seg n) by FINSEQ_1:def 2;

        then

        reconsider F = (P * f) as FinSequence by FINSEQ_1:def 2;

        ( rng F) = ( rng f) by A1, RELAT_1: 28;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    reserve P for Permutation of ( dom f);

    theorem :: CALCUL_2:19

    

     Th19: ( dom ( Per (f,P))) = ( dom f)

    proof

      ( rng P) = ( dom f) by FUNCT_2:def 3;

      then ( dom (P * f)) = ( dom P) by RELAT_1: 27;

      hence thesis by FUNCT_2: 52;

    end;

    theorem :: CALCUL_2:20

    

     Th20: |- (f ^ <*p*>) implies |- ((g ^ f) ^ <*p*>)

    proof

      ( Suc (f ^ <*p*>)) = p by CALCUL_1: 5;

      then

       A1: ( Suc (f ^ <*p*>)) = ( Suc ((g ^ f) ^ <*p*>)) by CALCUL_1: 5;

      ( Ant (f ^ <*p*>)) = f by CALCUL_1: 5;

      then ( Ant (f ^ <*p*>)) is_Subsequence_of (g ^ f) by Th18;

      then

       A2: ( Ant (f ^ <*p*>)) is_Subsequence_of ( Ant ((g ^ f) ^ <*p*>)) by CALCUL_1: 5;

      assume |- (f ^ <*p*>);

      hence thesis by A2, A1, CALCUL_1: 36;

    end;

    begin

    definition

      let Al, f;

      :: CALCUL_2:def3

      func Begin (f) -> Element of ( CQC-WFF Al) means

      : Def3: it = (f . 1) if 1 <= ( len f)

      otherwise it = ( VERUM Al);

      existence

      proof

        1 <= ( len f) implies ex p st p = (f . 1)

        proof

          assume 1 <= ( len f);

          then 1 in ( dom f) by FINSEQ_3: 25;

          then (f . 1) in ( CQC-WFF Al) by FINSEQ_2: 11;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness ;

      consistency ;

    end

    definition

      let Al, f;

      assume

       A1: 1 <= ( len f);

      :: CALCUL_2:def4

      func Impl (f) -> Element of ( CQC-WFF Al) means

      : Def4: ex F be FinSequence of ( CQC-WFF Al) st it = (F . ( len f)) & ( len F) = ( len f) & ((F . 1) = ( Begin f) or ( len f) = 0 ) & for n be Nat st 1 <= n & n < ( len f) holds ex p, q st p = (f . (n + 1)) & q = (F . n) & (F . (n + 1)) = (p => q);

      existence

      proof

        defpred P[ Nat, set, set] means ex p, q st p = (f . ($1 + 1)) & q = $2 & $3 = (p => q);

        

         A2: for n be Nat st 1 <= n & n < ( len f) holds for x be Element of ( CQC-WFF Al) holds ex y be Element of ( CQC-WFF Al) st P[n, x, y]

        proof

          let n be Nat such that 1 <= n and

           A3: n < ( len f);

          1 <= (n + 1) & (n + 1) <= ( len f) by A3, NAT_1: 11, NAT_1: 13;

          then (n + 1) in ( dom f) by FINSEQ_3: 25;

          then

          reconsider p = (f . (n + 1)) as Element of ( CQC-WFF Al) by FINSEQ_2: 11;

          let x be Element of ( CQC-WFF Al);

          take (p => x), p, x;

          thus thesis;

        end;

        consider F be FinSequence of ( CQC-WFF Al) such that

         A4: ( len F) = ( len f) & ((F . 1) = ( Begin f) or ( len f) = 0 ) & for n be Nat st 1 <= n & n < ( len f) holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 4( A2);

        ( len f) in ( dom F) by A1, A4, FINSEQ_3: 25;

        then

        reconsider p = (F . ( len f)) as Element of ( CQC-WFF Al) by FINSEQ_2: 11;

        take p;

        thus thesis by A4;

      end;

      uniqueness

      proof

        defpred P[ Nat, set, set] means ex p, q st p = (f . ($1 + 1)) & q = $2 & $3 = (p => q);

        let p1, p2 such that

         A5: ex F be FinSequence of ( CQC-WFF Al) st p1 = (F . ( len f)) & ( len F) = ( len f) & ((F . 1) = ( Begin f) or ( len f) = 0 ) & for n be Nat st 1 <= n & n < ( len f) holds P[n, (F . n), (F . (n + 1))] and

         A6: ex F be FinSequence of ( CQC-WFF Al) st p2 = (F . ( len f)) & ( len F) = ( len f) & ((F . 1) = ( Begin f) or ( len f) = 0 ) & for n be Nat st 1 <= n & n < ( len f) holds P[n, (F . n), (F . (n + 1))];

        consider H be FinSequence of ( CQC-WFF Al) such that

         A7: p2 = (H . ( len f)) and

         A8: ( len H) = ( len f) & ((H . 1) = ( Begin f) or ( len f) = 0 ) & for n be Nat st 1 <= n & n < ( len f) holds P[n, (H . n), (H . (n + 1))] by A6;

        consider G be FinSequence of ( CQC-WFF Al) such that

         A9: p1 = (G . ( len f)) and

         A10: ( len G) = ( len f) & ((G . 1) = ( Begin f) or ( len f) = 0 ) & for n be Nat st 1 <= n & n < ( len f) holds P[n, (G . n), (G . (n + 1))] by A5;

        

         A11: for n be Nat st 1 <= n & n < ( len f) holds for x,y1,y2 be Element of ( CQC-WFF Al) st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

        G = H from RECDEF_1:sch 8( A11, A10, A8);

        hence thesis by A9, A7;

      end;

    end

    theorem :: CALCUL_2:21

    

     Th21: |- ((f ^ <*p*>) ^ <*p*>)

    proof

      ( len (f ^ <*p*>)) in ( dom (f ^ <*p*>)) by CALCUL_1: 10;

      then (( len f) + ( len <*p*>)) in ( dom (f ^ <*p*>)) by FINSEQ_1: 22;

      then

       A1: (( len f) + 1) in ( dom (f ^ <*p*>)) by FINSEQ_1: 39;

      ((f ^ <*p*>) . (( len f) + 1)) = p by FINSEQ_1: 42;

      then p is_tail_of (f ^ <*p*>) by A1, CALCUL_1:def 16;

      then ( Suc ((f ^ <*p*>) ^ <*p*>)) is_tail_of (f ^ <*p*>) by CALCUL_1: 5;

      then ( Suc ((f ^ <*p*>) ^ <*p*>)) is_tail_of ( Ant ((f ^ <*p*>) ^ <*p*>)) by CALCUL_1: 5;

      hence thesis by CALCUL_1: 33;

    end;

    theorem :: CALCUL_2:22

    

     Th22: |- (f ^ <*(p '&' q)*>) implies |- (f ^ <*p*>)

    proof

      

       A1: (p '&' q) = ( Suc (f ^ <*(p '&' q)*>)) by CALCUL_1: 5;

      assume |- (f ^ <*(p '&' q)*>);

      then |- (( Ant (f ^ <*(p '&' q)*>)) ^ <*p*>) by A1, CALCUL_1: 40;

      hence thesis by CALCUL_1: 5;

    end;

    theorem :: CALCUL_2:23

    

     Th23: |- (f ^ <*(p '&' q)*>) implies |- (f ^ <*q*>)

    proof

      

       A1: (p '&' q) = ( Suc (f ^ <*(p '&' q)*>)) by CALCUL_1: 5;

      assume |- (f ^ <*(p '&' q)*>);

      then |- (( Ant (f ^ <*(p '&' q)*>)) ^ <*q*>) by A1, CALCUL_1: 41;

      hence thesis by CALCUL_1: 5;

    end;

    theorem :: CALCUL_2:24

    

     Th24: |- (f ^ <*p*>) & |- ((f ^ <*p*>) ^ <*q*>) implies |- (f ^ <*q*>)

    proof

      

       A1: 1 <= ( len (f ^ <*p*>)) by CALCUL_1: 10;

      assume |- (f ^ <*p*>) & |- ((f ^ <*p*>) ^ <*q*>);

      then |- (( Ant (f ^ <*p*>)) ^ <*q*>) by A1, CALCUL_1: 45;

      hence thesis by CALCUL_1: 5;

    end;

    theorem :: CALCUL_2:25

    

     Th25: |- (f ^ <*p*>) & |- (f ^ <*( 'not' p)*>) implies |- (f ^ <*q*>)

    proof

      

       A1: ( Ant (f ^ <*p*>)) = f & ( Suc (f ^ <*p*>)) = p by CALCUL_1: 5;

      assume |- (f ^ <*p*>) & |- (f ^ <*( 'not' p)*>);

      hence thesis by A1, CALCUL_1: 44;

    end;

    theorem :: CALCUL_2:26

    

     Th26: |- ((f ^ <*p*>) ^ <*q*>) & |- ((f ^ <*( 'not' p)*>) ^ <*q*>) implies |- (f ^ <*q*>)

    proof

      set f1 = ((f ^ <*p*>) ^ <*q*>);

      set f2 = ((f ^ <*( 'not' p)*>) ^ <*q*>);

      assume

       A1: |- f1 & |- f2;

      

       A2: ( Ant f2) = (f ^ <*( 'not' p)*>) by CALCUL_1: 5;

      

       A3: ( Ant f1) = (f ^ <*p*>) by CALCUL_1: 5;

      then ( Suc ( Ant f1)) = p by CALCUL_1: 5;

      then

       A4: ( 'not' ( Suc ( Ant f1))) = ( Suc ( Ant f2)) by A2, CALCUL_1: 5;

      

       A5: 1 < ( len f1) & 1 < ( len f2) by CALCUL_1: 9;

      

       A6: ( Suc f1) = q by CALCUL_1: 5;

      then

       A7: ( Suc f1) = ( Suc f2) by CALCUL_1: 5;

      

       A8: ( Ant ( Ant f1)) = f by A3, CALCUL_1: 5;

      then ( Ant ( Ant f1)) = ( Ant ( Ant f2)) by A2, CALCUL_1: 5;

      hence thesis by A1, A8, A4, A6, A5, A7, CALCUL_1: 37;

    end;

    theorem :: CALCUL_2:27

    

     Th27: |- ((f ^ <*p*>) ^ <*q*>) implies |- (f ^ <*(p => q)*>)

    proof

      assume

       A1: |- ((f ^ <*p*>) ^ <*q*>);

      set g1 = (((f ^ <*(p '&' ( 'not' q))*>) ^ <*p*>) ^ <*q*>);

      set g = ((f ^ <*p*>) ^ <*q*>);

      

       A2: ( Ant g1) = ((f ^ <*(p '&' ( 'not' q))*>) ^ <*p*>) by CALCUL_1: 5;

      ( Suc g) = q by CALCUL_1: 5;

      then

       A3: ( Suc g1) = ( Suc g) by CALCUL_1: 5;

      

       A4: ( Ant g) = (f ^ <*p*>) by CALCUL_1: 5;

      then

       A5: ( 0 + 1) <= ( len ( Ant g)) by CALCUL_1: 10;

      

       A6: |- ((f ^ <*(p '&' ( 'not' q))*>) ^ <*(p '&' ( 'not' q))*>) by Th21;

      then

       A7: |- ((f ^ <*(p '&' ( 'not' q))*>) ^ <*p*>) by Th22;

      ( Ant ( Ant g)) = f & ( Suc ( Ant g)) = p by A4, CALCUL_1: 5;

      then |- g1 by A1, A5, A3, A2, CALCUL_1: 13, CALCUL_1: 36;

      then

       A8: |- ((f ^ <*(p '&' ( 'not' q))*>) ^ <*q*>) by A7, Th24;

      

       A9: |- ((f ^ <*( 'not' (p '&' ( 'not' q)))*>) ^ <*( 'not' (p '&' ( 'not' q)))*>) by Th21;

       |- ((f ^ <*(p '&' ( 'not' q))*>) ^ <*( 'not' q)*>) by A6, Th23;

      then |- ((f ^ <*(p '&' ( 'not' q))*>) ^ <*( 'not' (p '&' ( 'not' q)))*>) by A8, Th25;

      then |- (f ^ <*( 'not' (p '&' ( 'not' q)))*>) by A9, Th26;

      hence thesis by QC_LANG2:def 2;

    end;

    theorem :: CALCUL_2:28

    

     Th28: 1 <= ( len g) & |- (f ^ g) implies |- (f ^ <*( Impl ( Rev g))*>)

    proof

      set h = ( Rev g);

      assume that

       A1: 1 <= ( len g) and

       A2: |- (f ^ g);

      

       A3: 1 <= ( len h) by A1, FINSEQ_5:def 3;

      then

      consider F be FinSequence of ( CQC-WFF Al) such that

       A4: ( Impl h) = (F . ( len h)) and

       A5: ( len F) = ( len h) and

       A6: (F . 1) = ( Begin h) or ( len h) = 0 and

       A7: for n be Nat st 1 <= n & n < ( len h) holds ex p, q st p = (h . (n + 1)) & q = (F . n) & (F . (n + 1)) = (p => q) by Def4;

      

       A8: 1 <= ( len h) by A1, FINSEQ_5:def 3;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len F) implies ex f1, f2, n st ($1 + n) = ( len (f ^ g)) & f1 = ((f ^ g) | ( Seg n)) & f2 = (f1 ^ <*(F . $1)*>) & |- f2;

      

       A9: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A10: P[k];

        

         A11: ( len g) <= ( len (f ^ g)) by CALCUL_1: 6;

        assume that

         A12: 1 <= (k + 1) and

         A13: (k + 1) <= ( len F);

        

         A14: (k + 1) <= ( len g) by A5, A13, FINSEQ_5:def 3;

        then

        consider n be Nat such that

         A15: ( len (f ^ g)) = ((k + 1) + n) by A11, NAT_1: 10, XXREAL_0: 2;

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

         A16:

        now

          (k + 1) in ( dom F) by A12, A13, FINSEQ_3: 25;

          then

          reconsider r = (F . (k + 1)) as Element of ( CQC-WFF Al) by FINSEQ_2: 11;

          set f1 = ((f ^ g) | ( Seg n));

          reconsider f1 as FinSequence of ( CQC-WFF Al) by FINSEQ_1: 18;

          set f2 = (f1 ^ <*r*>);

          ( len (f ^ g)) <= (( len (f ^ g)) + k) by NAT_1: 11;

          then

           A17: (( len (f ^ g)) - k) <= ((( len (f ^ g)) + k) - k) by XREAL_1: 9;

          assume k <> 0 ;

          then

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

          then

          consider f1k be FinSequence of ( CQC-WFF Al) such that

           A19: ex f2, n st (k + n) = ( len (f ^ g)) & f1k = ((f ^ g) | ( Seg n)) & f2 = (f1k ^ <*(F . k)*>) & |- f2 by A10, A13, NAT_1: 13;

          consider f2k be FinSequence of ( CQC-WFF Al) such that

           A20: ex n st (k + n) = ( len (f ^ g)) & f1k = ((f ^ g) | ( Seg n)) & f2k = (f1k ^ <*(F . k)*>) & |- f2k by A19;

          consider nk be Element of NAT such that

           A21: (k + nk) = ( len (f ^ g)) and

           A22: f1k = ((f ^ g) | ( Seg nk)) & f2k = (f1k ^ <*(F . k)*>) and

           A23: |- f2k by A20;

          1 <= (n + 1) by NAT_1: 11;

          then

           A24: nk in ( dom (f ^ g)) by A15, A21, A17, FINSEQ_3: 25;

          then

          reconsider p = ((f ^ g) . nk) as Element of ( CQC-WFF Al) by FINSEQ_2: 11;

          (n + 1) = nk by A15, A21;

          then

           A25: f2k = ((f1 ^ <*((f ^ g) . nk)*>) ^ <*(F . k)*>) by A22, A24, FINSEQ_5: 10;

          

           A26: k < ( len h) by A5, A13, NAT_1: 13;

          then

          consider p1, q1 such that

           A27: p1 = (h . (k + 1)) and

           A28: q1 = (F . k) & (F . (k + 1)) = (p1 => q1) by A7, A18;

          (k + 1) in ( dom h) by A5, A12, A13, FINSEQ_3: 25;

          then (k + 1) in ( dom g) by FINSEQ_5: 57;

          

          then

           A29: p1 = (g . ((( len g) - (k + 1)) + 1)) by A27, FINSEQ_5: 58

          .= (g . (( len g) - k));

          k < ( len g) by A26, FINSEQ_5:def 3;

          then

           A30: (k + ( - k)) < (( len g) + ( - k)) by XREAL_1: 8;

          then

          reconsider i = (( len g) - k) as Element of NAT by INT_1: 3;

          ( len g) <= (k + ( len g)) by NAT_1: 11;

          then

           A31: i <= ( len g) by XREAL_1: 20;

          ( 0 + 1) <= i by A30, INT_1: 7;

          then i in ( dom g) by A31, FINSEQ_3: 25;

          

          then p1 = ((f ^ g) . (( len f) + i)) by A29, FINSEQ_1:def 7

          .= ((f ^ g) . ((( len f) + ( len g)) - k))

          .= ((f ^ g) . (( len (f ^ g)) - k)) by FINSEQ_1: 22

          .= p by A21;

          then |- f2 by A23, A25, A28, Th27;

          hence thesis by A15;

        end;

        

         A32: (k + 1) <= ( len (f ^ g)) by A14, A11, XXREAL_0: 2;

        now

          (F . 1) = (h . 1) by A3, A6, Def3;

          then

           A33: (F . 1) = (g . ( len g)) by FINSEQ_5: 62;

          set f1 = ((f ^ g) | ( Seg n));

          reconsider f1 as FinSequence of ( CQC-WFF Al) by FINSEQ_1: 18;

          set f2 = (f1 ^ <*(F . 1)*>);

          

           A34: ( len g) in ( dom g) by A1, FINSEQ_3: 25;

          assume

           A35: k = 0 ;

          then

           A36: ((f ^ g) . (n + 1)) = ((f ^ g) . (( len f) + ( len g))) by A15, FINSEQ_1: 22;

          1 <= ( len (f ^ g)) by A12, A32, XXREAL_0: 2;

          then ( len (f ^ g)) in ( dom (f ^ g)) by FINSEQ_3: 25;

          then ((f ^ g) | ( Seg (n + 1))) = (f1 ^ <*((f ^ g) . (n + 1))*>) by A15, A35, FINSEQ_5: 10;

          then f2 = ((f ^ g) | ( Seg ( len (f ^ g)))) by A15, A35, A33, A34, A36, FINSEQ_1:def 7;

          then

           A37: f2 = ((f ^ g) | ( dom (f ^ g))) by FINSEQ_1:def 3;

          then

          reconsider f2 as FinSequence of ( CQC-WFF Al) by RELAT_1: 69;

          take f1, f2, n;

           |- f2 by A2, A37, RELAT_1: 69;

          hence thesis by A15, A35;

        end;

        hence thesis by A16;

      end;

      

       A38: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A38, A9);

      then

      consider f1 such that

       A39: ex f2, n st (( len h) + n) = ( len (f ^ g)) & f1 = ((f ^ g) | ( Seg n)) & f2 = (f1 ^ <*(F . ( len h))*>) & |- f2 by A5, A8;

      consider f2 such that

       A40: ex n st (( len h) + n) = ( len (f ^ g)) & f1 = ((f ^ g) | ( Seg n)) & f2 = (f1 ^ <*(F . ( len h))*>) & |- f2 by A39;

      consider n such that

       A41: (( len h) + n) = ( len (f ^ g)) and

       A42: f1 = ((f ^ g) | ( Seg n)) & f2 = (f1 ^ <*(F . ( len h))*>) & |- f2 by A40;

      ((n + ( len h)) - ( len h)) = (( len (f ^ g)) - ( len g)) by A41, FINSEQ_5:def 3;

      then ((n + ( len h)) + ( - ( len h))) = ((( len f) + ( len g)) - ( len g)) by FINSEQ_1: 22;

      then ( Seg n) = ( dom f) by FINSEQ_1:def 3;

      hence thesis by A4, A42, FINSEQ_1: 21;

    end;

    theorem :: CALCUL_2:29

    

     Th29: |- (( Per (f,P)) ^ <*( Impl ( Rev (f ^ <*p*>)))*>) implies |- (( Per (f,P)) ^ <*p*>)

    proof

      set g = (f ^ <*p*>);

      set h = ( Rev g);

      

       A1: 1 <= ( len g) by CALCUL_1: 10;

      then

       A2: 1 <= ( len h) by FINSEQ_5:def 3;

      then

      consider F be FinSequence of ( CQC-WFF Al) such that

       A3: ( Impl h) = (F . ( len h)) and

       A4: ( len F) = ( len h) and

       A5: (F . 1) = ( Begin h) or ( len h) = 0 and

       A6: for n be Nat st 1 <= n & n < ( len h) holds ex p, q st p = (h . (n + 1)) & q = (F . n) & (F . (n + 1)) = (p => q) by Def4;

      set H = ( Rev F);

      

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

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len H) implies ex p st p = (H . $1) & |- (( Per (f,P)) ^ <*p*>);

      assume

       A8: |- (( Per (f,P)) ^ <*( Impl ( Rev (f ^ <*p*>)))*>);

      

       A9: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A10: P[k];

        assume that

         A11: 1 <= (k + 1) and

         A12: (k + 1) <= ( len H);

         A13:

        now

          

           A14: k < ( len H) by A12, NAT_1: 13;

          then ( 0 + k) < ( len F) by FINSEQ_5:def 3;

          then

           A15: (( 0 + k) + ( - k)) < (( len F) + ( - k)) by XREAL_1: 8;

          then

          reconsider i = (( len F) - k) as Element of NAT by INT_1: 3;

          

           A16: (( len g) - i) = (( len g) - (( len g) - k)) by A4, FINSEQ_5:def 3

          .= k;

          then

          reconsider j = (( len g) - i) as Nat;

          

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

          then

           A18: 1 <= (i + 1) by NAT_1: 13;

          assume

           A19: k <> 0 ;

          then

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

          then

          consider pk be Element of ( CQC-WFF Al) such that

           A21: pk = (H . k) and

           A22: |- (( Per (f,P)) ^ <*pk*>) by A10, A12, NAT_1: 13;

          ( len F) < (( len F) + k) by A19, XREAL_1: 29;

          then

           A23: (( len F) + ( - k)) < ((( len F) + k) + ( - k)) by XREAL_1: 8;

          then

          consider p1, q1 such that

           A24: p1 = (h . (i + 1)) and

           A25: q1 = (F . i) and

           A26: (F . (i + 1)) = (p1 => q1) by A4, A6, A17;

          take q1;

          (k + 1) in ( dom H) by A11, A12, FINSEQ_3: 25;

          then i = ((( len F) - (k + 1)) + 1) & (k + 1) in ( dom F) by FINSEQ_5: 57;

          then

           A27: q1 = (H . (k + 1)) by A25, FINSEQ_5: 58;

          ( len g) < (( len g) + i) by A15, XREAL_1: 29;

          then (( len g) + ( - i)) < ((( len g) + i) + ( - i)) by XREAL_1: 8;

          then j < (( len f) + ( len <*p*>)) by FINSEQ_1: 22;

          then j < (( len f) + 1) by FINSEQ_1: 39;

          then j <= ( len f) by NAT_1: 13;

          then

           A28: j in ( dom f) by A20, A16, FINSEQ_3: 25;

          then

           A29: (g . j) = ((g | ( dom f)) . j) by FUNCT_1: 49;

          j in ( rng P) by A28, FUNCT_2:def 3;

          then

          consider a be object such that

           A30: a in ( dom P) and

           A31: (P . a) = j by FUNCT_1:def 3;

          

           A32: a in ( dom f) by A30;

          then

          reconsider j1 = a as Element of NAT ;

          set g1 = (( Per (f,P)) ^ <*p1*>);

          (i + 1) <= ( len h) by A4, A23, NAT_1: 13;

          then (i + 1) in ( dom h) by A18, FINSEQ_3: 25;

          then (i + 1) in ( dom g) by FINSEQ_5: 57;

          

          then p1 = (g . ((( len g) - (i + 1)) + 1)) by A24, FINSEQ_5: 58

          .= (g . (( len g) - i));

          then p1 = (f . (P . j1)) by A29, A31, FINSEQ_1: 21;

          then p1 = ((P * f) . j1) by A30, FUNCT_1: 13;

          then ( Suc g1) = (( Per (f,P)) . j1) by CALCUL_1: 5;

          then

           A33: ( Suc g1) = (( Ant g1) . j1) by CALCUL_1: 5;

          j1 in ( dom ( Per (f,P))) by A32, Th19;

          then j1 in ( dom ( Ant g1)) by CALCUL_1: 5;

          then ( Suc g1) is_tail_of ( Ant g1) by A33, CALCUL_1:def 16;

          then

           A34: |- g1 by CALCUL_1: 33;

          k in ( dom H) by A20, A14, FINSEQ_3: 25;

          then k in ( dom F) by FINSEQ_5: 57;

          then pk = (p1 => q1) by A21, A26, FINSEQ_5: 58;

          then |- (( Per (f,P)) ^ <*q1*>) by A22, A34, CALCUL_1: 56;

          hence thesis by A27;

        end;

        now

          1 <= ( len H) by A2, A4, FINSEQ_5:def 3;

          then

           A35: 1 in ( dom H) by FINSEQ_3: 25;

          then

          reconsider p = (H . 1) as Element of ( CQC-WFF Al) by FINSEQ_2: 11;

          assume

           A36: k = 0 ;

          take p;

          1 in ( dom F) by A35, FINSEQ_5: 57;

          

          then p = (F . ((( len F) - 1) + 1)) by FINSEQ_5: 58

          .= ( Impl h) by A3, A4;

          hence thesis by A8, A36;

        end;

        hence thesis by A13;

      end;

      

       A37: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A37, A9);

      then

      consider q such that

       A38: q = (H . ( len H)) and

       A39: |- (( Per (f,P)) ^ <*q*>) by A7;

      q = (H . ( len F)) by A38, FINSEQ_5:def 3;

      then q = ( Begin h) by A1, A5, FINSEQ_5: 62, FINSEQ_5:def 3;

      then q = (h . 1) by A2, Def3;

      then q = (g . ( len g)) by FINSEQ_5: 62;

      then q = (g . (( len f) + ( len <*p*>))) by FINSEQ_1: 22;

      then q = (g . (( len f) + 1)) by FINSEQ_1: 39;

      hence thesis by A39, FINSEQ_1: 42;

    end;

    theorem :: CALCUL_2:30

     |- (f ^ <*p*>) implies |- (( Per (f,P)) ^ <*p*>)

    proof

      set g = (f ^ <*p*>);

      assume |- (f ^ <*p*>);

      then |- ((( Per (f,P)) ^ f) ^ <*p*>) by Th20;

      then

       A1: |- (( Per (f,P)) ^ g) by FINSEQ_1: 32;

      1 <= ( len g) by CALCUL_1: 10;

      then |- (( Per (f,P)) ^ <*( Impl ( Rev g))*>) by A1, Th28;

      hence thesis by Th29;

    end;

    begin

    notation

      let n;

      let c be set;

      synonym IdFinS (c,n) for n |-> c;

    end

    theorem :: CALCUL_2:31

    

     Th31: for c be set st 1 <= n holds ( rng ( IdFinS (c,n))) = ( rng <*c*>)

    proof

      let c be set such that

       A1: 1 <= n;

      n in ( Seg n) by A1, FINSEQ_1: 1;

      then

       A2: (( IdFinS (c,n)) . n) = c by FUNCOP_1: 7;

      thus ( rng ( IdFinS (c,n))) c= ( rng <*c*>)

      proof

        let a be object;

        assume a in ( rng ( IdFinS (c,n)));

        then

        consider i be Nat such that

         A3: i in ( dom ( IdFinS (c,n))) and

         A4: (( IdFinS (c,n)) . i) = a by FINSEQ_2: 10;

        i in ( Seg ( len ( IdFinS (c,n)))) by A3, FINSEQ_1:def 3;

        then i in ( Seg n) by CARD_1:def 7;

        then a = c by A4, FUNCOP_1: 7;

        then a in {c} by TARSKI:def 1;

        hence thesis by FINSEQ_1: 38;

      end;

      let a be object;

      assume a in ( rng <*c*>);

      then a in {c} by FINSEQ_1: 38;

      then

       A5: a = c by TARSKI:def 1;

      n = ( len ( IdFinS (c,n))) by CARD_1:def 7;

      then n in ( dom ( IdFinS (c,n))) by A1, FINSEQ_3: 25;

      hence thesis by A5, A2, FUNCT_1:def 3;

    end;

    definition

      let D be non empty set, n be Element of NAT , p be Element of D;

      :: original: IdFinS

      redefine

      func IdFinS (p,n) -> FinSequence of D ;

      coherence

      proof

        now

          let i be Nat;

          assume i in ( dom ( IdFinS (p,n)));

          then i in ( Seg ( len ( IdFinS (p,n)))) by FINSEQ_1:def 3;

          then i in ( Seg n) by CARD_1:def 7;

          then (( IdFinS (p,n)) . i) = p by FUNCOP_1: 7;

          hence (( IdFinS (p,n)) . i) in D;

        end;

        hence thesis by FINSEQ_2: 12;

      end;

    end

    theorem :: CALCUL_2:32

    1 <= n & |- ((f ^ ( IdFinS (p,n))) ^ <*q*>) implies |- ((f ^ <*p*>) ^ <*q*>)

    proof

      assume that

       A1: 1 <= n and

       A2: |- ((f ^ ( IdFinS (p,n))) ^ <*q*>);

      set g = ((f ^ ( IdFinS (p,n))) ^ <*q*>);

      set h = ( Rev g);

      

       A3: 1 <= ( len g) by CALCUL_1: 10;

      then

       A4: 1 <= ( len h) by FINSEQ_5:def 3;

      then

      consider F be FinSequence of ( CQC-WFF Al) such that

       A5: ( Impl h) = (F . ( len h)) and

       A6: ( len F) = ( len h) and

       A7: (F . 1) = ( Begin h) or ( len h) = 0 and

       A8: for n be Nat st 1 <= n & n < ( len h) holds ex p, q st p = (h . (n + 1)) & q = (F . n) & (F . (n + 1)) = (p => q) by Def4;

      set H = ( Rev F);

      

       A9: 1 <= ( len H) by A4, A6, FINSEQ_5:def 3;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len H) implies ex p1 st p1 = (H . $1) & |- ((f ^ <*p*>) ^ <*p1*>);

       |- (((f ^ <*p*>) ^ (f ^ ( IdFinS (p,n)))) ^ <*q*>) by A2, Th20;

      then |- ((f ^ <*p*>) ^ ((f ^ ( IdFinS (p,n))) ^ <*q*>)) by FINSEQ_1: 32;

      then

       A10: |- ((f ^ <*p*>) ^ <*( Impl ( Rev g))*>) by A3, Th28;

      

       A11: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A12: P[k];

        assume that

         A13: 1 <= (k + 1) and

         A14: (k + 1) <= ( len H);

         A15:

        now

          

           A16: k < ( len H) by A14, NAT_1: 13;

          then ( 0 + k) < ( len F) by FINSEQ_5:def 3;

          then

           A17: (( 0 + k) + ( - k)) < (( len F) + ( - k)) by XREAL_1: 8;

          then

          reconsider i = (( len F) - k) as Element of NAT by INT_1: 3;

          

           A18: (( len g) - i) = (( len g) - (( len g) - k)) by A6, FINSEQ_5:def 3

          .= k;

          

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

          then

           A20: 1 <= (i + 1) by NAT_1: 13;

          assume

           A21: k <> 0 ;

          then

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

          then

          consider pk be Element of ( CQC-WFF Al) such that

           A23: pk = (H . k) and

           A24: |- ((f ^ <*p*>) ^ <*pk*>) by A12, A14, NAT_1: 13;

          ( len F) < (( len F) + k) by A21, XREAL_1: 29;

          then

           A25: (( len F) + ( - k)) < ((( len F) + k) + ( - k)) by XREAL_1: 8;

          then

          consider p1, q1 such that

           A26: p1 = (h . (i + 1)) and

           A27: q1 = (F . i) and

           A28: (F . (i + 1)) = (p1 => q1) by A6, A8, A19;

          set g1 = ((f ^ <*p*>) ^ <*p1*>);

          

           A29: ( Suc g1) = p1 by CALCUL_1: 5;

          ( len g) < (( len g) + i) by A17, XREAL_1: 29;

          then (( len g) + ( - i)) < ((( len g) + i) + ( - i)) by XREAL_1: 8;

          then k < (( len (f ^ ( IdFinS (p,n)))) + ( len <*q*>)) by FINSEQ_1: 22, A18;

          then k < (( len (f ^ ( IdFinS (p,n)))) + 1) by FINSEQ_1: 39;

          then k <= ( len (f ^ ( IdFinS (p,n)))) by NAT_1: 13;

          then

           A30: k in ( dom (f ^ ( IdFinS (p,n)))) by A22, FINSEQ_3: 25;

          then

           A31: (g . k) = ((g | ( dom (f ^ ( IdFinS (p,n))))) . k) by FUNCT_1: 49;

          

           A32: ((f ^ ( IdFinS (p,n))) . k) in ( rng (f ^ ( IdFinS (p,n)))) by A30, FUNCT_1: 3;

          ( rng (f ^ ( IdFinS (p,n)))) = (( rng f) \/ ( rng ( IdFinS (p,n)))) by FINSEQ_1: 31

          .= (( rng f) \/ ( rng <*p*>)) by A1, Th31

          .= ( rng (f ^ <*p*>)) by FINSEQ_1: 31;

          then

           A33: ((f ^ ( IdFinS (p,n))) . k) in ( rng ( Ant g1)) by A32, CALCUL_1: 5;

          (i + 1) <= ( len h) by A6, A25, NAT_1: 13;

          then (i + 1) in ( dom h) by A20, FINSEQ_3: 25;

          then (i + 1) in ( dom g) by FINSEQ_5: 57;

          

          then p1 = (g . ((( len g) - (i + 1)) + 1)) by A26, FINSEQ_5: 58

          .= (g . (( len g) - i));

          then p1 = ((f ^ ( IdFinS (p,n))) . k) by A31, FINSEQ_1: 21, A18;

          then ex j1 be Nat st j1 in ( dom ( Ant g1)) & (( Ant g1) . j1) = p1 by A33, FINSEQ_2: 10;

          then ( Suc g1) is_tail_of ( Ant g1) by A29, CALCUL_1:def 16;

          then

           A34: |- g1 by CALCUL_1: 33;

          take q1;

          (k + 1) in ( dom H) by A13, A14, FINSEQ_3: 25;

          then i = ((( len F) - (k + 1)) + 1) & (k + 1) in ( dom F) by FINSEQ_5: 57;

          then

           A35: q1 = (H . (k + 1)) by A27, FINSEQ_5: 58;

          k in ( dom H) by A22, A16, FINSEQ_3: 25;

          then k in ( dom F) by FINSEQ_5: 57;

          then pk = (p1 => q1) by A23, A28, FINSEQ_5: 58;

          then |- ((f ^ <*p*>) ^ <*q1*>) by A24, A34, CALCUL_1: 56;

          hence thesis by A35;

        end;

        now

          ( len H) = ( len h) by A6, FINSEQ_5:def 3;

          then

           A36: 1 in ( dom H) by A4, FINSEQ_3: 25;

          then

          reconsider p1 = (H . 1) as Element of ( CQC-WFF Al) by FINSEQ_2: 11;

          assume

           A37: k = 0 ;

          take p1;

          1 in ( dom F) by A36, FINSEQ_5: 57;

          

          then p1 = (F . ((( len F) - 1) + 1)) by FINSEQ_5: 58

          .= ( Impl h) by A5, A6;

          hence thesis by A10, A37;

        end;

        hence thesis by A15;

      end;

      

       A38: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A38, A11);

      then

      consider p1 such that

       A39: p1 = (H . ( len H)) and

       A40: |- ((f ^ <*p*>) ^ <*p1*>) by A9;

      p1 = (H . ( len F)) by A39, FINSEQ_5:def 3;

      then p1 = ( Begin h) by A3, A7, FINSEQ_5: 62, FINSEQ_5:def 3;

      then p1 = (h . 1) by A4, Def3;

      then p1 = (g . ( len g)) by FINSEQ_5: 62;

      then p1 = (g . (( len (f ^ ( IdFinS (p,n)))) + ( len <*q*>))) by FINSEQ_1: 22;

      then p1 = (g . (( len (f ^ ( IdFinS (p,n)))) + 1)) by FINSEQ_1: 39;

      hence thesis by A40, FINSEQ_1: 42;

    end;