calcul_1.miz



    begin

    reserve Al for QC-alphabet;

    reserve a,b,c,d for object,

i,j,k,m,n for Nat,

p,q,r for Element of ( CQC-WFF Al),

x,y,y0 for bound_QC-variable of Al,

X for Subset of ( CQC-WFF Al),

A for non empty set,

J for interpretation of Al, A,

v,w for Element of ( Valuations_in (Al,A)),

Sub for CQC_Substitution of Al,

f,f1,g,h,h1 for FinSequence of ( CQC-WFF Al);

    definition

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

      :: CALCUL_1:def1

      func Ant (f) -> FinSequence of D means

      : Def1: for i st ( len f) = (i + 1) holds it = (f | ( Seg i)) if ( len f) > 0

      otherwise it = {} ;

      existence

      proof

        

         A1: ( len f) > 0 implies ex g be FinSequence of D st for i st ( len f) = (i + 1) holds g = (f | ( Seg i))

        proof

          assume ( len f) > 0 ;

          then

          consider j be Nat such that

           A2: ( len f) = (j + 1) by NAT_1: 6;

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

          take g = (f | ( Seg j));

          reconsider g as FinSequence by FINSEQ_1: 15;

          now

            

             A3: ( rng g) c= ( rng f) by RELAT_1: 70;

            let a be object;

            assume a in ( rng g);

            then a in ( rng f) by A3;

            hence a in D;

          end;

          then ( rng g) c= D;

          then

          reconsider g as FinSequence of D by FINSEQ_1:def 4;

          for i st ( len f) = (i + 1) holds g = (f | ( Seg i)) by A2;

          hence thesis;

        end;

        ( <*> D) = {} ;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let g,h be FinSequence of D;

        ( len f) > 0 & (for i st ( len f) = (i + 1) holds g = (f | ( Seg i))) & (for i st ( len f) = (i + 1) holds h = (f | ( Seg i))) implies g = h

        proof

          assume that

           A4: ( len f) > 0 and

           A5: for i st ( len f) = (i + 1) holds g = (f | ( Seg i)) and

           A6: for i st ( len f) = (i + 1) holds h = (f | ( Seg i));

          consider j be Nat such that

           A7: ( len f) = (j + 1) by A4, NAT_1: 6;

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

          g = (f | ( Seg j)) by A5, A7;

          hence thesis by A6, A7;

        end;

        hence thesis;

      end;

      consistency ;

    end

    definition

      let Al;

      let f be FinSequence of ( CQC-WFF Al);

      :: CALCUL_1:def2

      func Suc (f) -> Element of ( CQC-WFF Al) equals

      : Def2: (f . ( len f)) if ( len f) > 0

      otherwise ( VERUM Al);

      coherence

      proof

        per cases ;

          suppose ( len f) > 0 ;

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

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

          then (f . ( len f)) in ( rng f) by FUNCT_1: 3;

          hence thesis;

        end;

          suppose

           A1: not ( len f) > 0 ;

          thus thesis by A1;

        end;

      end;

      consistency ;

    end

    definition

      let f be Relation, p be set;

      :: CALCUL_1:def3

      pred p is_tail_of f means p in ( rng f);

    end

     Lm1:

    now

      let f be FinSequence, p be set;

      assume p is_tail_of f;

      then p in ( rng f);

      then

      consider i be object such that

       A1: i in ( dom f) and

       A2: (f . i) = p by FUNCT_1:def 3;

      reconsider i as Nat by A1;

      take i;

      thus i in ( dom f) & (f . i) = p by A1, A2;

    end;

    

     Lm2: for f be FinSequence, p be set st ex i be Element of NAT st i in ( dom f) & (f . i) = p holds p is_tail_of f by FUNCT_1:def 3;

    definition

      let Al, f, g;

      :: CALCUL_1:def4

      pred f is_Subsequence_of g means ex N be Subset of NAT st f c= ( Seq (g | N));

    end

    theorem :: CALCUL_1:1

    

     Th1: f is_Subsequence_of g implies ( rng f) c= ( rng g) & ex N be Subset of NAT st ( rng f) c= ( rng (g | N))

    proof

      assume f is_Subsequence_of g;

      then

      consider N be Subset of NAT such that

       A1: f c= ( Seq (g | N));

      

       A2: ( rng (g | N)) c= ( rng g) by RELAT_1: 70;

       A3:

      now

        ( rng ( Seq (g | N))) = ( rng ((g | N) * ( Sgm ( dom (g | N))))) by FINSEQ_1:def 14;

        then

         A4: ( rng ( Seq (g | N))) c= ( rng (g | N)) by RELAT_1: 26;

        let a be object;

        assume a in ( rng f);

        then

        consider n be Nat such that

         A5: n in ( dom f) and

         A6: (f . n) = a by FINSEQ_2: 10;

         [n, (f . n)] in f by A5, FUNCT_1: 1;

        then

         A7: (( Seq (g | N)) . n) = a by A1, A6, FUNCT_1: 1;

        ( dom f) c= ( dom ( Seq (g | N))) by A1, RELAT_1: 11;

        then a in ( rng ( Seq (g | N))) by A5, A7, FUNCT_1: 3;

        hence a in ( rng (g | N)) by A4;

      end;

      then ( rng f) c= ( rng (g | N));

      hence ( rng f) c= ( rng g) by A2;

      take N;

      thus thesis by A3;

    end;

    theorem :: CALCUL_1:2

    

     Th2: ( len f) > 0 implies (( len ( Ant f)) + 1) = ( len f) & ( len ( Ant f)) < ( len f)

    proof

      assume ( len f) > 0 ;

      then

      consider i be Nat such that

       A1: ( len f) = (i + 1) by NAT_1: 6;

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

      ( Ant f) = (f | ( Seg i)) by A1, Def1;

      then ( dom ( Ant f)) = (( dom f) /\ ( Seg i)) by RELAT_1: 61;

      then ( Seg ( len ( Ant f))) = (( dom f) /\ ( Seg i)) by FINSEQ_1:def 3;

      then

       A2: ( Seg ( len ( Ant f))) = (( Seg ( len f)) /\ ( Seg i)) by FINSEQ_1:def 3;

      i <= ( len f) by A1, NAT_1: 11;

      then

       A3: ( Seg i) c= ( Seg ( len f)) by FINSEQ_1: 5;

      hence (( len ( Ant f)) + 1) = ( len f) by A1, A2, FINSEQ_1: 6, XBOOLE_1: 28;

      ( len ( Ant f)) = i by A2, A3, FINSEQ_1: 6, XBOOLE_1: 28;

      hence thesis by A1, NAT_1: 13;

    end;

    theorem :: CALCUL_1:3

    

     Th3: ( len f) > 0 implies f = (( Ant f) ^ <*( Suc f)*>) & ( rng f) = (( rng ( Ant f)) \/ {( Suc f)})

    proof

      assume

       A1: ( len f) > 0 ;

      then

       A2: ( len f) = (( len ( Ant f)) + 1) by Th2;

      

       A3: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

       A4:

      now

        let j be Nat such that

         A5: j in ( dom f);

        

         A6: 1 <= j by A3, A5, FINSEQ_1: 1;

         A7:

        now

          assume j <= ( len ( Ant f));

          then

           A8: j in ( dom ( Ant f)) by A6, FINSEQ_3: 25;

          ( Ant f) = (f | ( Seg ( len ( Ant f)))) by A2, Def1;

          then ( Ant f) = (f | ( dom ( Ant f))) by FINSEQ_1:def 3;

          then (f . j) = (( Ant f) . j) by A8, FUNCT_1: 49;

          hence (f . j) = ((( Ant f) ^ <*( Suc f)*>) . j) by A8, FINSEQ_1:def 7;

        end;

         A9:

        now

          1 in ( Seg 1) by FINSEQ_1: 1;

          then

           A10: 1 in ( dom <*( Suc f)*>) by FINSEQ_1: 38;

          assume

           A11: j = (( len ( Ant f)) + 1);

          then j = ( len f) by A1, Th2;

          then (f . j) = ( Suc f) by A1, Def2;

          then (f . j) = ( <*( Suc f)*> . 1) by FINSEQ_1: 40;

          hence (f . j) = ((( Ant f) ^ <*( Suc f)*>) . j) by A11, A10, FINSEQ_1:def 7;

        end;

        j <= (( len ( Ant f)) + 1) by A2, A3, A5, FINSEQ_1: 1;

        hence (f . j) = ((( Ant f) ^ <*( Suc f)*>) . j) by A7, A9, NAT_1: 8;

      end;

      ( len f) = (( len ( Ant f)) + ( len <*( Suc f)*>)) by A2, FINSEQ_1: 39;

      then

       A12: ( len f) = ( len (( Ant f) ^ <*( Suc f)*>)) by FINSEQ_1: 22;

      then f = (( Ant f) ^ <*( Suc f)*>) by A4, FINSEQ_2: 9;

      then ( rng f) = (( rng ( Ant f)) \/ ( rng <*( Suc f)*>)) by FINSEQ_1: 31;

      hence thesis by A12, A4, FINSEQ_1: 38, FINSEQ_2: 9;

    end;

    theorem :: CALCUL_1:4

    

     Th4: ( len f) > 1 implies ( len ( Ant f)) > 0

    proof

      assume ( len f) > 1;

      then (( len ( Ant f)) + 1) > 1 by Th2;

      hence thesis by NAT_1: 13;

    end;

    theorem :: CALCUL_1:5

    

     Th5: ( Suc (f ^ <*p*>)) = p & ( Ant (f ^ <*p*>)) = f

    proof

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

      

       A1: ( len fin) = (( len f) + 1) by FINSEQ_2: 16;

      then (fin . ( len fin)) = p by FINSEQ_1: 42;

      hence ( Suc (f ^ <*p*>)) = p by Def2;

      thus ( Ant (f ^ <*p*>)) = f

      proof

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

        now

          let a be object;

          assume a in f;

          then

          consider k be Nat such that

           A2: k in ( dom f) and

           A3: a = [k, (f . k)] by FINSEQ_1: 12;

          k in ( dom fin) & (f . k) = (fin . k) by A2, FINSEQ_1:def 7, FINSEQ_2: 15;

          hence a in fin by A3, FUNCT_1: 1;

        end;

        then f c= fin;

        then f = (fin | ( dom f)) by GRFUNC_1: 23;

        then f = (fin | ( Seg ( len f))) by FINSEQ_1:def 3;

        hence thesis by A1, Def1;

      end;

    end;

    reserve fin,fin1 for FinSequence;

    theorem :: CALCUL_1:6

    

     Th6: ( len fin) <= ( len (fin ^ fin1)) & ( len fin1) <= ( len (fin ^ fin1)) & (fin <> {} implies 1 <= ( len fin) & ( len fin1) < ( len (fin1 ^ fin)))

    proof

      ( len (fin ^ fin1)) = (( len fin) + ( len fin1)) by FINSEQ_1: 22;

      hence ( len fin) <= ( len (fin ^ fin1)) & ( len fin1) <= ( len (fin ^ fin1)) by NAT_1: 12;

      assume fin <> {} ;

      then

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

      then (( len fin1) + 1) <= (( len fin) + ( len fin1)) by XREAL_1: 6;

      then (( len fin1) + 1) <= ( len (fin1 ^ fin)) by FINSEQ_1: 22;

      hence thesis by A1, NAT_1: 13;

    end;

    theorem :: CALCUL_1:7

    

     Th7: ( Seq ((f ^ g) | ( dom f))) = ((f ^ g) | ( dom f))

    proof

      ((f ^ g) | ( dom f)) = f by FINSEQ_1: 21;

      hence thesis by FINSEQ_3: 116;

    end;

    theorem :: CALCUL_1:8

    

     Th8: f is_Subsequence_of (f ^ g)

    proof

      set a = ( len f);

      take N = ( Seg a);

      reconsider f1 = ((f ^ g) | N) as FinSequence by FINSEQ_1: 15;

      

       A1: N = ( dom f) by FINSEQ_1:def 3;

      then f c= f1 by FINSEQ_1: 21;

      hence thesis by A1, Th7;

    end;

    theorem :: CALCUL_1:9

    

     Th9: 1 < ( len ((fin ^ <*b*>) ^ <*c*>))

    proof

      ( len ((fin ^ <*b*>) ^ <*c*>)) = (( len (fin ^ <*b*>)) + ( len <*c*>)) by FINSEQ_1: 22;

      then ( len ((fin ^ <*b*>) ^ <*c*>)) = (( len (fin ^ <*b*>)) + 1) by FINSEQ_1: 39;

      then ( len ((fin ^ <*b*>) ^ <*c*>)) = ((( len fin) + ( len <*b*>)) + 1) by FINSEQ_1: 22;

      then ( len ((fin ^ <*b*>) ^ <*c*>)) = ((( len fin) + 1) + 1) by FINSEQ_1: 39;

      then ( len ((fin ^ <*b*>) ^ <*c*>)) = (( len fin) + (1 + 1));

      then (1 + 1) <= ( len ((fin ^ <*b*>) ^ <*c*>)) by NAT_1: 11;

      hence thesis by NAT_1: 13;

    end;

    theorem :: CALCUL_1:10

    

     Th10: 1 <= ( len (fin ^ <*b*>)) & ( len (fin ^ <*b*>)) in ( dom (fin ^ <*b*>))

    proof

      ( len (fin ^ <*b*>)) = (( len fin) + 1) by FINSEQ_2: 16;

      then 1 <= ( len (fin ^ <*b*>)) by NAT_1: 11;

      hence thesis by FINSEQ_3: 25;

    end;

    theorem :: CALCUL_1:11

    

     Th11: 0 < m implies ( len ( Sgm (( Seg n) \/ {(n + m)}))) = (n + 1)

    proof

      

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

      assume

       A2: 0 < m;

      then ( card (( Seg n) \/ {(n + m)})) = (( card ( Seg n)) + 1) by CARD_2: 41, FINSEQ_3: 10;

      then

       A3: ( card (( Seg n) \/ {(n + m)})) = (n + 1) by FINSEQ_1: 57;

      ( 0 + 1) <= m by A2, NAT_1: 13;

      then 1 <= (m + n) by A1, XXREAL_0: 2;

      then (n + m) in ( Seg (n + m)) by FINSEQ_1: 1;

      then

       A4: {(n + m)} c= ( Seg (n + m)) by ZFMISC_1: 31;

      ( Seg n) c= ( Seg (n + m)) by FINSEQ_3: 18;

      hence thesis by A3, A4, FINSEQ_3: 39, XBOOLE_1: 8;

    end;

    theorem :: CALCUL_1:12

    

     Th12: 0 < m implies ( dom ( Sgm (( Seg n) \/ {(n + m)}))) = ( Seg (n + 1))

    proof

      assume 0 < m;

      then ( len ( Sgm (( Seg n) \/ {(n + m)}))) = (n + 1) by Th11;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: CALCUL_1:13

    

     Th13: 0 < ( len f) implies f is_Subsequence_of ((( Ant f) ^ g) ^ <*( Suc f)*>)

    proof

      set n = ( len ( Ant f));

      set m = ( len g);

      set N = (( Seg n) \/ {(n + (m + 1))});

      set f1 = ((( Ant f) ^ g) ^ <*( Suc f)*>);

      reconsider f2 = (f1 | N) as FinSubsequence;

      assume

       A1: 0 < ( len f);

      take N;

      now

        now

          let b be object such that

           A2: b in N;

          reconsider i = b as Element of NAT by A2;

           A3:

          now

            assume i in {(n + (m + 1))};

            then

             A4: i = ((n + m) + 1) by TARSKI:def 1;

            then

             A5: 1 <= i by NAT_1: 11;

            ( len f1) = (( len (( Ant f) ^ g)) + ( len <*( Suc f)*>)) by FINSEQ_1: 22;

            then ( len f1) = ((n + m) + ( len <*( Suc f)*>)) by FINSEQ_1: 22;

            then i <= ( len f1) by A4, FINSEQ_1: 39;

            hence i in ( dom f1) by A5, FINSEQ_3: 25;

          end;

          now

            f1 = (( Ant f) ^ (g ^ <*( Suc f)*>)) by FINSEQ_1: 32;

            then

             A6: n <= ( len f1) by Th6;

            assume

             A7: i in ( Seg n);

            then

             A8: 1 <= i by FINSEQ_1: 1;

            i <= n by A7, FINSEQ_1: 1;

            then i <= ( len f1) by A6, XXREAL_0: 2;

            hence i in ( dom f1) by A8, FINSEQ_3: 25;

          end;

          hence b in ( dom f1) by A2, A3, XBOOLE_0:def 3;

        end;

        then

         A9: N c= ( dom f1);

        ( dom f2) = (( dom f1) /\ N) by RELAT_1: 61;

        then

         A10: ( dom f2) = N by A9, XBOOLE_1: 28;

        then

         A11: ( dom ( Sgm ( dom f2))) = ( Seg (n + 1)) by Th12;

        now

          let i;

          i in ( dom f) iff 1 <= i & i <= ( len f) by FINSEQ_3: 25;

          then i in ( dom f) iff 1 <= i & i <= (n + 1) by A1, Th2;

          hence i in ( dom f) iff i in ( Seg (n + 1)) by FINSEQ_1: 1;

        end;

        then for b be object holds b in ( dom f) iff b in ( Seg (n + 1));

        then

         A12: ( dom ( Sgm ( dom f2))) = ( dom f) by A11, TARSKI: 2;

         A13:

        now

          let i, j such that

           A14: i in ( Seg n) and

           A15: j in {(n + (m + 1))};

          

           A16: i <= n by A14, FINSEQ_1: 1;

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

          then n < (n + (m + 1)) by NAT_1: 13;

          then n < j by A15, TARSKI:def 1;

          hence i < j by A16, XXREAL_0: 2;

        end;

        let b be object such that

         A17: b in f;

        consider c,d be object such that

         A18: b = [c, d] by A17, RELAT_1:def 1;

        

         A19: c in ( dom f) by A17, A18, FUNCT_1: 1;

        then

        reconsider i = c as Element of NAT ;

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

        then 1 <= (n + (m + 1)) by XXREAL_0: 2;

        then (n + (m + 1)) in ( Seg (n + (m + 1))) by FINSEQ_1: 1;

        then {(n + (m + 1))} c= ( Seg (n + (m + 1))) by ZFMISC_1: 31;

        then ( Sgm ( dom f2)) = (( Sgm ( Seg n)) ^ ( Sgm {(n + (m + 1))})) by A10, A13, FINSEQ_3: 42;

        then ( Sgm ( dom f2)) = (( Sgm ( Seg n)) ^ <*(n + (m + 1))*>) by FINSEQ_3: 44;

        then

         A20: ( Sgm ( dom f2)) = (( idseq n) ^ <*(n + (m + 1))*>) by FINSEQ_3: 48;

         A21:

        now

          assume

           A22: i in ( Seg n);

          then

           A23: i in ( dom ( Ant f)) by FINSEQ_1:def 3;

          i in ( dom ( idseq n)) by A22;

          then (( Sgm ( dom f2)) . i) = (( idseq n) . i) by A20, FINSEQ_1:def 7;

          then

           A24: (( Sgm ( dom f2)) . i) = i by A22, FUNCT_1: 18;

          i in ( dom ( Sgm ( dom f2))) & ( Seq f2) = (f2 * ( Sgm ( dom f2))) by A17, A18, A12, FINSEQ_1:def 14, FUNCT_1: 1;

          then (( Seq f2) . i) = (f2 . i) by A24, FUNCT_1: 13;

          then (( Seq f2) . i) = ((f2 | ( Seg n)) . i) by A22, FUNCT_1: 49;

          then

           A25: (( Seq f2) . i) = ((f1 | ( Seg n)) . i) by RELAT_1: 74, XBOOLE_1: 7;

          f1 = (( Ant f) ^ (g ^ <*( Suc f)*>)) & ( Seg ( len ( Ant f))) = ( dom ( Ant f)) by FINSEQ_1: 32, FINSEQ_1:def 3;

          then

           A26: (( Seq f2) . i) = (( Ant f) . i) by A25, FINSEQ_1: 21;

          f = (( Ant f) ^ <*( Suc f)*>) by A1, Th3;

          hence (( Seq f2) . i) = (f . i) by A26, A23, FINSEQ_1:def 7;

        end;

        ( rng ( Sgm ( dom (f1 | N)))) = ( dom (f1 | N)) by FINSEQ_1: 50;

        then ( dom f) = ( dom ((f1 | N) * ( Sgm ( dom (f1 | N))))) by A12, RELAT_1: 27;

        then

         A27: ( dom f) = ( dom ( Seq f2)) by FINSEQ_1:def 14;

         A28:

        now

          1 in ( Seg 1) by FINSEQ_1: 1;

          then

           A29: ( len (( Ant f) ^ g)) = (n + m) & 1 in ( dom <*( Suc f)*>) by FINSEQ_1: 22, FINSEQ_1: 38;

          

           A30: i in ( dom ( Sgm ( dom f2))) & ( Seq f2) = (f2 * ( Sgm ( dom f2))) by A17, A18, A12, FINSEQ_1:def 14, FUNCT_1: 1;

          assume

           A31: i = (n + 1);

          ( len ( idseq n)) = n by CARD_1:def 7;

          then (( Sgm ( dom f2)) . i) = (n + (m + 1)) by A20, A31, FINSEQ_1: 42;

          then

           A32: (( Seq f2) . i) = (f2 . (n + (m + 1))) by A30, FUNCT_1: 13;

          (n + (m + 1)) in {(n + (m + 1))} & {(n + (m + 1))} c= N by TARSKI:def 1, XBOOLE_1: 7;

          then (( Seq f2) . i) = (f1 . ((n + m) + 1)) by A32, FUNCT_1: 49;

          then

           A33: (( Seq f2) . i) = ( <*( Suc f)*> . 1) by A29, FINSEQ_1:def 7;

          (f . i) = (f . ( len f)) by A1, A31, Th2;

          then (f . i) = ( Suc f) by A1, Def2;

          hence (( Seq f2) . i) = (f . i) by A33, FINSEQ_1: 40;

        end;

        d = (f . c) by A17, A18, FUNCT_1: 1;

        hence b in ( Seq f2) by A18, A19, A11, A12, A21, A28, A27, FINSEQ_2: 7, FUNCT_1: 1;

      end;

      hence thesis;

    end;

    theorem :: CALCUL_1:14

    

     Th14: 1 in ( dom <*c, d*>) & 2 in ( dom <*c, d*>) & ((f ^ <*c, d*>) . (( len f) + 1)) = c & ((f ^ <*c, d*>) . (( len f) + 2)) = d

    proof

      

       A1: 2 <= ( len <*c, d*>) by FINSEQ_1: 44;

      then 2 in ( dom <*c, d*>) by FINSEQ_3: 25;

      then

       A2: ((f ^ <*c, d*>) . (( len f) + 2)) = ( <*c, d*> . 2) by FINSEQ_1:def 7;

      1 <= 2;

      then

       A3: 1 <= ( len <*c, d*>) by FINSEQ_1: 44;

      then 1 in ( dom <*c, d*>) by FINSEQ_3: 25;

      then ((f ^ <*c, d*>) . (( len f) + 1)) = ( <*c, d*> . 1) by FINSEQ_1:def 7;

      hence thesis by A3, A1, A2, FINSEQ_1: 44, FINSEQ_3: 25;

    end;

    begin

    definition

      let Al, f;

      :: CALCUL_1:def5

      func still_not-bound_in f -> Subset of ( bound_QC-variables Al) means

      : Def5: a in it iff ex i, p st i in ( dom f) & p = (f . i) & a in ( still_not-bound_in p);

      existence

      proof

        defpred P[ object] means ex i, p st i in ( dom f) & p = (f . i) & $1 in ( still_not-bound_in p);

        consider X be set such that

         A1: for a be object holds a in X iff a in ( bound_QC-variables Al) & P[a] from XBOOLE_0:sch 1;

        take X;

        for a be object st a in X holds a in ( bound_QC-variables Al) by A1;

        hence X is Subset of ( bound_QC-variables Al) by TARSKI:def 3;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X,Y be Subset of ( bound_QC-variables Al);

        assume that

         A2: for a holds a in X iff ex i, p st i in ( dom f) & p = (f . i) & a in ( still_not-bound_in p) and

         A3: for a holds a in Y iff ex i, p st i in ( dom f) & p = (f . i) & a in ( still_not-bound_in p);

        now

          let a be object;

          a in X iff ex i, p st i in ( dom f) & p = (f . i) & a in ( still_not-bound_in p) by A2;

          hence a in X iff a in Y by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let Al;

      :: CALCUL_1:def6

      func set_of_CQC-WFF-seq (Al) -> set means

      : Def6: a in it iff a is FinSequence of ( CQC-WFF Al);

      existence

      proof

        defpred P[ object] means $1 is FinSequence of ( CQC-WFF Al);

        consider X be set such that

         A1: for a be object holds a in X iff a in ( bool [: NAT , ( CQC-WFF Al):]) & P[a] from XBOOLE_0:sch 1;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X,Y be set such that

         A2: a in X iff a is FinSequence of ( CQC-WFF Al) and

         A3: a in Y iff a is FinSequence of ( CQC-WFF Al);

        now

          let a be object;

          a in X iff a is FinSequence of ( CQC-WFF Al) by A2;

          hence a in X iff a in Y by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    reserve PR,PR1 for FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

    definition

      let Al, PR;

      let n be Nat;

      :: CALCUL_1:def7

      pred PR,n is_a_correct_step means

      : Def7: ex f st ( Suc f) is_tail_of ( Ant f) & ((PR . n) `1 ) = f if ((PR . n) `2 ) = 0 ,

ex f st ((PR . n) `1 ) = (f ^ <*( VERUM Al)*>) if ((PR . n) `2 ) = 1,

ex i, f, g st 1 <= i & i < n & ( Ant f) is_Subsequence_of ( Ant g) & ( Suc f) = ( Suc g) & ((PR . i) `1 ) = f & ((PR . n) `1 ) = g if ((PR . n) `2 ) = 2,

ex i, j, f, g st 1 <= i & i < n & 1 <= j & j < i & ( len f) > 1 & ( len g) > 1 & ( Ant ( Ant f)) = ( Ant ( Ant g)) & ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant g)) & ( Suc f) = ( Suc g) & f = ((PR . j) `1 ) & g = ((PR . i) `1 ) & (( Ant ( Ant f)) ^ <*( Suc f)*>) = ((PR . n) `1 ) if ((PR . n) `2 ) = 3,

ex i, j, f, g, p st 1 <= i & i < n & 1 <= j & j < i & ( len f) > 1 & ( Ant f) = ( Ant g) & ( Suc ( Ant f)) = ( 'not' p) & ( 'not' ( Suc f)) = ( Suc g) & f = ((PR . j) `1 ) & g = ((PR . i) `1 ) & (( Ant ( Ant f)) ^ <*p*>) = ((PR . n) `1 ) if ((PR . n) `2 ) = 4,

ex i, j, f, g st 1 <= i & i < n & 1 <= j & j < i & ( Ant f) = ( Ant g) & f = ((PR . j) `1 ) & g = ((PR . i) `1 ) & (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>) = ((PR . n) `1 ) if ((PR . n) `2 ) = 5,

ex i, f, p, q st 1 <= i & i < n & (p '&' q) = ( Suc f) & f = ((PR . i) `1 ) & (( Ant f) ^ <*p*>) = ((PR . n) `1 ) if ((PR . n) `2 ) = 6,

ex i, f, p, q st 1 <= i & i < n & (p '&' q) = ( Suc f) & f = ((PR . i) `1 ) & (( Ant f) ^ <*q*>) = ((PR . n) `1 ) if ((PR . n) `2 ) = 7,

ex i, f, p, x, y st 1 <= i & i < n & ( Suc f) = ( All (x,p)) & f = ((PR . i) `1 ) & (( Ant f) ^ <*(p . (x,y))*>) = ((PR . n) `1 ) if ((PR . n) `2 ) = 8,

ex i, f, p, x, y st 1 <= i & i < n & ( Suc f) = (p . (x,y)) & not y in ( still_not-bound_in ( Ant f)) & not y in ( still_not-bound_in ( All (x,p))) & f = ((PR . i) `1 ) & (( Ant f) ^ <*( All (x,p))*>) = ((PR . n) `1 ) if ((PR . n) `2 ) = 9;

      consistency ;

    end

    definition

      let Al, PR;

      :: CALCUL_1:def8

      attr PR is a_proof means PR <> {} & for n be Nat st 1 <= n & n <= ( len PR) holds (PR,n) is_a_correct_step ;

    end

    definition

      let Al, f;

      :: CALCUL_1:def9

      pred |- f means ex PR st PR is a_proof & f = ((PR . ( len PR)) `1 );

    end

    definition

      let Al, p, X;

      :: CALCUL_1:def10

      pred p is_formal_provable_from X means ex f st ( rng ( Ant f)) c= X & ( Suc f) = p & |- f;

    end

    definition

      let Al, X, A, J, v;

      :: CALCUL_1:def11

      pred J,v |= X means p in X implies (J,v) |= p;

    end

    definition

      let Al, X, p;

      :: CALCUL_1:def12

      pred X |= p means (J,v) |= X implies (J,v) |= p;

    end

    definition

      let Al, p;

      :: CALCUL_1:def13

      pred |= p means ( {} ( CQC-WFF Al)) |= p;

    end

    definition

      let Al, f, A, J, v;

      :: CALCUL_1:def14

      pred J,v |= f means (J,v) |= ( rng f);

    end

    definition

      let Al, f, p;

      :: CALCUL_1:def15

      pred f |= p means (J,v) |= f implies (J,v) |= p;

    end

    theorem :: CALCUL_1:15

    

     Th15: ( Suc f) is_tail_of ( Ant f) implies ( Ant f) |= ( Suc f)

    proof

      assume ( Suc f) is_tail_of ( Ant f);

      then ex i st i in ( dom ( Ant f)) & (( Ant f) . i) = ( Suc f) by Lm1;

      then

       A1: ( Suc f) in ( rng ( Ant f)) by FUNCT_1: 3;

      let A, J, v;

      assume (J,v) |= ( rng ( Ant f));

      hence thesis by A1;

    end;

    theorem :: CALCUL_1:16

    

     Th16: ( Ant f) is_Subsequence_of ( Ant g) & ( Suc f) = ( Suc g) & ( Ant f) |= ( Suc f) implies ( Ant g) |= ( Suc g)

    proof

      assume that

       A1: ( Ant f) is_Subsequence_of ( Ant g) and

       A2: ( Suc f) = ( Suc g) & ( Ant f) |= ( Suc f);

      let A, J, v such that

       A3: (J,v) |= ( rng ( Ant g));

      now

        let p;

        assume

         A4: p in ( rng ( Ant f));

        ( rng ( Ant f)) c= ( rng ( Ant g)) by A1, Th1;

        hence (J,v) |= p by A3, A4;

      end;

      then (J,v) |= ( rng ( Ant f));

      then (J,v) |= ( Ant f);

      hence thesis by A2;

    end;

    theorem :: CALCUL_1:17

    

     Th17: ( len f) > 0 implies ((J,v) |= ( Ant f) & (J,v) |= ( Suc f) iff (J,v) |= f)

    proof

      assume

       A1: ( len f) > 0 ;

      thus (J,v) |= ( Ant f) & (J,v) |= ( Suc f) implies (J,v) |= f

      proof

        assume that

         A2: (J,v) |= ( Ant f) and

         A3: (J,v) |= ( Suc f);

        let p;

        assume p in ( rng f);

        then p in (( rng ( Ant f)) \/ {( Suc f)}) by A1, Th3;

        then

         A4: p in ( rng ( Ant f)) or p in {( Suc f)} by XBOOLE_0:def 3;

        (J,v) |= ( rng ( Ant f)) by A2;

        hence thesis by A3, A4, TARSKI:def 1;

      end;

      thus (J,v) |= f implies (J,v) |= ( Ant f) & (J,v) |= ( Suc f)

      proof

        assume

         A5: (J,v) |= ( rng f);

        thus (J,v) |= ( rng ( Ant f))

        proof

          

           A6: ( rng ( Ant f)) c= (( rng ( Ant f)) \/ {( Suc f)}) by XBOOLE_1: 7;

          let p;

          assume p in ( rng ( Ant f));

          then p in (( rng ( Ant f)) \/ {( Suc f)}) by A6;

          then p in ( rng f) by A1, Th3;

          hence thesis by A5;

        end;

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

        then

         A7: ( len f) in ( dom f) by FINSEQ_3: 25;

        ( Suc f) = (f . ( len f)) by A1, Def2;

        then ( Suc f) in ( rng f) by A7, FUNCT_1: 3;

        hence (J,v) |= ( Suc f) by A5;

      end;

    end;

    theorem :: CALCUL_1:18

    

     Th18: ( len f) > 1 & ( len g) > 1 & ( Ant ( Ant f)) = ( Ant ( Ant g)) & ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant g)) & ( Suc f) = ( Suc g) & ( Ant f) |= ( Suc f) & ( Ant g) |= ( Suc g) implies ( Ant ( Ant f)) |= ( Suc f)

    proof

      assume that

       A1: ( len f) > 1 and

       A2: ( len g) > 1 and

       A3: ( Ant ( Ant f)) = ( Ant ( Ant g)) and

       A4: ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant g)) and

       A5: ( Suc f) = ( Suc g) and

       A6: ( Ant f) |= ( Suc f) and

       A7: ( Ant g) |= ( Suc g);

      let A, J, v such that

       A8: (J,v) |= ( Ant ( Ant f));

      

       A9: ( len ( Ant g)) > 0 by A2, Th4;

       A10:

      now

        assume not (J,v) |= ( Suc ( Ant f));

        then (J,v) |= ( Suc ( Ant g)) by A4, VALUAT_1: 17;

        then (J,v) |= ( Ant g) by A3, A9, A8, Th17;

        hence thesis by A5, A7;

      end;

      

       A11: ( len ( Ant f)) > 0 by A1, Th4;

      now

        assume (J,v) |= ( Suc ( Ant f));

        then (J,v) |= ( Ant f) by A11, A8, Th17;

        hence thesis by A6;

      end;

      hence thesis by A10;

    end;

    theorem :: CALCUL_1:19

    

     Th19: ( len f) > 1 & ( Ant f) = ( Ant g) & ( 'not' p) = ( Suc ( Ant f)) & ( 'not' ( Suc f)) = ( Suc g) & ( Ant f) |= ( Suc f) & ( Ant g) |= ( Suc g) implies ( Ant ( Ant f)) |= p

    proof

      assume that

       A1: ( len f) > 1 and

       A2: ( Ant f) = ( Ant g) and

       A3: ( 'not' p) = ( Suc ( Ant f)) and

       A4: ( 'not' ( Suc f)) = ( Suc g) & ( Ant f) |= ( Suc f) & ( Ant g) |= ( Suc g);

      

       A5: ( len ( Ant f)) > 0 by A1, Th4;

       A6:

      now

        given A, J, v such that

         A7: (J,v) |= ( Ant f);

        (J,v) |= ( Suc f) & (J,v) |= ( 'not' ( Suc f)) by A2, A4, A7;

        hence contradiction by VALUAT_1: 17;

      end;

      let A, J, v such that

       A8: (J,v) |= ( Ant ( Ant f));

      now

        assume (J,v) |= ( Suc ( Ant f));

        then (J,v) |= ( Ant f) by A5, A8, Th17;

        hence contradiction by A6;

      end;

      hence thesis by A3, VALUAT_1: 17;

    end;

    theorem :: CALCUL_1:20

    

     Th20: ( Ant f) = ( Ant g) & ( Ant f) |= ( Suc f) & ( Ant g) |= ( Suc g) implies ( Ant f) |= (( Suc f) '&' ( Suc g))

    proof

      assume

       A1: ( Ant f) = ( Ant g) & ( Ant f) |= ( Suc f) & ( Ant g) |= ( Suc g);

      let A, J, v;

      assume (J,v) |= ( Ant f);

      then (J,v) |= ( Suc f) & (J,v) |= ( Suc g) by A1;

      hence thesis by VALUAT_1: 18;

    end;

    theorem :: CALCUL_1:21

    

     Th21: ( Ant f) |= (p '&' q) implies ( Ant f) |= p

    proof

      assume

       A1: ( Ant f) |= (p '&' q);

      let A, J, v;

      assume (J,v) |= ( Ant f);

      then (J,v) |= (p '&' q) by A1;

      hence thesis by VALUAT_1: 18;

    end;

    theorem :: CALCUL_1:22

    

     Th22: ( Ant f) |= (p '&' q) implies ( Ant f) |= q

    proof

      assume

       A1: ( Ant f) |= (p '&' q);

      let A, J, v;

      assume (J,v) |= ( Ant f);

      then (J,v) |= (p '&' q) by A1;

      hence thesis by VALUAT_1: 18;

    end;

    theorem :: CALCUL_1:23

    

     Th23: (J,v) |= [p, Sub] iff (J,v) |= p

    proof

      (J,v) |= [p, Sub] iff (J,v) |= ( [p, Sub] `1 ) by SUBLEMMA:def 2;

      hence thesis;

    end;

    reserve a for Element of A;

    theorem :: CALCUL_1:24

    

     Th24: (J,v) |= (p . (x,y)) iff ex a st (v . y) = a & (J,(v . (x | a))) |= p

    proof

      

       A1: (J,v) |= ( CQC_Sub [p, ( Sbst (x,y))]) iff (J,(v . ( Val_S (v, [p, ( Sbst (x,y))])))) |= [p, ( Sbst (x,y))] by SUBLEMMA: 89;

      

       A2: (J,(v . ( Val_S (v, [p, ( Sbst (x,y))])))) |= [p, ( Sbst (x,y))] iff (J,(v . ( Val_S (v, [p, ( Sbst (x,y))])))) |= p by Th23;

      ( Val_S (v, [p, ( Sbst (x,y))])) = (v * ( @ ( [p, ( Sbst (x,y))] `2 ))) by SUBLEMMA:def 1;

      then ( Val_S (v, [p, ( Sbst (x,y))])) = (v * ( @ ( Sbst (x,y))));

      then

       A3: ( Val_S (v, [p, ( Sbst (x,y))])) = (v * (x .--> y)) by SUBSTUT1:def 2;

      y in ( bound_QC-variables Al);

      then y in ( dom v) by SUBLEMMA: 58;

      then ( Val_S (v, [p, ( Sbst (x,y))])) = (x .--> (v . y)) by A3, FUNCOP_1: 17;

      hence thesis by A1, A2, SUBSTUT2:def 1;

    end;

    theorem :: CALCUL_1:25

    

     Th25: ( Suc f) = ( All (x,p)) & ( Ant f) |= ( Suc f) implies for y holds ( Ant f) |= (p . (x,y))

    proof

      assume

       A1: ( Suc f) = ( All (x,p)) & ( Ant f) |= ( Suc f);

      let y, A, J, v;

      assume (J,v) |= ( Ant f);

      then

       A2: (J,v) |= ( All (x,p)) by A1;

      ex a st (v . y) = a & (J,(v . (x | a))) |= p

      proof

        take (v . y);

        thus thesis by A2, SUBLEMMA: 50;

      end;

      hence thesis by Th24;

    end;

    theorem :: CALCUL_1:26

    

     Th26: for X be set st X c= ( bound_QC-variables Al) holds not x in X implies ((v . (x | a)) | X) = (v | X)

    proof

      let X be set such that

       A1: X c= ( bound_QC-variables Al) and

       A2: not x in X;

      set f2 = (v | X);

      set f1 = ((v . (x | a)) | X);

      

       A3: ( dom f1) = ( dom f2) by A1, SUBLEMMA: 63;

      now

        let b be object such that

         A4: b in ( dom f1);

        x <> b by A2, A4;

        then

         A5: ((v . (x | a)) . b) = (v . b) by SUBLEMMA: 48;

        ((v . (x | a)) . b) = (f1 . b) by A4, FUNCT_1: 47;

        hence (f1 . b) = (f2 . b) by A3, A4, A5, FUNCT_1: 47;

      end;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: CALCUL_1:27

    

     Th27: for v, w holds (v | ( still_not-bound_in f)) = (w | ( still_not-bound_in f)) implies ((J,v) |= f implies (J,w) |= f)

    proof

      let v, w such that

       A1: (v | ( still_not-bound_in f)) = (w | ( still_not-bound_in f));

      assume (J,v) |= f;

      then

       A2: (J,v) |= ( rng f);

      let p such that

       A3: p in ( rng f);

      ex i be Nat st i in ( dom f) & p = (f . i) by A3, FINSEQ_2: 10;

      then for b be object st b in ( still_not-bound_in p) holds b in ( still_not-bound_in f) by Def5;

      then ( still_not-bound_in p) c= ( still_not-bound_in f);

      then

       A4: (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) by A1, RELAT_1: 153;

      (J,v) |= p by A2, A3;

      hence thesis by A4, SUBLEMMA: 68;

    end;

    theorem :: CALCUL_1:28

    

     Th28: not y in ( still_not-bound_in ( All (x,p))) implies (((v . (y | a)) . (x | a)) | ( still_not-bound_in p)) = ((v . (x | a)) | ( still_not-bound_in p))

    proof

      

       A1: ((v . (y | a)) . (x | a)) = (v +* ((y | a) +* (x | a))) by FUNCT_4: 14;

      assume

       A2: not y in ( still_not-bound_in ( All (x,p)));

      now

        assume

         A3: x <> y;

        ( dom (x | a)) = {x} & ( dom (y | a)) = {y};

        then ((v . (y | a)) . (x | a)) = (v +* ((x | a) +* (y | a))) by A1, A3, FUNCT_4: 35, ZFMISC_1: 11;

        then

         A4: ((v . (y | a)) . (x | a)) = ((v +* (x | a)) +* (y | a)) by FUNCT_4: 14;

         not y in (( still_not-bound_in p) \ {x}) by A2, QC_LANG3: 12;

        then not y in ( still_not-bound_in p) by A3, ZFMISC_1: 56;

        hence thesis by A4, Th26;

      end;

      hence thesis by A1;

    end;

    theorem :: CALCUL_1:29

    

     Th29: ( Suc f) = (p . (x,y)) & ( Ant f) |= ( Suc f) & not y in ( still_not-bound_in ( Ant f)) & not y in ( still_not-bound_in ( All (x,p))) implies ( Ant f) |= ( All (x,p))

    proof

      assume that

       A1: ( Suc f) = (p . (x,y)) & ( Ant f) |= ( Suc f) and

       A2: not y in ( still_not-bound_in ( Ant f)) and

       A3: not y in ( still_not-bound_in ( All (x,p)));

      let A, J, v such that

       A4: (J,v) |= ( Ant f);

      for a holds (J,(v . (x | a))) |= p

      proof

        let a;

        ((v . (y | a)) | ( still_not-bound_in ( Ant f))) = (v | ( still_not-bound_in ( Ant f))) by A2, Th26;

        then (J,(v . (y | a))) |= ( Ant f) by A4, Th27;

        then (J,(v . (y | a))) |= (p . (x,y)) by A1;

        then ex a1 be Element of A st ((v . (y | a)) . y) = a1 & (J,((v . (y | a)) . (x | a1))) |= p by Th24;

        then

         A5: (J,((v . (y | a)) . (x | a))) |= p by SUBLEMMA: 49;

        (((v . (y | a)) . (x | a)) | ( still_not-bound_in p)) = ((v . (x | a)) | ( still_not-bound_in p)) by A3, Th28;

        hence thesis by A5, SUBLEMMA: 68;

      end;

      hence thesis by SUBLEMMA: 50;

    end;

    theorem :: CALCUL_1:30

    

     Th30: ( Ant (f ^ <*( VERUM Al)*>)) |= ( Suc (f ^ <*( VERUM Al)*>))

    proof

      let A, J, v such that (J,v) |= ( Ant (f ^ <*( VERUM Al)*>));

      ( Suc (f ^ <*( VERUM Al)*>)) = ( VERUM Al) by Th5;

      hence thesis by VALUAT_1: 32;

    end;

    theorem :: CALCUL_1:31

    

     Th31: for n be Nat holds 1 <= n & n <= ( len PR) implies ((PR . n) `2 ) = 0 or ... or ((PR . n) `2 ) = 9

    proof

      let n be Nat;

      assume 1 <= n & n <= ( len PR);

      then n in ( dom PR) by FINSEQ_3: 25;

      then (PR . n) in ( rng PR) by FUNCT_1:def 3;

      then ((PR . n) `2 ) in { k where k be Nat : k <= 9 } by CQC_THE1:def 3, MCART_1: 10;

      then ex k be Nat st k = ((PR . n) `2 ) & k <= 9;

      hence thesis;

    end;

    

     Lm3: 1 <= n & n <= ( len PR) implies ((PR . n) `1 ) is FinSequence of ( CQC-WFF Al)

    proof

      assume 1 <= n & n <= ( len PR);

      then n in ( dom PR) by FINSEQ_3: 25;

      then (PR . n) in ( rng PR) by FUNCT_1:def 3;

      then ((PR . n) `1 ) in ( set_of_CQC-WFF-seq Al) by MCART_1: 10;

      hence thesis by Def6;

    end;

    theorem :: CALCUL_1:32

    p is_formal_provable_from X implies X |= p

    proof

      assume p is_formal_provable_from X;

      then

      consider f such that

       A1: ( rng ( Ant f)) c= X and

       A2: ( Suc f) = p and

       A3: |- f;

      consider PR such that

       A4: PR is a_proof and

       A5: f = ((PR . ( len PR)) `1 ) by A3;

      PR <> {} by A4;

      then

       A6: 1 <= ( len PR) by FINSEQ_1: 20;

      defpred P[ Nat] means $1 <= ( len PR) implies for m st 1 <= m & m <= $1 holds ex g st g = ((PR . m) `1 ) & ( Ant g) |= ( Suc g);

      

       A7: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat such that

         A8: P[k];

        assume

         A9: (k + 1) <= ( len PR);

        

         A10: k <= (k + 1) by NAT_1: 11;

        let m such that

         A11: 1 <= m and

         A12: m <= (k + 1);

        

         A13: m <= ( len PR) by A9, A12, XXREAL_0: 2;

         A14:

        now

          assume

           A15: m = (k + 1);

          take g = ((PR . m) `1 );

          thus g = ((PR . m) `1 );

          reconsider g = ((PR . m) `1 ) as FinSequence of ( CQC-WFF Al) by A11, A13, Lm3;

          

           A16: (PR,m) is_a_correct_step by A4, A11, A13;

          now

            ((PR . m) `2 ) = 0 or ... or ((PR . m) `2 ) = 9 by A11, A13, Th31;

            per cases ;

              suppose ((PR . m) `2 ) = 0 ;

              then ex f st ( Suc f) is_tail_of ( Ant f) & ((PR . m) `1 ) = f by A16, Def7;

              hence ( Ant g) |= ( Suc g) by Th15;

            end;

              suppose ((PR . m) `2 ) = 1;

              then ex f st g = (f ^ <*( VERUM Al)*>) by A16, Def7;

              hence ( Ant g) |= ( Suc g) by Th30;

            end;

              suppose ((PR . m) `2 ) = 2;

              then

              consider i, f, f1 such that

               A17: 1 <= i and

               A18: i < m and

               A19: ( Ant f) is_Subsequence_of ( Ant f1) & ( Suc f) = ( Suc f1) & ((PR . i) `1 ) = f & ((PR . m) `1 ) = f1 by A16, Def7;

              i <= k by A15, A18, NAT_1: 13;

              then ex h st h = ((PR . i) `1 ) & ( Ant h) |= ( Suc h) by A8, A9, A10, A17, XXREAL_0: 2;

              hence ( Ant g) |= ( Suc g) by A19, Th16;

            end;

              suppose ((PR . m) `2 ) = 3;

              then

              consider i, j, f, f1 such that

               A20: 1 <= i and

               A21: i < m and

               A22: 1 <= j and

               A23: j < i and

               A24: ( len f) > 1 & ( len f1) > 1 & ( Ant ( Ant f)) = ( Ant ( Ant f1)) & ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant f1)) & ( Suc f) = ( Suc f1) & f = ((PR . j) `1 ) & f1 = ((PR . i) `1 ) and

               A25: (( Ant ( Ant f)) ^ <*( Suc f)*>) = ((PR . m) `1 ) by A16, Def7;

              

               A26: ( Ant g) = ( Ant ( Ant f)) & ( Suc g) = ( Suc f) by A25, Th5;

              

               A27: i <= k by A15, A21, NAT_1: 13;

              then j <= k by A23, XXREAL_0: 2;

              then

               A28: ex h1 st h1 = ((PR . j) `1 ) & ( Ant h1) |= ( Suc h1) by A8, A9, A10, A22, XXREAL_0: 2;

              ex h st h = ((PR . i) `1 ) & ( Ant h) |= ( Suc h) by A8, A9, A10, A20, A27, XXREAL_0: 2;

              hence ( Ant g) |= ( Suc g) by A24, A28, A26, Th18;

            end;

              suppose ((PR . m) `2 ) = 4;

              then

              consider i, j, f, f1, p such that

               A29: 1 <= i and

               A30: i < m and

               A31: 1 <= j and

               A32: j < i and

               A33: ( len f) > 1 & ( Ant f) = ( Ant f1) & ( Suc ( Ant f)) = ( 'not' p) & ( 'not' ( Suc f)) = ( Suc f1) & f = ((PR . j) `1 ) & f1 = ((PR . i) `1 ) and

               A34: (( Ant ( Ant f)) ^ <*p*>) = ((PR . m) `1 ) by A16, Def7;

              

               A35: ( Ant g) = ( Ant ( Ant f)) & ( Suc g) = p by A34, Th5;

              

               A36: i <= k by A15, A30, NAT_1: 13;

              then j <= k by A32, XXREAL_0: 2;

              then

               A37: ex h1 st h1 = ((PR . j) `1 ) & ( Ant h1) |= ( Suc h1) by A8, A9, A10, A31, XXREAL_0: 2;

              ex h st h = ((PR . i) `1 ) & ( Ant h) |= ( Suc h) by A8, A9, A10, A29, A36, XXREAL_0: 2;

              hence ( Ant g) |= ( Suc g) by A33, A37, A35, Th19;

            end;

              suppose ((PR . m) `2 ) = 5;

              then

              consider i, j, f, f1 such that

               A38: 1 <= i and

               A39: i < m and

               A40: 1 <= j and

               A41: j < i and

               A42: ( Ant f) = ( Ant f1) & f = ((PR . j) `1 ) & f1 = ((PR . i) `1 ) and

               A43: (( Ant f) ^ <*(( Suc f) '&' ( Suc f1))*>) = ((PR . m) `1 ) by A16, Def7;

              

               A44: ( Ant g) = ( Ant f) & ( Suc g) = (( Suc f) '&' ( Suc f1)) by A43, Th5;

              

               A45: i <= k by A15, A39, NAT_1: 13;

              then j <= k by A41, XXREAL_0: 2;

              then

               A46: ex h1 st h1 = ((PR . j) `1 ) & ( Ant h1) |= ( Suc h1) by A8, A9, A10, A40, XXREAL_0: 2;

              ex h st h = ((PR . i) `1 ) & ( Ant h) |= ( Suc h) by A8, A9, A10, A38, A45, XXREAL_0: 2;

              hence ( Ant g) |= ( Suc g) by A42, A46, A44, Th20;

            end;

              suppose ((PR . m) `2 ) = 6;

              then

              consider i, f, p, q such that

               A47: 1 <= i and

               A48: i < m and

               A49: (p '&' q) = ( Suc f) & f = ((PR . i) `1 ) and

               A50: (( Ant f) ^ <*p*>) = ((PR . m) `1 ) by A16, Def7;

              i <= k by A15, A48, NAT_1: 13;

              then

               A51: ex h st h = ((PR . i) `1 ) & ( Ant h) |= ( Suc h) by A8, A9, A10, A47, XXREAL_0: 2;

              ( Ant g) = ( Ant f) & ( Suc g) = p by A50, Th5;

              hence ( Ant g) |= ( Suc g) by A49, A51, Th21;

            end;

              suppose ((PR . m) `2 ) = 7;

              then

              consider i, f, p, q such that

               A52: 1 <= i and

               A53: i < m and

               A54: (p '&' q) = ( Suc f) & f = ((PR . i) `1 ) and

               A55: (( Ant f) ^ <*q*>) = ((PR . m) `1 ) by A16, Def7;

              i <= k by A15, A53, NAT_1: 13;

              then

               A56: ex h st h = ((PR . i) `1 ) & ( Ant h) |= ( Suc h) by A8, A9, A10, A52, XXREAL_0: 2;

              ( Ant g) = ( Ant f) & ( Suc g) = q by A55, Th5;

              hence ( Ant g) |= ( Suc g) by A54, A56, Th22;

            end;

              suppose ((PR . m) `2 ) = 8;

              then

              consider i, f, p, x, y such that

               A57: 1 <= i and

               A58: i < m and

               A59: ( Suc f) = ( All (x,p)) & f = ((PR . i) `1 ) and

               A60: (( Ant f) ^ <*(p . (x,y))*>) = ((PR . m) `1 ) by A16, Def7;

              i <= k by A15, A58, NAT_1: 13;

              then

               A61: ex h st h = ((PR . i) `1 ) & ( Ant h) |= ( Suc h) by A8, A9, A10, A57, XXREAL_0: 2;

              ( Ant g) = ( Ant f) & ( Suc g) = (p . (x,y)) by A60, Th5;

              hence ( Ant g) |= ( Suc g) by A59, A61, Th25;

            end;

              suppose ((PR . m) `2 ) = 9;

              then

              consider i, f, p, x, y such that

               A62: 1 <= i and

               A63: i < m and

               A64: ( Suc f) = (p . (x,y)) & not y in ( still_not-bound_in ( Ant f)) & ( not y in ( still_not-bound_in ( All (x,p)))) & f = ((PR . i) `1 ) and

               A65: (( Ant f) ^ <*( All (x,p))*>) = ((PR . m) `1 ) by A16, Def7;

              i <= k by A15, A63, NAT_1: 13;

              then

               A66: ex h st h = ((PR . i) `1 ) & ( Ant h) |= ( Suc h) by A8, A9, A10, A62, XXREAL_0: 2;

              ( Ant g) = ( Ant f) & ( Suc g) = ( All (x,p)) by A65, Th5;

              hence ( Ant g) |= ( Suc g) by A64, A66, Th29;

            end;

          end;

          hence thesis;

        end;

        m <= k implies ex g st g = ((PR . m) `1 ) & ( Ant g) |= ( Suc g) by A8, A9, A11, A10, XXREAL_0: 2;

        hence thesis by A12, A14, NAT_1: 8;

      end;

      

       A67: P[ 0 ];

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

      then

      consider g such that

       A68: g = ((PR . ( len PR)) `1 ) and

       A69: ( Ant g) |= ( Suc g) by A6;

      let A, J, v;

      assume (J,v) |= X;

      then for p st p in ( rng ( Ant f)) holds (J,v) |= p by A1;

      then (J,v) |= ( rng ( Ant f));

      then (J,v) |= ( Ant g) by A5, A68;

      hence thesis by A2, A5, A68, A69;

    end;

    begin

    theorem :: CALCUL_1:33

    

     Th33: ( Suc f) is_tail_of ( Ant f) implies |- f

    proof

      set PR = <* [f, 0 ]*>;

      

       A1: ( rng PR) = { [f, 0 ]} by FINSEQ_1: 38;

      now

        let a be object;

        assume a in ( rng PR);

        then

         A2: a = [f, 0 ] by A1, TARSKI:def 1;

        f in ( set_of_CQC-WFF-seq Al) by Def6;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A2, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng PR) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      assume

       A3: ( Suc f) is_tail_of ( Ant f);

      now

        let n be Nat such that

         A4: 1 <= n and

         A5: n <= ( len PR);

        n <= 1 by A5, FINSEQ_1: 39;

        then n = 1 by A4, XXREAL_0: 1;

        then (PR . n) = [f, 0 ] by FINSEQ_1: 40;

        then ((PR . n) `1 ) = f & ((PR . n) `2 ) = 0 ;

        hence (PR,n) is_a_correct_step by A3, Def7;

      end;

      then

       A6: PR is a_proof;

      (PR . 1) = [f, 0 ] by FINSEQ_1: 40;

      then (PR . ( len PR)) = [f, 0 ] by FINSEQ_1: 40;

      then ((PR . ( len PR)) `1 ) = f;

      hence thesis by A6;

    end;

    theorem :: CALCUL_1:34

    

     Th34: for n be Nat holds 1 <= n & n <= ( len PR) implies ((PR,n) is_a_correct_step iff ((PR ^ PR1),n) is_a_correct_step )

    proof

      let n be Nat;

      assume that

       A1: 1 <= n and

       A2: n <= ( len PR);

      n in ( dom PR) by A1, A2, FINSEQ_3: 25;

      then

       A3: ((PR ^ PR1) . n) = (PR . n) by FINSEQ_1:def 7;

      ( len (PR ^ PR1)) = (( len PR) + ( len PR1)) by FINSEQ_1: 22;

      then ( len PR) <= ( len (PR ^ PR1)) by NAT_1: 11;

      then

       A4: n <= ( len (PR ^ PR1)) by A2, XXREAL_0: 2;

      thus (PR,n) is_a_correct_step implies ((PR ^ PR1),n) is_a_correct_step

      proof

        assume

         A5: (PR,n) is_a_correct_step ;

        (((PR ^ PR1) . n) `2 ) = 0 or ... or (((PR ^ PR1) . n) `2 ) = 9 by A1, A4, Th31;

        per cases ;

          case (((PR ^ PR1) . n) `2 ) = 0 ;

          hence thesis by A3, A5, Def7;

        end;

          case (((PR ^ PR1) . n) `2 ) = 1;

          hence thesis by A3, A5, Def7;

        end;

          case (((PR ^ PR1) . n) `2 ) = 2;

          then

          consider i, f, g such that

           A6: 1 <= i and

           A7: i < n and

           A8: ( Ant f) is_Subsequence_of ( Ant g) & ( Suc f) = ( Suc g) & ((PR . i) `1 ) = f & ((PR . n) `1 ) = g by A3, A5, Def7;

          i <= ( len PR) by A2, A7, XXREAL_0: 2;

          then i in ( dom PR) by A6, FINSEQ_3: 25;

          then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

          hence thesis by A3, A6, A7, A8;

        end;

          case (((PR ^ PR1) . n) `2 ) = 3;

          then

          consider i, j, f, g such that

           A9: 1 <= i and

           A10: i < n and

           A11: 1 <= j and

           A12: j < i and

           A13: ( len f) > 1 & ( len g) > 1 & ( Ant ( Ant f)) = ( Ant ( Ant g)) & ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant g)) & ( Suc f) = ( Suc g) & f = ((PR . j) `1 ) & g = ((PR . i) `1 ) & (( Ant ( Ant f)) ^ <*( Suc f)*>) = ((PR . n) `1 ) by A3, A5, Def7;

          

           A14: i <= ( len PR) by A2, A10, XXREAL_0: 2;

          then i in ( Seg ( len PR)) by A9, FINSEQ_1: 1;

          then i in ( dom PR) by FINSEQ_1:def 3;

          then

           A15: (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

          j <= ( len PR) by A12, A14, XXREAL_0: 2;

          then j in ( dom PR) by A11, FINSEQ_3: 25;

          then (PR . j) = ((PR ^ PR1) . j) by FINSEQ_1:def 7;

          hence thesis by A3, A9, A10, A11, A12, A13, A15;

        end;

          case (((PR ^ PR1) . n) `2 ) = 4;

          then

          consider i, j, f, g, p such that

           A16: 1 <= i and

           A17: i < n and

           A18: 1 <= j and

           A19: j < i and

           A20: ( len f) > 1 & ( Ant f) = ( Ant g) & ( Suc ( Ant f)) = ( 'not' p) & ( 'not' ( Suc f)) = ( Suc g) & f = ((PR . j) `1 ) & g = ((PR . i) `1 ) & (( Ant ( Ant f)) ^ <*p*>) = ((PR . n) `1 ) by A3, A5, Def7;

          

           A21: i <= ( len PR) by A2, A17, XXREAL_0: 2;

          then i in ( Seg ( len PR)) by A16, FINSEQ_1: 1;

          then i in ( dom PR) by FINSEQ_1:def 3;

          then

           A22: (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

          j <= ( len PR) by A19, A21, XXREAL_0: 2;

          then j in ( dom PR) by A18, FINSEQ_3: 25;

          then (PR . j) = ((PR ^ PR1) . j) by FINSEQ_1:def 7;

          hence thesis by A3, A16, A17, A18, A19, A20, A22;

        end;

          case (((PR ^ PR1) . n) `2 ) = 5;

          then

          consider i, j, f, g such that

           A23: 1 <= i and

           A24: i < n and

           A25: 1 <= j and

           A26: j < i and

           A27: ( Ant f) = ( Ant g) & f = ((PR . j) `1 ) & g = ((PR . i) `1 ) & (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>) = ((PR . n) `1 ) by A3, A5, Def7;

          

           A28: i <= ( len PR) by A2, A24, XXREAL_0: 2;

          then i in ( Seg ( len PR)) by A23, FINSEQ_1: 1;

          then i in ( dom PR) by FINSEQ_1:def 3;

          then

           A29: (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

          j <= ( len PR) by A26, A28, XXREAL_0: 2;

          then j in ( dom PR) by A25, FINSEQ_3: 25;

          then (PR . j) = ((PR ^ PR1) . j) by FINSEQ_1:def 7;

          hence thesis by A3, A23, A24, A25, A26, A27, A29;

        end;

          case (((PR ^ PR1) . n) `2 ) = 6;

          then

          consider i, f, p, q such that

           A30: 1 <= i and

           A31: i < n and

           A32: (p '&' q) = ( Suc f) & f = ((PR . i) `1 ) & (( Ant f) ^ <*p*>) = ((PR . n) `1 ) by A3, A5, Def7;

          i <= ( len PR) by A2, A31, XXREAL_0: 2;

          then i in ( dom PR) by A30, FINSEQ_3: 25;

          then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

          hence thesis by A3, A30, A31, A32;

        end;

          case (((PR ^ PR1) . n) `2 ) = 7;

          then

          consider i, f, p, q such that

           A33: 1 <= i and

           A34: i < n and

           A35: (p '&' q) = ( Suc f) & f = ((PR . i) `1 ) & (( Ant f) ^ <*q*>) = ((PR . n) `1 ) by A3, A5, Def7;

          i <= ( len PR) by A2, A34, XXREAL_0: 2;

          then i in ( dom PR) by A33, FINSEQ_3: 25;

          then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

          hence thesis by A3, A33, A34, A35;

        end;

          case (((PR ^ PR1) . n) `2 ) = 8;

          then

          consider i, f, p, x, y such that

           A36: 1 <= i and

           A37: i < n and

           A38: ( Suc f) = ( All (x,p)) & f = ((PR . i) `1 ) & (( Ant f) ^ <*(p . (x,y))*>) = ((PR . n) `1 ) by A3, A5, Def7;

          i <= ( len PR) by A2, A37, XXREAL_0: 2;

          then i in ( dom PR) by A36, FINSEQ_3: 25;

          then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

          hence thesis by A3, A36, A37, A38;

        end;

          case (((PR ^ PR1) . n) `2 ) = 9;

          then

          consider i, f, p, x, y such that

           A39: 1 <= i and

           A40: i < n and

           A41: ( Suc f) = (p . (x,y)) & not y in ( still_not-bound_in ( Ant f)) & ( not y in ( still_not-bound_in ( All (x,p)))) & f = ((PR . i) `1 ) & (( Ant f) ^ <*( All (x,p))*>) = ((PR . n) `1 ) by A3, A5, Def7;

          i <= ( len PR) by A2, A40, XXREAL_0: 2;

          then i in ( dom PR) by A39, FINSEQ_3: 25;

          then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

          hence thesis by A3, A39, A40, A41;

        end;

      end;

      assume

       A42: ((PR ^ PR1),n) is_a_correct_step ;

      ((PR . n) `2 ) = 0 or ... or ((PR . n) `2 ) = 9 by A1, A2, Th31;

      per cases ;

        case ((PR . n) `2 ) = 0 ;

        hence thesis by A3, A42, Def7;

      end;

        case ((PR . n) `2 ) = 1;

        hence thesis by A3, A42, Def7;

      end;

        case ((PR . n) `2 ) = 2;

        then

        consider i, f, g such that

         A43: 1 <= i and

         A44: i < n and

         A45: ( Ant f) is_Subsequence_of ( Ant g) & ( Suc f) = ( Suc g) & (((PR ^ PR1) . i) `1 ) = f & (((PR ^ PR1) . n) `1 ) = g by A3, A42, Def7;

        i <= ( len PR) by A2, A44, XXREAL_0: 2;

        then i in ( dom PR) by A43, FINSEQ_3: 25;

        then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

        hence thesis by A3, A43, A44, A45;

      end;

        case ((PR . n) `2 ) = 3;

        then

        consider i, j, f, f1 such that

         A46: 1 <= i and

         A47: i < n and

         A48: 1 <= j and

         A49: j < i and

         A50: ( len f) > 1 & ( len f1) > 1 & ( Ant ( Ant f)) = ( Ant ( Ant f1)) & ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant f1)) & ( Suc f) = ( Suc f1) & f = (((PR ^ PR1) . j) `1 ) & f1 = (((PR ^ PR1) . i) `1 ) & (( Ant ( Ant f)) ^ <*( Suc f)*>) = (((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

        

         A51: i <= ( len PR) by A2, A47, XXREAL_0: 2;

        then i in ( Seg ( len PR)) by A46, FINSEQ_1: 1;

        then i in ( dom PR) by FINSEQ_1:def 3;

        then

         A52: (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

        j <= ( len PR) by A49, A51, XXREAL_0: 2;

        then j in ( dom PR) by A48, FINSEQ_3: 25;

        then (PR . j) = ((PR ^ PR1) . j) by FINSEQ_1:def 7;

        hence thesis by A3, A46, A47, A48, A49, A50, A52;

      end;

        case ((PR . n) `2 ) = 4;

        then

        consider i, j, f, g, p such that

         A53: 1 <= i and

         A54: i < n and

         A55: 1 <= j and

         A56: j < i and

         A57: ( len f) > 1 & ( Ant f) = ( Ant g) & ( Suc ( Ant f)) = ( 'not' p) & ( 'not' ( Suc f)) = ( Suc g) & f = (((PR ^ PR1) . j) `1 ) & g = (((PR ^ PR1) . i) `1 ) & (( Ant ( Ant f)) ^ <*p*>) = (((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

        

         A58: i <= ( len PR) by A2, A54, XXREAL_0: 2;

        then i in ( Seg ( len PR)) by A53, FINSEQ_1: 1;

        then i in ( dom PR) by FINSEQ_1:def 3;

        then

         A59: (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

        j <= ( len PR) by A56, A58, XXREAL_0: 2;

        then j in ( dom PR) by A55, FINSEQ_3: 25;

        then (PR . j) = ((PR ^ PR1) . j) by FINSEQ_1:def 7;

        hence thesis by A3, A53, A54, A55, A56, A57, A59;

      end;

        case ((PR . n) `2 ) = 5;

        then

        consider i, j, f, g such that

         A60: 1 <= i and

         A61: i < n and

         A62: 1 <= j and

         A63: j < i and

         A64: ( Ant f) = ( Ant g) & f = (((PR ^ PR1) . j) `1 ) & g = (((PR ^ PR1) . i) `1 ) & (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>) = (((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

        

         A65: i <= ( len PR) by A2, A61, XXREAL_0: 2;

        then i in ( Seg ( len PR)) by A60, FINSEQ_1: 1;

        then i in ( dom PR) by FINSEQ_1:def 3;

        then

         A66: (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

        j <= ( len PR) by A63, A65, XXREAL_0: 2;

        then j in ( dom PR) by A62, FINSEQ_3: 25;

        then (PR . j) = ((PR ^ PR1) . j) by FINSEQ_1:def 7;

        hence thesis by A3, A60, A61, A62, A63, A64, A66;

      end;

        case ((PR . n) `2 ) = 6;

        then

        consider i, f, p, q such that

         A67: 1 <= i and

         A68: i < n and

         A69: (p '&' q) = ( Suc f) & f = (((PR ^ PR1) . i) `1 ) & (( Ant f) ^ <*p*>) = (((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

        i <= ( len PR) by A2, A68, XXREAL_0: 2;

        then i in ( dom PR) by A67, FINSEQ_3: 25;

        then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

        hence thesis by A3, A67, A68, A69;

      end;

        case ((PR . n) `2 ) = 7;

        then

        consider i, f, p, q such that

         A70: 1 <= i and

         A71: i < n and

         A72: (p '&' q) = ( Suc f) & f = (((PR ^ PR1) . i) `1 ) & (( Ant f) ^ <*q*>) = (((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

        i <= ( len PR) by A2, A71, XXREAL_0: 2;

        then i in ( dom PR) by A70, FINSEQ_3: 25;

        then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

        hence thesis by A3, A70, A71, A72;

      end;

        case ((PR . n) `2 ) = 8;

        then

        consider i, f, p, x, y such that

         A73: 1 <= i and

         A74: i < n and

         A75: ( Suc f) = ( All (x,p)) & f = (((PR ^ PR1) . i) `1 ) & (( Ant f) ^ <*(p . (x,y))*>) = (((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

        i <= ( len PR) by A2, A74, XXREAL_0: 2;

        then i in ( dom PR) by A73, FINSEQ_3: 25;

        then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

        hence thesis by A3, A73, A74, A75;

      end;

        case ((PR . n) `2 ) = 9;

        then

        consider i, f, p, x, y such that

         A76: 1 <= i and

         A77: i < n and

         A78: ( Suc f) = (p . (x,y)) & not y in ( still_not-bound_in ( Ant f)) & ( not y in ( still_not-bound_in ( All (x,p)))) & f = (((PR ^ PR1) . i) `1 ) & (( Ant f) ^ <*( All (x,p))*>) = (((PR ^ PR1) . n) `1 ) by A3, A42, Def7;

        i <= ( len PR) by A2, A77, XXREAL_0: 2;

        then i in ( dom PR) by A76, FINSEQ_3: 25;

        then (PR . i) = ((PR ^ PR1) . i) by FINSEQ_1:def 7;

        hence thesis by A3, A76, A77, A78;

      end;

    end;

    theorem :: CALCUL_1:35

    

     Th35: 1 <= n & n <= ( len PR1) & (PR1,n) is_a_correct_step implies ((PR ^ PR1),(n + ( len PR))) is_a_correct_step

    proof

      assume that

       A1: 1 <= n and

       A2: n <= ( len PR1) and

       A3: (PR1,n) is_a_correct_step ;

      n in ( dom PR1) by A1, A2, FINSEQ_3: 25;

      then

       A4: (PR1 . n) = ((PR ^ PR1) . (n + ( len PR))) by FINSEQ_1:def 7;

      (n + ( len PR)) <= (( len PR) + ( len PR1)) by A2, XREAL_1: 6;

      then

       A5: (n + ( len PR)) <= ( len (PR ^ PR1)) by FINSEQ_1: 22;

      (((PR ^ PR1) . (n + ( len PR))) `2 ) = 0 or ... or (((PR ^ PR1) . (n + ( len PR))) `2 ) = 9 by A1, A5, Th31, NAT_1: 12;

      per cases ;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 0 ;

        hence thesis by A3, A4, Def7;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 1;

        hence thesis by A3, A4, Def7;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 2;

        then

        consider i, f, g such that

         A6: 1 <= i and

         A7: i < n and

         A8: ( Ant f) is_Subsequence_of ( Ant g) & ( Suc f) = ( Suc g) & ((PR1 . i) `1 ) = f & ((PR1 . n) `1 ) = g by A3, A4, Def7;

        i <= ( len PR1) by A2, A7, XXREAL_0: 2;

        then i in ( dom PR1) by A6, FINSEQ_3: 25;

        then

         A9: (PR1 . i) = ((PR ^ PR1) . (( len PR) + i)) by FINSEQ_1:def 7;

        1 <= (( len PR) + i) & (( len PR) + i) < (n + ( len PR)) by A6, A7, NAT_1: 12, XREAL_1: 6;

        hence thesis by A4, A8, A9;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 3;

        then

        consider i, j, f, f1 such that

         A10: 1 <= i and

         A11: i < n and

         A12: 1 <= j and

         A13: j < i and

         A14: ( len f) > 1 & ( len f1) > 1 & ( Ant ( Ant f)) = ( Ant ( Ant f1)) & ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant f1)) & ( Suc f) = ( Suc f1) & f = ((PR1 . j) `1 ) & f1 = ((PR1 . i) `1 ) & (( Ant ( Ant f)) ^ <*( Suc f)*>) = ((PR1 . n) `1 ) by A3, A4, Def7;

        

         A15: 1 <= (( len PR) + j) & (( len PR) + j) < (i + ( len PR)) by A12, A13, NAT_1: 12, XREAL_1: 6;

        

         A16: i <= ( len PR1) by A2, A11, XXREAL_0: 2;

        then i in ( dom PR1) by A10, FINSEQ_3: 25;

        then

         A17: (PR1 . i) = ((PR ^ PR1) . (( len PR) + i)) by FINSEQ_1:def 7;

        j <= ( len PR1) by A13, A16, XXREAL_0: 2;

        then j in ( dom PR1) by A12, FINSEQ_3: 25;

        then

         A18: (PR1 . j) = ((PR ^ PR1) . (( len PR) + j)) by FINSEQ_1:def 7;

        1 <= (( len PR) + i) & (( len PR) + i) < (n + ( len PR)) by A10, A11, NAT_1: 12, XREAL_1: 6;

        hence thesis by A4, A14, A15, A17, A18;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 4;

        then

        consider i, j, f, g, p such that

         A19: 1 <= i and

         A20: i < n and

         A21: 1 <= j and

         A22: j < i and

         A23: ( len f) > 1 & ( Ant f) = ( Ant g) & ( Suc ( Ant f)) = ( 'not' p) & ( 'not' ( Suc f)) = ( Suc g) & f = ((PR1 . j) `1 ) & g = ((PR1 . i) `1 ) & (( Ant ( Ant f)) ^ <*p*>) = ((PR1 . n) `1 ) by A3, A4, Def7;

        

         A24: 1 <= (( len PR) + j) & (( len PR) + j) < (i + ( len PR)) by A21, A22, NAT_1: 12, XREAL_1: 6;

        

         A25: i <= ( len PR1) by A2, A20, XXREAL_0: 2;

        then i in ( dom PR1) by A19, FINSEQ_3: 25;

        then

         A26: (PR1 . i) = ((PR ^ PR1) . (( len PR) + i)) by FINSEQ_1:def 7;

        j <= ( len PR1) by A22, A25, XXREAL_0: 2;

        then j in ( dom PR1) by A21, FINSEQ_3: 25;

        then

         A27: (PR1 . j) = ((PR ^ PR1) . (( len PR) + j)) by FINSEQ_1:def 7;

        1 <= (( len PR) + i) & (( len PR) + i) < (n + ( len PR)) by A19, A20, NAT_1: 12, XREAL_1: 6;

        hence thesis by A4, A23, A24, A26, A27;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 5;

        then

        consider i, j, f, g such that

         A28: 1 <= i and

         A29: i < n and

         A30: 1 <= j and

         A31: j < i and

         A32: ( Ant f) = ( Ant g) & f = ((PR1 . j) `1 ) & g = ((PR1 . i) `1 ) & (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>) = ((PR1 . n) `1 ) by A3, A4, Def7;

        

         A33: 1 <= (( len PR) + j) & (( len PR) + j) < (i + ( len PR)) by A30, A31, NAT_1: 12, XREAL_1: 6;

        

         A34: i <= ( len PR1) by A2, A29, XXREAL_0: 2;

        then i in ( dom PR1) by A28, FINSEQ_3: 25;

        then

         A35: (PR1 . i) = ((PR ^ PR1) . (( len PR) + i)) by FINSEQ_1:def 7;

        j <= ( len PR1) by A31, A34, XXREAL_0: 2;

        then j in ( dom PR1) by A30, FINSEQ_3: 25;

        then

         A36: (PR1 . j) = ((PR ^ PR1) . (( len PR) + j)) by FINSEQ_1:def 7;

        1 <= (( len PR) + i) & (( len PR) + i) < (n + ( len PR)) by A28, A29, NAT_1: 12, XREAL_1: 6;

        hence thesis by A4, A32, A33, A35, A36;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 6;

        then

        consider i, f, p, q such that

         A37: 1 <= i and

         A38: i < n and

         A39: (p '&' q) = ( Suc f) & f = ((PR1 . i) `1 ) & (( Ant f) ^ <*p*>) = ((PR1 . n) `1 ) by A3, A4, Def7;

        i <= ( len PR1) by A2, A38, XXREAL_0: 2;

        then i in ( dom PR1) by A37, FINSEQ_3: 25;

        then

         A40: (PR1 . i) = ((PR ^ PR1) . (( len PR) + i)) by FINSEQ_1:def 7;

        1 <= (( len PR) + i) & (( len PR) + i) < (n + ( len PR)) by A37, A38, NAT_1: 12, XREAL_1: 6;

        hence thesis by A4, A39, A40;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 7;

        then

        consider i, f, p, q such that

         A41: 1 <= i and

         A42: i < n and

         A43: (p '&' q) = ( Suc f) & f = ((PR1 . i) `1 ) & (( Ant f) ^ <*q*>) = ((PR1 . n) `1 ) by A3, A4, Def7;

        i <= ( len PR1) by A2, A42, XXREAL_0: 2;

        then i in ( dom PR1) by A41, FINSEQ_3: 25;

        then

         A44: (PR1 . i) = ((PR ^ PR1) . (( len PR) + i)) by FINSEQ_1:def 7;

        1 <= (( len PR) + i) & (( len PR) + i) < (n + ( len PR)) by A41, A42, NAT_1: 12, XREAL_1: 6;

        hence thesis by A4, A43, A44;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 8;

        then

        consider i, f, p, x, y such that

         A45: 1 <= i and

         A46: i < n and

         A47: ( Suc f) = ( All (x,p)) & f = ((PR1 . i) `1 ) & (( Ant f) ^ <*(p . (x,y))*>) = ((PR1 . n) `1 ) by A3, A4, Def7;

        i <= ( len PR1) by A2, A46, XXREAL_0: 2;

        then i in ( dom PR1) by A45, FINSEQ_3: 25;

        then

         A48: (PR1 . i) = ((PR ^ PR1) . (( len PR) + i)) by FINSEQ_1:def 7;

        1 <= (( len PR) + i) & (( len PR) + i) < (n + ( len PR)) by A45, A46, NAT_1: 12, XREAL_1: 6;

        hence thesis by A4, A47, A48;

      end;

        case (((PR ^ PR1) . (n + ( len PR))) `2 ) = 9;

        then

        consider i, f, p, x, y such that

         A49: 1 <= i and

         A50: i < n and

         A51: ( Suc f) = (p . (x,y)) & not y in ( still_not-bound_in ( Ant f)) & ( not y in ( still_not-bound_in ( All (x,p)))) & f = ((PR1 . i) `1 ) & (( Ant f) ^ <*( All (x,p))*>) = ((PR1 . n) `1 ) by A3, A4, Def7;

        i <= ( len PR1) by A2, A50, XXREAL_0: 2;

        then i in ( dom PR1) by A49, FINSEQ_3: 25;

        then

         A52: (PR1 . i) = ((PR ^ PR1) . (( len PR) + i)) by FINSEQ_1:def 7;

        1 <= (( len PR) + i) & (( len PR) + i) < (n + ( len PR)) by A49, A50, NAT_1: 12, XREAL_1: 6;

        hence thesis by A4, A51, A52;

      end;

    end;

    theorem :: CALCUL_1:36

    

     Th36: ( Ant f) is_Subsequence_of ( Ant g) & ( Suc f) = ( Suc g) & |- f implies |- g

    proof

      assume that

       A1: ( Ant f) is_Subsequence_of ( Ant g) & ( Suc f) = ( Suc g) and

       A2: |- f;

      consider PR such that

       A3: PR is a_proof and

       A4: ((PR . ( len PR)) `1 ) = f by A2;

      

       A5: g in ( set_of_CQC-WFF-seq Al) by Def6;

      now

        let a be object;

        assume a in ( rng <* [g, 2]*>);

        then a in { [g, 2]} by FINSEQ_1: 38;

        then a = [g, 2] by TARSKI:def 1;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A5, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng <* [g, 2]*>) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR1 = <* [g, 2]*> as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A6: 1 in ( dom PR1) by FINSEQ_1: 38;

      set PR2 = (PR ^ PR1);

      reconsider PR2 as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      

       A7: PR <> {} by A3;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len PR2);

        then

         A8: n in ( dom PR2) by FINSEQ_3: 25;

         A9:

        now

          

           A10: 1 <= ( len PR) by A7, Th6;

          then ( len PR) in ( dom PR) by FINSEQ_3: 25;

          then

           A11: f = ((PR2 . ( len PR)) `1 ) by A4, FINSEQ_1:def 7;

          given k be Nat such that

           A12: k in ( dom PR1) and

           A13: n = (( len PR) + k);

          k in ( Seg 1) by A12, FINSEQ_1: 38;

          then

           A14: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then

           A15: (PR1 . k) = [g, 2] by FINSEQ_1: 40;

          then ((PR1 . k) `1 ) = g;

          then

           A16: ((PR2 . n) `1 ) = g by A12, A13, FINSEQ_1:def 7;

          ((PR1 . k) `2 ) = 2 by A15;

          then

           A17: ((PR2 . n) `2 ) = 2 by A12, A13, FINSEQ_1:def 7;

          ( len PR) < n by A13, A14, NAT_1: 13;

          hence (PR2,n) is_a_correct_step by A1, A16, A17, A10, A11, Def7;

        end;

        now

          assume n in ( dom PR);

          then

           A18: 1 <= n & n <= ( len PR) by FINSEQ_3: 25;

          then (PR,n) is_a_correct_step by A3;

          hence (PR2,n) is_a_correct_step by A18, Th34;

        end;

        hence (PR2,n) is_a_correct_step by A8, A9, FINSEQ_1: 25;

      end;

      then

       A19: PR2 is a_proof;

      (PR2 . ( len PR2)) = (PR2 . (( len PR) + ( len PR1))) by FINSEQ_1: 22;

      then (PR2 . ( len PR2)) = (PR2 . (( len PR) + 1)) by FINSEQ_1: 39;

      then (PR2 . ( len PR2)) = (PR1 . 1) by A6, FINSEQ_1:def 7;

      then (PR2 . ( len PR2)) = [g, 2] by FINSEQ_1: 40;

      then ((PR2 . ( len PR2)) `1 ) = g;

      hence thesis by A19;

    end;

    theorem :: CALCUL_1:37

    

     Th37: 1 < ( len f) & 1 < ( len g) & ( Ant ( Ant f)) = ( Ant ( Ant g)) & ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant g)) & ( Suc f) = ( Suc g) & |- f & |- g implies |- (( Ant ( Ant f)) ^ <*( Suc f)*>)

    proof

      assume that

       A1: 1 < ( len f) & 1 < ( len g) & ( Ant ( Ant f)) = ( Ant ( Ant g)) & ( 'not' ( Suc ( Ant f))) = ( Suc ( Ant g)) & ( Suc f) = ( Suc g) and

       A2: |- f and

       A3: |- g;

      consider PR1 such that

       A4: PR1 is a_proof and

       A5: g = ((PR1 . ( len PR1)) `1 ) by A3;

      consider PR such that

       A6: PR is a_proof and

       A7: f = ((PR . ( len PR)) `1 ) by A2;

      

       A8: (( Ant ( Ant f)) ^ <*( Suc f)*>) in ( set_of_CQC-WFF-seq Al) by Def6;

      now

        let a be object;

        assume a in ( rng <* [(( Ant ( Ant f)) ^ <*( Suc f)*>), 3]*>);

        then a in { [(( Ant ( Ant f)) ^ <*( Suc f)*>), 3]} by FINSEQ_1: 38;

        then a = [(( Ant ( Ant f)) ^ <*( Suc f)*>), 3] by TARSKI:def 1;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A8, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng <* [(( Ant ( Ant f)) ^ <*( Suc f)*>), 3]*>) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR2 = <* [(( Ant ( Ant f)) ^ <*( Suc f)*>), 3]*> as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A9: 1 in ( dom PR2) by FINSEQ_1: 38;

      set PR3 = ((PR ^ PR1) ^ PR2);

      reconsider PR3 as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      

       A10: PR <> {} by A6;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len PR3);

        then

         A11: n in ( dom PR3) by FINSEQ_3: 25;

         A12:

        now

          given k be Nat such that

           A13: k in ( dom PR2) and

           A14: n = (( len (PR ^ PR1)) + k);

          k in ( Seg 1) by A13, FINSEQ_1: 38;

          then

           A15: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then

           A16: (PR2 . k) = [(( Ant ( Ant f)) ^ <*( Suc f)*>), 3] by FINSEQ_1: 40;

          then ((PR2 . k) `1 ) = (( Ant ( Ant f)) ^ <*( Suc f)*>);

          then

           A17: ((PR3 . n) `1 ) = (( Ant ( Ant f)) ^ <*( Suc f)*>) by A13, A14, FINSEQ_1:def 7;

          ((PR2 . k) `2 ) = 3 by A16;

          then

           A18: ((PR3 . n) `2 ) = 3 by A13, A14, FINSEQ_1:def 7;

          

           A19: ( len (PR ^ PR1)) < n by A14, A15, NAT_1: 13;

          

           A20: 1 <= ( len PR) by A10, Th6;

          then ( len PR) in ( dom PR) by FINSEQ_3: 25;

          then

           A21: f = (((PR ^ PR1) . ( len PR)) `1 ) by A7, FINSEQ_1:def 7;

          

           A22: PR1 <> {} by A4;

          then

           A23: ( len PR) < ( len (PR ^ PR1)) by Th6;

          then ( len PR) in ( dom (PR ^ PR1)) by A20, FINSEQ_3: 25;

          then

           A24: f = ((PR3 . ( len PR)) `1 ) by A21, FINSEQ_1:def 7;

          1 <= ( len PR1) by A22, Th6;

          then ( len PR1) in ( dom PR1) by FINSEQ_3: 25;

          then g = (((PR ^ PR1) . (( len PR) + ( len PR1))) `1 ) by A5, FINSEQ_1:def 7;

          then

           A25: g = (((PR ^ PR1) . ( len (PR ^ PR1))) `1 ) by FINSEQ_1: 22;

          1 <= ( len (PR ^ PR1)) by A10, Th6;

          then ( len (PR ^ PR1)) in ( dom (PR ^ PR1)) by FINSEQ_3: 25;

          then

           A26: g = ((PR3 . ( len (PR ^ PR1))) `1 ) by A25, FINSEQ_1:def 7;

          1 <= ( len (PR ^ PR1)) by A10, Th6;

          hence (PR3,n) is_a_correct_step by A1, A17, A18, A20, A23, A24, A19, A26, Def7;

        end;

        now

           A27:

          now

            given k be Nat such that

             A28: k in ( dom PR1) and

             A29: n = (( len PR) + k);

            

             A30: 1 <= k by A28, FINSEQ_3: 25;

            

             A31: k <= ( len PR1) by A28, FINSEQ_3: 25;

            then n <= (( len PR1) + ( len PR)) by A29, XREAL_1: 6;

            then

             A32: n <= ( len (PR ^ PR1)) by FINSEQ_1: 22;

            k <= n by A29, NAT_1: 11;

            then

             A33: 1 <= n by A30, XXREAL_0: 2;

            (PR1,k) is_a_correct_step by A4, A30, A31;

            then ((PR ^ PR1),n) is_a_correct_step by A29, A30, A31, Th35;

            hence (PR3,n) is_a_correct_step by A33, A32, Th34;

          end;

           A34:

          now

            assume

             A35: n in ( dom PR);

            then

             A36: 1 <= n by FINSEQ_3: 25;

            

             A37: n <= ( len PR) by A35, FINSEQ_3: 25;

            ( len PR) <= ( len (PR ^ PR1)) by Th6;

            then

             A38: n <= ( len (PR ^ PR1)) by A37, XXREAL_0: 2;

            (PR,n) is_a_correct_step by A6, A36, A37;

            then ((PR ^ PR1),n) is_a_correct_step by A36, A37, Th34;

            hence (PR3,n) is_a_correct_step by A36, A38, Th34;

          end;

          assume n in ( dom (PR ^ PR1));

          hence (PR3,n) is_a_correct_step by A34, A27, FINSEQ_1: 25;

        end;

        hence (PR3,n) is_a_correct_step by A11, A12, FINSEQ_1: 25;

      end;

      then

       A39: PR3 is a_proof;

      (PR3 . ( len PR3)) = (PR3 . (( len (PR ^ PR1)) + ( len PR2))) by FINSEQ_1: 22;

      then (PR3 . ( len PR3)) = (PR3 . (( len (PR ^ PR1)) + 1)) by FINSEQ_1: 39;

      then (PR3 . ( len PR3)) = (PR2 . 1) by A9, FINSEQ_1:def 7;

      then (PR3 . ( len PR3)) = [(( Ant ( Ant f)) ^ <*( Suc f)*>), 3] by FINSEQ_1: 40;

      then ((PR3 . ( len PR3)) `1 ) = (( Ant ( Ant f)) ^ <*( Suc f)*>);

      hence thesis by A39;

    end;

    theorem :: CALCUL_1:38

    

     Th38: ( len f) > 1 & ( Ant f) = ( Ant g) & ( Suc ( Ant f)) = ( 'not' p) & ( 'not' ( Suc f)) = ( Suc g) & |- f & |- g implies |- (( Ant ( Ant f)) ^ <*p*>)

    proof

      assume that

       A1: ( len f) > 1 & ( Ant f) = ( Ant g) & ( Suc ( Ant f)) = ( 'not' p) & ( 'not' ( Suc f)) = ( Suc g) and

       A2: |- f and

       A3: |- g;

      consider PR1 such that

       A4: PR1 is a_proof and

       A5: g = ((PR1 . ( len PR1)) `1 ) by A3;

      consider PR such that

       A6: PR is a_proof and

       A7: f = ((PR . ( len PR)) `1 ) by A2;

      

       A8: (( Ant ( Ant f)) ^ <*p*>) in ( set_of_CQC-WFF-seq Al) by Def6;

      now

        let a be object;

        assume a in ( rng <* [(( Ant ( Ant f)) ^ <*p*>), 4]*>);

        then a in { [(( Ant ( Ant f)) ^ <*p*>), 4]} by FINSEQ_1: 38;

        then a = [(( Ant ( Ant f)) ^ <*p*>), 4] by TARSKI:def 1;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A8, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng <* [(( Ant ( Ant f)) ^ <*p*>), 4]*>) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR2 = <* [(( Ant ( Ant f)) ^ <*p*>), 4]*> as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A9: 1 in ( dom PR2) by FINSEQ_1: 38;

      set PR3 = ((PR ^ PR1) ^ PR2);

      reconsider PR3 as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      

       A10: PR <> {} by A6;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len PR3);

        then

         A11: n in ( dom PR3) by FINSEQ_3: 25;

         A12:

        now

          given k be Nat such that

           A13: k in ( dom PR2) and

           A14: n = (( len (PR ^ PR1)) + k);

          k in ( Seg 1) by A13, FINSEQ_1: 38;

          then

           A15: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then

           A16: (PR2 . k) = [(( Ant ( Ant f)) ^ <*p*>), 4] by FINSEQ_1: 40;

          then ((PR2 . k) `1 ) = (( Ant ( Ant f)) ^ <*p*>);

          then

           A17: ((PR3 . n) `1 ) = (( Ant ( Ant f)) ^ <*p*>) by A13, A14, FINSEQ_1:def 7;

          ((PR2 . k) `2 ) = 4 by A16;

          then

           A18: ((PR3 . n) `2 ) = 4 by A13, A14, FINSEQ_1:def 7;

          

           A19: ( len (PR ^ PR1)) < n by A14, A15, NAT_1: 13;

          

           A20: 1 <= ( len PR) by A10, Th6;

          then ( len PR) in ( dom PR) by FINSEQ_3: 25;

          then

           A21: f = (((PR ^ PR1) . ( len PR)) `1 ) by A7, FINSEQ_1:def 7;

          

           A22: PR1 <> {} by A4;

          then

           A23: ( len PR) < ( len (PR ^ PR1)) by Th6;

          then ( len PR) in ( dom (PR ^ PR1)) by A20, FINSEQ_3: 25;

          then

           A24: f = ((PR3 . ( len PR)) `1 ) by A21, FINSEQ_1:def 7;

          1 <= ( len PR1) by A22, Th6;

          then ( len PR1) in ( dom PR1) by FINSEQ_3: 25;

          then g = (((PR ^ PR1) . (( len PR) + ( len PR1))) `1 ) by A5, FINSEQ_1:def 7;

          then

           A25: g = (((PR ^ PR1) . ( len (PR ^ PR1))) `1 ) by FINSEQ_1: 22;

          1 <= ( len (PR ^ PR1)) by A10, Th6;

          then ( len (PR ^ PR1)) in ( dom (PR ^ PR1)) by FINSEQ_3: 25;

          then

           A26: g = ((PR3 . ( len (PR ^ PR1))) `1 ) by A25, FINSEQ_1:def 7;

          1 <= ( len (PR ^ PR1)) by A10, Th6;

          hence (PR3,n) is_a_correct_step by A1, A17, A18, A20, A23, A24, A19, A26, Def7;

        end;

        now

           A27:

          now

            given k be Nat such that

             A28: k in ( dom PR1) and

             A29: n = (( len PR) + k);

            

             A30: 1 <= k by A28, FINSEQ_3: 25;

            

             A31: k <= ( len PR1) by A28, FINSEQ_3: 25;

            then n <= (( len PR1) + ( len PR)) by A29, XREAL_1: 6;

            then

             A32: n <= ( len (PR ^ PR1)) by FINSEQ_1: 22;

            k <= n by A29, NAT_1: 11;

            then

             A33: 1 <= n by A30, XXREAL_0: 2;

            (PR1,k) is_a_correct_step by A4, A30, A31;

            then ((PR ^ PR1),n) is_a_correct_step by A29, A30, A31, Th35;

            hence (PR3,n) is_a_correct_step by A33, A32, Th34;

          end;

           A34:

          now

            assume

             A35: n in ( dom PR);

            then

             A36: 1 <= n by FINSEQ_3: 25;

            

             A37: n <= ( len PR) by A35, FINSEQ_3: 25;

            ( len PR) <= ( len (PR ^ PR1)) by Th6;

            then

             A38: n <= ( len (PR ^ PR1)) by A37, XXREAL_0: 2;

            (PR,n) is_a_correct_step by A6, A36, A37;

            then ((PR ^ PR1),n) is_a_correct_step by A36, A37, Th34;

            hence (PR3,n) is_a_correct_step by A36, A38, Th34;

          end;

          assume n in ( dom (PR ^ PR1));

          hence (PR3,n) is_a_correct_step by A34, A27, FINSEQ_1: 25;

        end;

        hence (PR3,n) is_a_correct_step by A11, A12, FINSEQ_1: 25;

      end;

      then

       A39: PR3 is a_proof;

      (PR3 . ( len PR3)) = (PR3 . (( len (PR ^ PR1)) + ( len PR2))) by FINSEQ_1: 22;

      then (PR3 . ( len PR3)) = (PR3 . (( len (PR ^ PR1)) + 1)) by FINSEQ_1: 39;

      then (PR3 . ( len PR3)) = (PR2 . 1) by A9, FINSEQ_1:def 7;

      then (PR3 . ( len PR3)) = [(( Ant ( Ant f)) ^ <*p*>), 4] by FINSEQ_1: 40;

      then ((PR3 . ( len PR3)) `1 ) = (( Ant ( Ant f)) ^ <*p*>);

      hence thesis by A39;

    end;

    theorem :: CALCUL_1:39

    

     Th39: ( Ant f) = ( Ant g) & |- f & |- g implies |- (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>)

    proof

      assume that

       A1: ( Ant f) = ( Ant g) and

       A2: |- f and

       A3: |- g;

      consider PR1 such that

       A4: PR1 is a_proof and

       A5: g = ((PR1 . ( len PR1)) `1 ) by A3;

      consider PR such that

       A6: PR is a_proof and

       A7: f = ((PR . ( len PR)) `1 ) by A2;

      

       A8: (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>) in ( set_of_CQC-WFF-seq Al) by Def6;

      now

        let a be object;

        assume a in ( rng <* [(( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>), 5]*>);

        then a in { [(( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>), 5]} by FINSEQ_1: 38;

        then a = [(( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>), 5] by TARSKI:def 1;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A8, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng <* [(( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>), 5]*>) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR2 = <* [(( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>), 5]*> as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A9: 1 in ( dom PR2) by FINSEQ_1: 38;

      set PR3 = ((PR ^ PR1) ^ PR2);

      reconsider PR3 as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      

       A10: PR <> {} by A6;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len PR3);

        then

         A11: n in ( dom PR3) by FINSEQ_3: 25;

         A12:

        now

          given k be Nat such that

           A13: k in ( dom PR2) and

           A14: n = (( len (PR ^ PR1)) + k);

          k in ( Seg 1) by A13, FINSEQ_1: 38;

          then

           A15: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then

           A16: (PR2 . k) = [(( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>), 5] by FINSEQ_1: 40;

          then ((PR2 . k) `1 ) = (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>);

          then

           A17: ((PR3 . n) `1 ) = (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>) by A13, A14, FINSEQ_1:def 7;

          ((PR2 . k) `2 ) = 5 by A16;

          then

           A18: ((PR3 . n) `2 ) = 5 by A13, A14, FINSEQ_1:def 7;

          

           A19: ( len (PR ^ PR1)) < n by A14, A15, NAT_1: 13;

          

           A20: 1 <= ( len PR) by A10, Th6;

          then ( len PR) in ( dom PR) by FINSEQ_3: 25;

          then

           A21: f = (((PR ^ PR1) . ( len PR)) `1 ) by A7, FINSEQ_1:def 7;

          

           A22: PR1 <> {} by A4;

          then

           A23: ( len PR) < ( len (PR ^ PR1)) by Th6;

          then ( len PR) in ( dom (PR ^ PR1)) by A20, FINSEQ_3: 25;

          then

           A24: f = ((PR3 . ( len PR)) `1 ) by A21, FINSEQ_1:def 7;

          1 <= ( len PR1) by A22, Th6;

          then ( len PR1) in ( dom PR1) by FINSEQ_3: 25;

          then g = (((PR ^ PR1) . (( len PR) + ( len PR1))) `1 ) by A5, FINSEQ_1:def 7;

          then

           A25: g = (((PR ^ PR1) . ( len (PR ^ PR1))) `1 ) by FINSEQ_1: 22;

          1 <= ( len (PR ^ PR1)) by A10, Th6;

          then ( len (PR ^ PR1)) in ( dom (PR ^ PR1)) by FINSEQ_3: 25;

          then

           A26: g = ((PR3 . ( len (PR ^ PR1))) `1 ) by A25, FINSEQ_1:def 7;

          1 <= ( len (PR ^ PR1)) by A10, Th6;

          hence (PR3,n) is_a_correct_step by A1, A17, A18, A20, A23, A24, A19, A26, Def7;

        end;

        now

           A27:

          now

            given k be Nat such that

             A28: k in ( dom PR1) and

             A29: n = (( len PR) + k);

            

             A30: 1 <= k by A28, FINSEQ_3: 25;

            

             A31: k <= ( len PR1) by A28, FINSEQ_3: 25;

            then n <= (( len PR1) + ( len PR)) by A29, XREAL_1: 6;

            then

             A32: n <= ( len (PR ^ PR1)) by FINSEQ_1: 22;

            k <= n by A29, NAT_1: 11;

            then

             A33: 1 <= n by A30, XXREAL_0: 2;

            (PR1,k) is_a_correct_step by A4, A30, A31;

            then ((PR ^ PR1),n) is_a_correct_step by A29, A30, A31, Th35;

            hence (PR3,n) is_a_correct_step by A33, A32, Th34;

          end;

           A34:

          now

            assume

             A35: n in ( dom PR);

            then

             A36: 1 <= n by FINSEQ_3: 25;

            

             A37: n <= ( len PR) by A35, FINSEQ_3: 25;

            ( len PR) <= ( len (PR ^ PR1)) by Th6;

            then

             A38: n <= ( len (PR ^ PR1)) by A37, XXREAL_0: 2;

            (PR,n) is_a_correct_step by A6, A36, A37;

            then ((PR ^ PR1),n) is_a_correct_step by A36, A37, Th34;

            hence (PR3,n) is_a_correct_step by A36, A38, Th34;

          end;

          assume n in ( dom (PR ^ PR1));

          hence (PR3,n) is_a_correct_step by A34, A27, FINSEQ_1: 25;

        end;

        hence (PR3,n) is_a_correct_step by A11, A12, FINSEQ_1: 25;

      end;

      then

       A39: PR3 is a_proof;

      (PR3 . ( len PR3)) = (PR3 . (( len (PR ^ PR1)) + ( len PR2))) by FINSEQ_1: 22;

      then (PR3 . ( len PR3)) = (PR3 . (( len (PR ^ PR1)) + 1)) by FINSEQ_1: 39;

      then (PR3 . ( len PR3)) = (PR2 . 1) by A9, FINSEQ_1:def 7;

      then (PR3 . ( len PR3)) = [(( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>), 5] by FINSEQ_1: 40;

      then ((PR3 . ( len PR3)) `1 ) = (( Ant f) ^ <*(( Suc f) '&' ( Suc g))*>);

      hence thesis by A39;

    end;

    theorem :: CALCUL_1:40

    

     Th40: (p '&' q) = ( Suc f) & |- f implies |- (( Ant f) ^ <*p*>)

    proof

      assume that

       A1: (p '&' q) = ( Suc f) and

       A2: |- f;

      consider PR such that

       A3: PR is a_proof and

       A4: ((PR . ( len PR)) `1 ) = f by A2;

      

       A5: (( Ant f) ^ <*p*>) in ( set_of_CQC-WFF-seq Al) by Def6;

      now

        let a be object;

        assume a in ( rng <* [(( Ant f) ^ <*p*>), 6]*>);

        then a in { [(( Ant f) ^ <*p*>), 6]} by FINSEQ_1: 38;

        then a = [(( Ant f) ^ <*p*>), 6] by TARSKI:def 1;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A5, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng <* [(( Ant f) ^ <*p*>), 6]*>) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR1 = <* [(( Ant f) ^ <*p*>), 6]*> as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A6: 1 in ( dom PR1) by FINSEQ_1: 38;

      set PR2 = (PR ^ PR1);

      reconsider PR2 as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      

       A7: PR <> {} by A3;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len PR2);

        then

         A8: n in ( dom PR2) by FINSEQ_3: 25;

         A9:

        now

          

           A10: 1 <= ( len PR) by A7, Th6;

          then ( len PR) in ( dom PR) by FINSEQ_3: 25;

          then

           A11: f = ((PR2 . ( len PR)) `1 ) by A4, FINSEQ_1:def 7;

          given k be Nat such that

           A12: k in ( dom PR1) and

           A13: n = (( len PR) + k);

          k in ( Seg 1) by A12, FINSEQ_1: 38;

          then

           A14: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then

           A15: (PR1 . k) = [(( Ant f) ^ <*p*>), 6] by FINSEQ_1: 40;

          then ((PR1 . k) `1 ) = (( Ant f) ^ <*p*>);

          then

           A16: ((PR2 . n) `1 ) = (( Ant f) ^ <*p*>) by A12, A13, FINSEQ_1:def 7;

          ((PR1 . k) `2 ) = 6 by A15;

          then

           A17: ((PR2 . n) `2 ) = 6 by A12, A13, FINSEQ_1:def 7;

          ( len PR) < n by A13, A14, NAT_1: 13;

          hence (PR2,n) is_a_correct_step by A1, A16, A17, A10, A11, Def7;

        end;

        now

          assume n in ( dom PR);

          then

           A18: 1 <= n & n <= ( len PR) by FINSEQ_3: 25;

          then (PR,n) is_a_correct_step by A3;

          hence (PR2,n) is_a_correct_step by A18, Th34;

        end;

        hence (PR2,n) is_a_correct_step by A8, A9, FINSEQ_1: 25;

      end;

      then

       A19: PR2 is a_proof;

      (PR2 . ( len PR2)) = (PR2 . (( len PR) + ( len PR1))) by FINSEQ_1: 22;

      then (PR2 . ( len PR2)) = (PR2 . (( len PR) + 1)) by FINSEQ_1: 39;

      then (PR2 . ( len PR2)) = (PR1 . 1) by A6, FINSEQ_1:def 7;

      then (PR2 . ( len PR2)) = [(( Ant f) ^ <*p*>), 6] by FINSEQ_1: 40;

      then ((PR2 . ( len PR2)) `1 ) = (( Ant f) ^ <*p*>);

      hence thesis by A19;

    end;

    theorem :: CALCUL_1:41

    

     Th41: (p '&' q) = ( Suc f) & |- f implies |- (( Ant f) ^ <*q*>)

    proof

      assume that

       A1: (p '&' q) = ( Suc f) and

       A2: |- f;

      consider PR such that

       A3: PR is a_proof and

       A4: ((PR . ( len PR)) `1 ) = f by A2;

      

       A5: (( Ant f) ^ <*q*>) in ( set_of_CQC-WFF-seq Al) by Def6;

      now

        let a be object;

        assume a in ( rng <* [(( Ant f) ^ <*q*>), 7]*>);

        then a in { [(( Ant f) ^ <*q*>), 7]} by FINSEQ_1: 38;

        then a = [(( Ant f) ^ <*q*>), 7] by TARSKI:def 1;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A5, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng <* [(( Ant f) ^ <*q*>), 7]*>) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR1 = <* [(( Ant f) ^ <*q*>), 7]*> as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A6: 1 in ( dom PR1) by FINSEQ_1: 38;

      set PR2 = (PR ^ PR1);

      reconsider PR2 as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      

       A7: PR <> {} by A3;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len PR2);

        then

         A8: n in ( dom PR2) by FINSEQ_3: 25;

         A9:

        now

          

           A10: 1 <= ( len PR) by A7, Th6;

          then ( len PR) in ( dom PR) by FINSEQ_3: 25;

          then

           A11: f = ((PR2 . ( len PR)) `1 ) by A4, FINSEQ_1:def 7;

          given k be Nat such that

           A12: k in ( dom PR1) and

           A13: n = (( len PR) + k);

          k in ( Seg 1) by A12, FINSEQ_1: 38;

          then

           A14: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then

           A15: (PR1 . k) = [(( Ant f) ^ <*q*>), 7] by FINSEQ_1: 40;

          then ((PR1 . k) `1 ) = (( Ant f) ^ <*q*>);

          then

           A16: ((PR2 . n) `1 ) = (( Ant f) ^ <*q*>) by A12, A13, FINSEQ_1:def 7;

          ((PR1 . k) `2 ) = 7 by A15;

          then

           A17: ((PR2 . n) `2 ) = 7 by A12, A13, FINSEQ_1:def 7;

          ( len PR) < n by A13, A14, NAT_1: 13;

          hence (PR2,n) is_a_correct_step by A1, A16, A17, A10, A11, Def7;

        end;

        now

          assume n in ( dom PR);

          then

           A18: 1 <= n & n <= ( len PR) by FINSEQ_3: 25;

          then (PR,n) is_a_correct_step by A3;

          hence (PR2,n) is_a_correct_step by A18, Th34;

        end;

        hence (PR2,n) is_a_correct_step by A8, A9, FINSEQ_1: 25;

      end;

      then

       A19: PR2 is a_proof;

      (PR2 . ( len PR2)) = (PR2 . (( len PR) + ( len PR1))) by FINSEQ_1: 22;

      then (PR2 . ( len PR2)) = (PR2 . (( len PR) + 1)) by FINSEQ_1: 39;

      then (PR2 . ( len PR2)) = (PR1 . 1) by A6, FINSEQ_1:def 7;

      then (PR2 . ( len PR2)) = [(( Ant f) ^ <*q*>), 7] by FINSEQ_1: 40;

      then ((PR2 . ( len PR2)) `1 ) = (( Ant f) ^ <*q*>);

      hence thesis by A19;

    end;

    theorem :: CALCUL_1:42

    

     Th42: ( Suc f) = ( All (x,p)) & |- f implies |- (( Ant f) ^ <*(p . (x,y))*>)

    proof

      assume that

       A1: ( Suc f) = ( All (x,p)) and

       A2: |- f;

      consider PR such that

       A3: PR is a_proof and

       A4: ((PR . ( len PR)) `1 ) = f by A2;

      

       A5: (( Ant f) ^ <*(p . (x,y))*>) in ( set_of_CQC-WFF-seq Al) by Def6;

      now

        let a be object;

        assume a in ( rng <* [(( Ant f) ^ <*(p . (x,y))*>), 8]*>);

        then a in { [(( Ant f) ^ <*(p . (x,y))*>), 8]} by FINSEQ_1: 38;

        then a = [(( Ant f) ^ <*(p . (x,y))*>), 8] by TARSKI:def 1;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A5, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng <* [(( Ant f) ^ <*(p . (x,y))*>), 8]*>) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR1 = <* [(( Ant f) ^ <*(p . (x,y))*>), 8]*> as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A6: 1 in ( dom PR1) by FINSEQ_1: 38;

      set PR2 = (PR ^ PR1);

      reconsider PR2 as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      

       A7: PR <> {} by A3;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len PR2);

        then

         A8: n in ( dom PR2) by FINSEQ_3: 25;

         A9:

        now

          

           A10: 1 <= ( len PR) by A7, Th6;

          then ( len PR) in ( dom PR) by FINSEQ_3: 25;

          then

           A11: f = ((PR2 . ( len PR)) `1 ) by A4, FINSEQ_1:def 7;

          given k be Nat such that

           A12: k in ( dom PR1) and

           A13: n = (( len PR) + k);

          k in ( Seg 1) by A12, FINSEQ_1: 38;

          then

           A14: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then

           A15: (PR1 . k) = [(( Ant f) ^ <*(p . (x,y))*>), 8] by FINSEQ_1: 40;

          then ((PR1 . k) `1 ) = (( Ant f) ^ <*(p . (x,y))*>);

          then

           A16: ((PR2 . n) `1 ) = (( Ant f) ^ <*(p . (x,y))*>) by A12, A13, FINSEQ_1:def 7;

          ((PR1 . k) `2 ) = 8 by A15;

          then

           A17: ((PR2 . n) `2 ) = 8 by A12, A13, FINSEQ_1:def 7;

          ( len PR) < n by A13, A14, NAT_1: 13;

          hence (PR2,n) is_a_correct_step by A1, A16, A17, A10, A11, Def7;

        end;

        now

          assume n in ( dom PR);

          then

           A18: 1 <= n & n <= ( len PR) by FINSEQ_3: 25;

          then (PR,n) is_a_correct_step by A3;

          hence (PR2,n) is_a_correct_step by A18, Th34;

        end;

        hence (PR2,n) is_a_correct_step by A8, A9, FINSEQ_1: 25;

      end;

      then

       A19: PR2 is a_proof;

      (PR2 . ( len PR2)) = (PR2 . (( len PR) + ( len PR1))) by FINSEQ_1: 22;

      then (PR2 . ( len PR2)) = (PR2 . (( len PR) + 1)) by FINSEQ_1: 39;

      then (PR2 . ( len PR2)) = (PR1 . 1) by A6, FINSEQ_1:def 7;

      then (PR2 . ( len PR2)) = [(( Ant f) ^ <*(p . (x,y))*>), 8] by FINSEQ_1: 40;

      then ((PR2 . ( len PR2)) `1 ) = (( Ant f) ^ <*(p . (x,y))*>);

      hence thesis by A19;

    end;

    theorem :: CALCUL_1:43

    

     Th43: ( Suc f) = (p . (x,y)) & not y in ( still_not-bound_in ( Ant f)) & not y in ( still_not-bound_in ( All (x,p))) & |- f implies |- (( Ant f) ^ <*( All (x,p))*>)

    proof

      assume that

       A1: ( Suc f) = (p . (x,y)) & not y in ( still_not-bound_in ( Ant f)) & not y in ( still_not-bound_in ( All (x,p))) and

       A2: |- f;

      consider PR such that

       A3: PR is a_proof and

       A4: ((PR . ( len PR)) `1 ) = f by A2;

      

       A5: (( Ant f) ^ <*( All (x,p))*>) in ( set_of_CQC-WFF-seq Al) by Def6;

      now

        let a be object;

        assume a in ( rng <* [(( Ant f) ^ <*( All (x,p))*>), 9]*>);

        then a in { [(( Ant f) ^ <*( All (x,p))*>), 9]} by FINSEQ_1: 38;

        then a = [(( Ant f) ^ <*( All (x,p))*>), 9] by TARSKI:def 1;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A5, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng <* [(( Ant f) ^ <*( All (x,p))*>), 9]*>) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR1 = <* [(( Ant f) ^ <*( All (x,p))*>), 9]*> as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A6: 1 in ( dom PR1) by FINSEQ_1: 38;

      set PR2 = (PR ^ PR1);

      reconsider PR2 as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      

       A7: PR <> {} by A3;

      now

        let n be Nat;

        assume 1 <= n & n <= ( len PR2);

        then

         A8: n in ( dom PR2) by FINSEQ_3: 25;

         A9:

        now

          

           A10: 1 <= ( len PR) by A7, Th6;

          then ( len PR) in ( dom PR) by FINSEQ_3: 25;

          then

           A11: f = ((PR2 . ( len PR)) `1 ) by A4, FINSEQ_1:def 7;

          given k be Nat such that

           A12: k in ( dom PR1) and

           A13: n = (( len PR) + k);

          k in ( Seg 1) by A12, FINSEQ_1: 38;

          then

           A14: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then

           A15: (PR1 . k) = [(( Ant f) ^ <*( All (x,p))*>), 9] by FINSEQ_1: 40;

          then ((PR1 . k) `1 ) = (( Ant f) ^ <*( All (x,p))*>);

          then

           A16: ((PR2 . n) `1 ) = (( Ant f) ^ <*( All (x,p))*>) by A12, A13, FINSEQ_1:def 7;

          ((PR1 . k) `2 ) = 9 by A15;

          then

           A17: ((PR2 . n) `2 ) = 9 by A12, A13, FINSEQ_1:def 7;

          ( len PR) < n by A13, A14, NAT_1: 13;

          hence (PR2,n) is_a_correct_step by A1, A16, A17, A10, A11, Def7;

        end;

        now

          assume n in ( dom PR);

          then

           A18: 1 <= n & n <= ( len PR) by FINSEQ_3: 25;

          then (PR,n) is_a_correct_step by A3;

          hence (PR2,n) is_a_correct_step by A18, Th34;

        end;

        hence (PR2,n) is_a_correct_step by A8, A9, FINSEQ_1: 25;

      end;

      then

       A19: PR2 is a_proof;

      (PR2 . ( len PR2)) = (PR2 . (( len PR) + ( len PR1))) by FINSEQ_1: 22;

      then (PR2 . ( len PR2)) = (PR2 . (( len PR) + 1)) by FINSEQ_1: 39;

      then (PR2 . ( len PR2)) = (PR1 . 1) by A6, FINSEQ_1:def 7;

      then (PR2 . ( len PR2)) = [(( Ant f) ^ <*( All (x,p))*>), 9] by FINSEQ_1: 40;

      then ((PR2 . ( len PR2)) `1 ) = (( Ant f) ^ <*( All (x,p))*>);

      hence thesis by A19;

    end;

    theorem :: CALCUL_1:44

    

     Th44: |- f & |- (( Ant f) ^ <*( 'not' ( Suc f))*>) implies |- (( Ant f) ^ <*p*>)

    proof

      assume that

       A1: |- f and

       A2: |- (( Ant f) ^ <*( 'not' ( Suc f))*>);

      set f1 = ((( Ant f) ^ <*( 'not' p)*>) ^ <*( Suc f)*>);

      ( Ant f1) = (( Ant f) ^ <*( 'not' p)*>) & ( Suc f) = ( Suc f1) by Th5;

      then

       A3: |- f1 by A1, Th8, Th36;

      set f3 = ((( Ant f) ^ <*( 'not' p)*>) ^ <*( 'not' ( Suc f))*>);

      set f2 = (( Ant f) ^ <*( 'not' ( Suc f))*>);

      ( Suc f2) = ( 'not' ( Suc f)) by Th5;

      then

       A4: ( Suc f2) = ( Suc f3) by Th5;

      ( Ant f3) = (( Ant f) ^ <*( 'not' p)*>) & ( Ant f2) = ( Ant f) by Th5;

      then

       A5: |- f3 by A2, A4, Th8, Th36;

      ( Suc f1) = ( Suc f) by Th5;

      then

       A6: ( 'not' ( Suc f1)) = ( Suc f3) by Th5;

      

       A7: 1 < ( len f1) by Th9;

      

       A8: ( Ant f1) = (( Ant f) ^ <*( 'not' p)*>) by Th5;

      then ( Ant f1) = ( Ant f3) & ( Suc ( Ant f1)) = ( 'not' p) by Th5;

      then |- (( Ant ( Ant f1)) ^ <*p*>) by A3, A5, A6, A7, Th38;

      hence thesis by A8, Th5;

    end;

    theorem :: CALCUL_1:45

    

     Th45: 1 <= ( len f) & |- f & |- (f ^ <*p*>) implies |- (( Ant f) ^ <*p*>)

    proof

      assume that

       A1: 1 <= ( len f) and

       A2: |- f and

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

      set f2 = ((( Ant f) ^ <*( 'not' ( Suc f))*>) ^ <*( 'not' ( Suc f))*>);

      set f1 = ((( Ant f) ^ <*( 'not' ( Suc f))*>) ^ <*( Suc f)*>);

      

       A4: ( Ant f2) = (( Ant f) ^ <*( 'not' ( Suc f))*>) by Th5;

      then

       A5: ( len ( Ant f2)) in ( dom ( Ant f2)) by Th10;

      ((( Ant f) ^ <*( 'not' ( Suc f))*>) . (( len ( Ant f)) + 1)) = ( 'not' ( Suc f)) by FINSEQ_1: 42;

      then (( Ant f2) . (( len ( Ant f)) + 1)) = ( 'not' ( Suc f)) by Th5;

      then (( Ant f2) . (( len ( Ant f)) + 1)) = ( Suc f2) by Th5;

      then (( Ant f2) . ( len ( Ant f2))) = ( Suc f2) by A4, FINSEQ_2: 16;

      then

       A6: |- f2 by A5, Lm2, Th33;

      set f4 = (( Ant f1) ^ <*p*>);

      f2 = (( Ant f1) ^ <*( 'not' ( Suc f))*>) by Th5;

      then

       A7: f2 = (( Ant f1) ^ <*( 'not' ( Suc f1))*>) by Th5;

      ( Ant f1) = (( Ant f) ^ <*( 'not' ( Suc f))*>) & ( Suc f1) = ( Suc f) by Th5;

      then |- f1 by A2, Th8, Th36;

      then

       A8: |- (( Ant f1) ^ <*p*>) by A6, A7, Th44;

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

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

      then (1 + 1) <= (( len f) + ( len <*p*>)) by FINSEQ_1: 39;

      then (1 + 1) <= ( len f3) by FINSEQ_1: 22;

      then

       A9: 1 < ( len f3) by NAT_1: 13;

      

       A10: ( Ant f1) = (( Ant f) ^ <*( 'not' ( Suc f))*>) by Th5;

      then ( Suc ( Ant f1)) = ( 'not' ( Suc f)) by Th5;

      then ( Suc ( Ant f1)) = ( 'not' ( Suc ( Ant f3))) by Th5;

      then

       A11: ( Suc ( Ant f4)) = ( 'not' ( Suc ( Ant f3))) by Th5;

      1 <= ( len ( Ant f1)) by A10, Th10;

      then (1 + 1) <= (( len ( Ant f1)) + 1) by XREAL_1: 6;

      then (1 + 1) <= (( len ( Ant f1)) + ( len <*p*>)) by FINSEQ_1: 39;

      then (1 + 1) <= ( len f4) by FINSEQ_1: 22;

      then

       A12: 1 < ( len f4) by NAT_1: 13;

      ( Ant f4) = ( Ant f1) by Th5;

      then ( Ant ( Ant f4)) = ( Ant f) by A10, Th5;

      then

       A13: ( Ant ( Ant f4)) = ( Ant ( Ant f3)) by Th5;

      ( Suc f4) = p by Th5;

      then |- (( Ant ( Ant f3)) ^ <*( Suc f3)*>) by A3, A8, A9, A12, A13, A11, Th5, Th37;

      then |- (( Ant f) ^ <*( Suc f3)*>) by Th5;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:46

    

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

    proof

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

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

      assume

       A1: |- f1;

      

       A2: ( Ant f1) = (f ^ <*p*>) by Th5;

      then

       A3: ( Ant ( Ant f1)) = f by Th5;

      set f4 = (((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*( 'not' p)*>) ^ <*( 'not' p)*>);

      set f3 = (((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*p*>) ^ <*( 'not' q)*>);

      

       A4: 1 < ( len f4) by Th9;

      

       A5: ( Suc (( Ant f2) ^ <*( 'not' p)*>)) = ( 'not' p) by Th5;

      then

       A6: ( Suc (( Ant f2) ^ <*( 'not' p)*>)) = ( Suc f4) by Th5;

      ( Ant f3) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*p*>) by Th5;

      then ( Ant f3) = (( Ant ( Ant f1)) ^ ( <*( 'not' q)*> ^ <*p*>)) by FINSEQ_1: 32;

      then

       A7: ( Ant f3) = (( Ant ( Ant f1)) ^ <*( 'not' q), p*>) by FINSEQ_1:def 9;

      then (( Ant f3) . (( len f) + 1)) = ( 'not' q) by A3, Th14;

      then

       A8: (( Ant f3) . (( len f) + 1)) = ( Suc f3) by Th5;

      ( Suc f1) = q by Th5;

      then

       A9: ( Suc f1) = ( Suc f2) by Th5;

      

       A10: ( Ant f2) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*p*>) by Th5;

      then

       A11: 1 < ( len (( Ant f2) ^ <*( 'not' p)*>)) by Th9;

      ( Suc ( Ant f1)) = p & ( 0 + 1) <= ( len ( Ant f1)) by A2, Th5, Th10;

      then

       A12: |- f2 by A1, A10, A9, Th13, Th36;

      1 in ( dom <*( 'not' q), p*>) by Th14;

      then

       A13: (( len f) + 1) in ( dom ( Ant f3)) by A3, A7, FINSEQ_1: 28;

      ( Suc f2) = q & ( Ant f2) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*p*>) by Th5;

      then |- (( Ant f2) ^ <*( 'not' ( Suc f2))*>) by A8, A13, Lm2, Th33;

      then

       A14: |- (( Ant f2) ^ <*( 'not' p)*>) by A12, Th44;

      

       A15: ( Ant f4) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*( 'not' p)*>) by Th5;

      then ( Ant f4) = (( Ant ( Ant f1)) ^ ( <*( 'not' q)*> ^ <*( 'not' p)*>)) by FINSEQ_1: 32;

      then

       A16: ( Ant f4) = (( Ant ( Ant f1)) ^ <*( 'not' q), ( 'not' p)*>) by FINSEQ_1:def 9;

      then (( Ant f4) . (( len f) + 2)) = ( 'not' p) by A3, Th14;

      then

       A17: (( Ant f4) . (( len f) + 2)) = ( Suc f4) by Th5;

      2 in ( dom <*( 'not' q), ( 'not' p)*>) by Th14;

      then (( len f) + 2) in ( dom ( Ant f4)) by A3, A16, FINSEQ_1: 28;

      then

       A18: |- f4 by A17, Lm2, Th33;

      

       A19: ( Ant (( Ant f2) ^ <*( 'not' p)*>)) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*p*>) by A10, Th5;

      then ( Suc ( Ant (( Ant f2) ^ <*( 'not' p)*>))) = p by Th5;

      then

       A20: ( 'not' ( Suc ( Ant (( Ant f2) ^ <*( 'not' p)*>)))) = ( Suc ( Ant f4)) by A15, Th5;

      

       A21: ( Ant ( Ant (( Ant f2) ^ <*( 'not' p)*>))) = (( Ant ( Ant f1)) ^ <*( 'not' q)*>) by A19, Th5;

      then ( Ant ( Ant f4)) = ( Ant ( Ant (( Ant f2) ^ <*( 'not' p)*>))) by A15, Th5;

      hence thesis by A3, A14, A18, A11, A4, A21, A20, A5, A6, Th37;

    end;

    theorem :: CALCUL_1:47

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

    proof

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

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

      assume

       A1: |- f1;

      

       A2: ( Ant f2) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*( 'not' p)*>) by Th5;

      ( Suc f1) = ( 'not' q) by Th5;

      then

       A3: ( Suc f1) = ( Suc f2) by Th5;

      

       A4: ( Ant f1) = (f ^ <*( 'not' p)*>) by Th5;

      then

       A5: ( Ant ( Ant f1)) = f by Th5;

      ( Suc ( Ant f1)) = ( 'not' p) & ( 0 + 1) <= ( len ( Ant f1)) by A4, Th5, Th10;

      then

       A6: |- f2 by A1, A2, A3, Th13, Th36;

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

      set f3 = (((( Ant ( Ant f1)) ^ <*q*>) ^ <*( 'not' p)*>) ^ <*q*>);

      

       A7: 1 < ( len f4) by Th9;

      

       A8: ( Ant f3) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*( 'not' p)*>) by Th5;

      then

       A9: 1 < ( len (( Ant f3) ^ <*p*>)) by Th9;

      ( Ant f3) = (( Ant ( Ant f1)) ^ ( <*q*> ^ <*( 'not' p)*>)) by A8, FINSEQ_1: 32;

      then

       A10: ( Ant f3) = (( Ant ( Ant f1)) ^ <*q, ( 'not' p)*>) by FINSEQ_1:def 9;

      then (( Ant f3) . (( len f) + 1)) = q by A5, Th14;

      then

       A11: (( Ant f3) . (( len f) + 1)) = ( Suc f3) by Th5;

      1 in ( dom <*q, ( 'not' p)*>) by Th14;

      then (( len f) + 1) in ( dom ( Ant f3)) by A5, A10, FINSEQ_1: 28;

      then

       A12: |- f3 by A11, Lm2, Th33;

      

       A13: ( Suc (( Ant f3) ^ <*p*>)) = p by Th5;

      then

       A14: ( Suc (( Ant f3) ^ <*p*>)) = ( Suc f4) by Th5;

      ( Ant f2) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*( 'not' p)*>) by Th5;

      then

       A15: ( Ant f2) = ( Ant f3) by Th5;

      ( Suc f2) = ( 'not' q) by Th5;

      then

       A16: ( Suc f2) = ( 'not' ( Suc f3)) by Th5;

      

       A17: ( Ant f4) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*p*>) by Th5;

      then ( Ant f4) = (( Ant ( Ant f1)) ^ ( <*q*> ^ <*p*>)) by FINSEQ_1: 32;

      then

       A18: ( Ant f4) = (( Ant ( Ant f1)) ^ <*q, p*>) by FINSEQ_1:def 9;

      then (( Ant f4) . (( len f) + 2)) = p by A5, Th14;

      then

       A19: (( Ant f4) . (( len f) + 2)) = ( Suc f4) by Th5;

      2 in ( dom <*q, p*>) by Th14;

      then (( len f) + 2) in ( dom ( Ant f4)) by A5, A18, FINSEQ_1: 28;

      then

       A20: |- f4 by A19, Lm2, Th33;

      

       A21: ( Ant (( Ant f3) ^ <*p*>)) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*( 'not' p)*>) by A8, Th5;

      then ( Suc ( Ant (( Ant f3) ^ <*p*>))) = ( 'not' p) by Th5;

      then

       A22: ( Suc ( Ant (( Ant f3) ^ <*p*>))) = ( 'not' ( Suc ( Ant f4))) by A17, Th5;

      ( 0 + 1) <= ( len f2) by Th10;

      then |- (( Ant f3) ^ <*( 'not' ( Suc f3))*>) by A6, A16, A15, Th3;

      then

       A23: |- (( Ant f3) ^ <*p*>) by A12, Th44;

      

       A24: ( Ant ( Ant (( Ant f3) ^ <*p*>))) = (( Ant ( Ant f1)) ^ <*q*>) by A21, Th5;

      then ( Ant ( Ant f4)) = ( Ant ( Ant (( Ant f3) ^ <*p*>))) by A17, Th5;

      hence thesis by A5, A23, A20, A9, A7, A24, A22, A13, A14, Th37;

    end;

    theorem :: CALCUL_1:48

    

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

    proof

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

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

      assume

       A1: |- f1;

      

       A2: ( Ant f1) = (f ^ <*( 'not' p)*>) by Th5;

      then

       A3: ( Ant ( Ant f1)) = f by Th5;

      set f4 = (((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*p*>) ^ <*p*>);

      set f3 = (((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*( 'not' p)*>) ^ <*( 'not' q)*>);

      

       A4: 1 < ( len f4) by Th9;

      ( Ant f3) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*( 'not' p)*>) by Th5;

      then ( Ant f3) = (( Ant ( Ant f1)) ^ ( <*( 'not' q)*> ^ <*( 'not' p)*>)) by FINSEQ_1: 32;

      then

       A5: ( Ant f3) = (( Ant ( Ant f1)) ^ <*( 'not' q), ( 'not' p)*>) by FINSEQ_1:def 9;

      then (( Ant f3) . (( len f) + 1)) = ( 'not' q) by A3, Th14;

      then

       A6: (( Ant f3) . (( len f) + 1)) = ( Suc f3) by Th5;

      1 in ( dom <*( 'not' q), ( 'not' p)*>) by Th14;

      then

       A7: (( len f) + 1) in ( dom ( Ant f3)) by A3, A5, FINSEQ_1: 28;

      ( Suc f1) = q by Th5;

      then

       A8: ( Suc f1) = ( Suc f2) by Th5;

      

       A9: ( Ant f2) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*( 'not' p)*>) by Th5;

      then

       A10: 1 < ( len (( Ant f2) ^ <*p*>)) by Th9;

      ( Suc ( Ant f1)) = ( 'not' p) & ( 0 + 1) <= ( len ( Ant f1)) by A2, Th5, Th10;

      then

       A11: |- f2 by A1, A9, A8, Th13, Th36;

      ( Suc f2) = q & ( Ant f2) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*( 'not' p)*>) by Th5;

      then |- (( Ant f2) ^ <*( 'not' ( Suc f2))*>) by A6, A7, Lm2, Th33;

      then

       A12: |- (( Ant f2) ^ <*p*>) by A11, Th44;

      

       A13: ( Ant f4) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*p*>) by Th5;

      then ( Ant f4) = (( Ant ( Ant f1)) ^ ( <*( 'not' q)*> ^ <*p*>)) by FINSEQ_1: 32;

      then

       A14: ( Ant f4) = (( Ant ( Ant f1)) ^ <*( 'not' q), p*>) by FINSEQ_1:def 9;

      then (( Ant f4) . (( len f) + 2)) = p by A3, Th14;

      then

       A15: (( Ant f4) . (( len f) + 2)) = ( Suc f4) by Th5;

      2 in ( dom <*( 'not' q), p*>) by Th14;

      then (( len f) + 2) in ( dom ( Ant f4)) by A3, A14, FINSEQ_1: 28;

      then

       A16: |- f4 by A15, Lm2, Th33;

      

       A17: ( Ant (( Ant f2) ^ <*p*>)) = ((( Ant ( Ant f1)) ^ <*( 'not' q)*>) ^ <*( 'not' p)*>) by A9, Th5;

      then ( Ant ( Ant (( Ant f2) ^ <*p*>))) = (( Ant ( Ant f1)) ^ <*( 'not' q)*>) by Th5;

      then

       A18: ( Ant ( Ant f4)) = ( Ant ( Ant (( Ant f2) ^ <*p*>))) by A13, Th5;

      ( Suc ( Ant (( Ant f2) ^ <*p*>))) = ( 'not' p) by A17, Th5;

      then

       A19: ( Suc ( Ant (( Ant f2) ^ <*p*>))) = ( 'not' ( Suc ( Ant f4))) by A13, Th5;

      

       A20: ( Suc f4) = p by Th5;

      then ( Suc (( Ant f2) ^ <*p*>)) = ( Suc f4) by Th5;

      then |- (( Ant ( Ant f4)) ^ <*p*>) by A12, A16, A10, A4, A18, A19, A20, Th37;

      hence thesis by A3, A13, Th5;

    end;

    theorem :: CALCUL_1:49

    

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

    proof

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

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

      assume

       A1: |- f1;

      

       A2: ( Ant f2) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*p*>) by Th5;

      ( Suc f1) = ( 'not' q) by Th5;

      then

       A3: ( Suc f1) = ( Suc f2) by Th5;

      

       A4: ( Ant f1) = (f ^ <*p*>) by Th5;

      then

       A5: ( Ant ( Ant f1)) = f by Th5;

      ( Suc ( Ant f1)) = p & ( 0 + 1) <= ( len ( Ant f1)) by A4, Th5, Th10;

      then

       A6: |- f2 by A1, A2, A3, Th13, Th36;

      set f4 = (((( Ant ( Ant f1)) ^ <*q*>) ^ <*( 'not' p)*>) ^ <*( 'not' p)*>);

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

      

       A7: 1 < ( len f4) by Th9;

      

       A8: ( Ant f3) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*p*>) by Th5;

      then

       A9: 1 < ( len (( Ant f3) ^ <*( 'not' p)*>)) by Th9;

      ( Ant f3) = (( Ant ( Ant f1)) ^ ( <*q*> ^ <*p*>)) by A8, FINSEQ_1: 32;

      then

       A10: ( Ant f3) = (( Ant ( Ant f1)) ^ <*q, p*>) by FINSEQ_1:def 9;

      then (( Ant f3) . (( len f) + 1)) = q by A5, Th14;

      then

       A11: (( Ant f3) . (( len f) + 1)) = ( Suc f3) by Th5;

      1 in ( dom <*q, p*>) by Th14;

      then (( len f) + 1) in ( dom ( Ant f3)) by A5, A10, FINSEQ_1: 28;

      then

       A12: |- f3 by A11, Lm2, Th33;

      

       A13: ( Suc (( Ant f3) ^ <*( 'not' p)*>)) = ( 'not' p) by Th5;

      then

       A14: ( Suc (( Ant f3) ^ <*( 'not' p)*>)) = ( Suc f4) by Th5;

      ( Ant f2) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*p*>) by Th5;

      then

       A15: ( Ant f2) = ( Ant f3) by Th5;

      ( Suc f2) = ( 'not' q) by Th5;

      then

       A16: ( Suc f2) = ( 'not' ( Suc f3)) by Th5;

      

       A17: ( Ant f4) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*( 'not' p)*>) by Th5;

      then ( Ant f4) = (( Ant ( Ant f1)) ^ ( <*q*> ^ <*( 'not' p)*>)) by FINSEQ_1: 32;

      then

       A18: ( Ant f4) = (( Ant ( Ant f1)) ^ <*q, ( 'not' p)*>) by FINSEQ_1:def 9;

      then (( Ant f4) . (( len f) + 2)) = ( 'not' p) by A5, Th14;

      then

       A19: (( Ant f4) . (( len f) + 2)) = ( Suc f4) by Th5;

      2 in ( dom <*q, ( 'not' p)*>) by Th14;

      then (( len f) + 2) in ( dom ( Ant f4)) by A5, A18, FINSEQ_1: 28;

      then

       A20: |- f4 by A19, Lm2, Th33;

      

       A21: ( Ant (( Ant f3) ^ <*( 'not' p)*>)) = ((( Ant ( Ant f1)) ^ <*q*>) ^ <*p*>) by A8, Th5;

      then ( Suc ( Ant (( Ant f3) ^ <*( 'not' p)*>))) = p by Th5;

      then

       A22: ( 'not' ( Suc ( Ant (( Ant f3) ^ <*( 'not' p)*>)))) = ( Suc ( Ant f4)) by A17, Th5;

      ( 0 + 1) <= ( len f2) by Th10;

      then |- (( Ant f3) ^ <*( 'not' ( Suc f3))*>) by A6, A16, A15, Th3;

      then

       A23: |- (( Ant f3) ^ <*( 'not' p)*>) by A12, Th44;

      

       A24: ( Ant ( Ant (( Ant f3) ^ <*( 'not' p)*>))) = (( Ant ( Ant f1)) ^ <*q*>) by A21, Th5;

      then ( Ant ( Ant f4)) = ( Ant ( Ant (( Ant f3) ^ <*( 'not' p)*>))) by A17, Th5;

      hence thesis by A5, A23, A20, A9, A7, A24, A22, A13, A14, Th37;

    end;

    ::$Canceled

    theorem :: CALCUL_1:51

     |- (f ^ <*p*>) implies |- (f ^ <*(p 'or' q)*>)

    proof

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

      assume

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

      

       A2: ( Ant f1) = (f ^ <*(( 'not' p) '&' ( 'not' q))*>) by Th5;

      (( len f) + 1) = (( len f) + ( len <*(( 'not' p) '&' ( 'not' q))*>)) by FINSEQ_1: 39;

      then (( len f) + 1) = ( len ( Ant f1)) by A2, FINSEQ_1: 22;

      then

       A3: (( len f) + 1) in ( dom ( Ant f1)) by A2, Th10;

      

       A4: ( Suc f1) = (( 'not' p) '&' ( 'not' q)) by Th5;

      (( Ant f1) . (( len f) + 1)) = (( 'not' p) '&' ( 'not' q)) by A2, FINSEQ_1: 42;

      then ( Suc f1) is_tail_of ( Ant f1) by A4, A3, Lm2;

      then |- ((f ^ <*(( 'not' p) '&' ( 'not' q))*>) ^ <*( 'not' p)*>) by A2, A4, Th33, Th40;

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

      then

       A5: |- ((f ^ <*p*>) ^ <*(p 'or' q)*>) by QC_LANG2:def 3;

      1 <= ( len (f ^ <*p*>)) by Th10;

      then |- (( Ant (f ^ <*p*>)) ^ <*(p 'or' q)*>) by A1, A5, Th45;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:52

     |- (f ^ <*q*>) implies |- (f ^ <*(p 'or' q)*>)

    proof

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

      assume

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

      

       A2: ( Ant f1) = (f ^ <*(( 'not' p) '&' ( 'not' q))*>) by Th5;

      (( len f) + 1) = (( len f) + ( len <*(( 'not' p) '&' ( 'not' q))*>)) by FINSEQ_1: 39;

      then (( len f) + 1) = ( len ( Ant f1)) by A2, FINSEQ_1: 22;

      then

       A3: (( len f) + 1) in ( dom ( Ant f1)) by A2, Th10;

      

       A4: ( Suc f1) = (( 'not' p) '&' ( 'not' q)) by Th5;

      (( Ant f1) . (( len f) + 1)) = (( 'not' p) '&' ( 'not' q)) by A2, FINSEQ_1: 42;

      then ( Suc f1) is_tail_of ( Ant f1) by A4, A3, Lm2;

      then |- ((f ^ <*(( 'not' p) '&' ( 'not' q))*>) ^ <*( 'not' q)*>) by A2, A4, Th33, Th41;

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

      then

       A5: |- ((f ^ <*q*>) ^ <*(p 'or' q)*>) by QC_LANG2:def 3;

      1 <= ( len (f ^ <*q*>)) by Th10;

      then |- (( Ant (f ^ <*q*>)) ^ <*(p 'or' q)*>) by A1, A5, Th45;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:53

    

     Th52: |- ((f ^ <*p*>) ^ <*r*>) & |- ((f ^ <*q*>) ^ <*r*>) implies |- ((f ^ <*(p 'or' q)*>) ^ <*r*>)

    proof

      set f1 = ((f ^ <*( 'not' r)*>) ^ <*( 'not' p)*>);

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

      

       A1: ( Ant f1) = (f ^ <*( 'not' r)*>) by Th5;

      

       A2: ( Suc f2) = ( 'not' q) by Th5;

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

      then

       A3: |- ((f ^ <*( 'not' r)*>) ^ <*( 'not' p)*>) & |- ((f ^ <*( 'not' r)*>) ^ <*( 'not' q)*>) by Th46;

      ( Suc f1) = ( 'not' p) & ( Ant f2) = (f ^ <*( 'not' r)*>) by Th5;

      then |- (( Ant f1) ^ <*(( 'not' p) '&' ( 'not' q))*>) by A3, A2, Th5, Th39;

      then |- ((f ^ <*( 'not' (( 'not' p) '&' ( 'not' q)))*>) ^ <*r*>) by A1, Th48;

      hence thesis by QC_LANG2:def 3;

    end;

    theorem :: CALCUL_1:54

    

     Th53: |- (f ^ <*p*>) implies |- (f ^ <*( 'not' ( 'not' p))*>)

    proof

      assume

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

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

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

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

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

      set f3 = (( Ant f1) ^ <*( 'not' ( 'not' p))*>);

      

       A2: ( Suc f1) = p by Th5;

      

       A3: ( Ant f1) = ((f ^ <*p*>) ^ <*( 'not' p)*>) by Th5;

      then

       A4: 1 < ( len f3) by Th9;

      

       A5: ( Ant f4) = ((f ^ <*p*>) ^ <*( 'not' ( 'not' p))*>) by Th5;

      then ( Ant f4) = (f ^ ( <*p*> ^ <*( 'not' ( 'not' p))*>)) by FINSEQ_1: 32;

      then

       A6: ( Ant f4) = (f ^ <*p, ( 'not' ( 'not' p))*>) by FINSEQ_1:def 9;

      

       A7: ( Ant f3) = ( Ant f1) by Th5;

      then ( Suc ( Ant f3)) = ( 'not' p) by A3, Th5;

      then

       A8: ( 'not' ( Suc ( Ant f3))) = ( Suc ( Ant f4)) by A5, Th5;

      ( Ant f1) = (f ^ ( <*p*> ^ <*( 'not' p)*>)) by A3, FINSEQ_1: 32;

      then

       A9: ( Ant f1) = (f ^ <*p, ( 'not' p)*>) by FINSEQ_1:def 9;

      (( len f) + 2) = (( len f) + ( len <*p, ( 'not' p)*>)) by FINSEQ_1: 44;

      then (( len f) + 2) = ( len ( Ant f1)) by A9, FINSEQ_1: 22;

      then 1 <= (( len f) + 1) & (( len f) + 1) <= ( len ( Ant f1)) by NAT_1: 11, XREAL_1: 6;

      then

       A10: (( len f) + 1) in ( dom ( Ant f1)) by FINSEQ_3: 25;

      (( Ant f1) . (( len f) + 1)) = p by A9, Th14;

      then

       A11: |- f1 by A2, A10, Lm2, Th33;

      

       A12: 1 < ( len f4) by Th9;

      ( 0 + 1) <= ( len f2) by Th10;

      then

       A13: f2 = (( Ant f2) ^ <*( Suc f2)*>) by Th3;

      

       A14: 1 <= ( len f5) by Th10;

      (( len f) + 2) = (( len f) + ( len <*p, ( 'not' ( 'not' p))*>)) by FINSEQ_1: 44;

      then (( len f) + 2) = ( len ( Ant f4)) by A6, FINSEQ_1: 22;

      then

       A15: (( len f) + 2) in ( dom ( Ant f4)) by A5, Th10;

      

       A16: ( Ant f2) = ((f ^ <*p*>) ^ <*( 'not' p)*>) by Th5;

      then ( Ant f2) = (f ^ ( <*p*> ^ <*( 'not' p)*>)) by FINSEQ_1: 32;

      then

       A17: ( Ant f2) = (f ^ <*p, ( 'not' p)*>) by FINSEQ_1:def 9;

      (( len f) + 2) = (( len f) + ( len <*p, ( 'not' p)*>)) by FINSEQ_1: 44;

      then (( len f) + 2) = ( len ( Ant f2)) by A17, FINSEQ_1: 22;

      then

       A18: (( len f) + 2) in ( dom ( Ant f2)) by A16, Th10;

      

       A19: ( Suc f2) = ( 'not' p) by Th5;

      then

       A20: ( 'not' ( Suc f1)) = ( Suc f2) by Th5;

      (( Ant f2) . (( len f) + 2)) = ( 'not' p) by A17, Th14;

      then

       A21: |- f2 by A18, A19, Lm2, Th33;

      

       A22: ( Suc f4) = ( 'not' ( 'not' p)) by Th5;

      then

       A23: ( Suc f3) = ( Suc f4) by Th5;

      (( Ant f4) . (( len f) + 2)) = ( 'not' ( 'not' p)) by A6, Th14;

      then

       A24: |- f4 by A15, A22, Lm2, Th33;

      ( Ant f1) = ( Ant f2) by A16, Th5;

      then

       A25: |- (( Ant f1) ^ <*( 'not' ( 'not' p))*>) by A11, A21, A13, A20, Th44;

      

       A26: ( Ant ( Ant f3)) = (f ^ <*p*>) by A3, A7, Th5;

      then ( Ant ( Ant f3)) = ( Ant ( Ant f4)) by A5, Th5;

      then |- ((f ^ <*p*>) ^ <*( 'not' ( 'not' p))*>) by A25, A22, A24, A23, A26, A8, A4, A12, Th37;

      then |- (( Ant f5) ^ <*( 'not' ( 'not' p))*>) by A1, A14, Th45;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:55

    

     Th54: |- (f ^ <*( 'not' ( 'not' p))*>) implies |- (f ^ <*p*>)

    proof

      assume

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

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

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

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

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

      set f3 = (( Ant f1) ^ <*p*>);

      

       A2: ( Suc f1) = ( 'not' p) by Th5;

      

       A3: ( Ant f1) = ((f ^ <*( 'not' ( 'not' p))*>) ^ <*( 'not' p)*>) by Th5;

      then

       A4: 1 < ( len f3) by Th9;

      ( Ant f1) = (f ^ ( <*( 'not' ( 'not' p))*> ^ <*( 'not' p)*>)) by A3, FINSEQ_1: 32;

      then

       A5: ( Ant f1) = (f ^ <*( 'not' ( 'not' p)), ( 'not' p)*>) by FINSEQ_1:def 9;

      (( len f) + 2) = (( len f) + ( len <*( 'not' ( 'not' p)), ( 'not' p)*>)) by FINSEQ_1: 44;

      then (( len f) + 2) = ( len ( Ant f1)) by A5, FINSEQ_1: 22;

      then

       A6: (( len f) + 2) in ( dom ( Ant f1)) by A3, Th10;

      (( Ant f1) . (( len f) + 2)) = ( 'not' p) by A5, Th14;

      then

       A7: |- f1 by A2, A6, Lm2, Th33;

      

       A8: 1 < ( len f4) by Th9;

      

       A9: ( Ant f2) = ((f ^ <*( 'not' ( 'not' p))*>) ^ <*( 'not' p)*>) by Th5;

      then ( Ant f2) = (f ^ ( <*( 'not' ( 'not' p))*> ^ <*( 'not' p)*>)) by FINSEQ_1: 32;

      then

       A10: ( Ant f2) = (f ^ <*( 'not' ( 'not' p)), ( 'not' p)*>) by FINSEQ_1:def 9;

      (( len f) + 2) = (( len f) + ( len <*( 'not' ( 'not' p)), ( 'not' p)*>)) by FINSEQ_1: 44;

      then (( len f) + 2) = ( len ( Ant f2)) by A10, FINSEQ_1: 22;

      then 1 <= (( len f) + 1) & (( len f) + 1) <= ( len ( Ant f2)) by NAT_1: 11, XREAL_1: 6;

      then

       A11: (( len f) + 1) in ( dom ( Ant f2)) by FINSEQ_3: 25;

      ( 0 + 1) <= ( len f2) by Th10;

      then

       A12: f2 = (( Ant f2) ^ <*( Suc f2)*>) by Th3;

      

       A13: 1 <= ( len f5) by Th10;

      

       A14: ( Ant f4) = ((f ^ <*( 'not' ( 'not' p))*>) ^ <*p*>) by Th5;

      then ( Ant f4) = (f ^ ( <*( 'not' ( 'not' p))*> ^ <*p*>)) by FINSEQ_1: 32;

      then

       A15: ( Ant f4) = (f ^ <*( 'not' ( 'not' p)), p*>) by FINSEQ_1:def 9;

      

       A16: ( Ant f3) = ( Ant f1) by Th5;

      then ( Suc ( Ant f3)) = ( 'not' p) by A3, Th5;

      then

       A17: ( Suc ( Ant f3)) = ( 'not' ( Suc ( Ant f4))) by A14, Th5;

      (( len f) + 2) = (( len f) + ( len <*( 'not' ( 'not' p)), p*>)) by FINSEQ_1: 44;

      then (( len f) + 2) = ( len ( Ant f4)) by A15, FINSEQ_1: 22;

      then

       A18: (( len f) + 2) in ( dom ( Ant f4)) by A14, Th10;

      

       A19: ( Suc f2) = ( 'not' ( 'not' p)) by Th5;

      then

       A20: ( 'not' ( Suc f1)) = ( Suc f2) by Th5;

      (( Ant f2) . (( len f) + 1)) = ( 'not' ( 'not' p)) by A10, Th14;

      then

       A21: |- f2 by A11, A19, Lm2, Th33;

      

       A22: ( Suc f4) = p by Th5;

      then

       A23: ( Suc f3) = ( Suc f4) by Th5;

      (( Ant f4) . (( len f) + 2)) = p by A15, Th14;

      then

       A24: |- f4 by A18, A22, Lm2, Th33;

      ( Ant f1) = ( Ant f2) by A9, Th5;

      then

       A25: |- (( Ant f1) ^ <*p*>) by A7, A21, A12, A20, Th44;

      

       A26: ( Ant ( Ant f3)) = (f ^ <*( 'not' ( 'not' p))*>) by A3, A16, Th5;

      then ( Ant ( Ant f3)) = ( Ant ( Ant f4)) by A14, Th5;

      then |- ((f ^ <*( 'not' ( 'not' p))*>) ^ <*p*>) by A25, A22, A24, A23, A26, A17, A4, A8, Th37;

      then |- (( Ant f5) ^ <*p*>) by A1, A13, Th45;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:56

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

    proof

      assume that

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

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

      set f3 = ((f ^ <*q*>) ^ <*q*>);

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

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

      

       A3: ( Ant f1) = (f ^ <*( 'not' p)*>) by Th5;

      ( Suc (f ^ <*p*>)) = p by Th5;

      then

       A4: ( Suc (f ^ <*p*>)) = ( Suc f1) by Th5;

      

       A5: ( 0 + 1) <= ( len f2) by Th10;

      

       A6: ( Ant f3) = (f ^ <*q*>) by Th5;

      then

       A7: (( Ant f3) . (( len f) + 1)) = q by FINSEQ_1: 42;

      (( len f) + 1) = (( len f) + ( len <*q*>)) by FINSEQ_1: 39;

      then (( len f) + 1) = ( len ( Ant f3)) by A6, FINSEQ_1: 22;

      then

       A8: (( len f) + 1) in ( dom ( Ant f3)) by A6, Th10;

      ( Suc f3) = q by Th5;

      then

       A9: |- f3 by A7, A8, Lm2, Th33;

      

       A10: ( Ant f2) = (f ^ <*( 'not' p)*>) by Th5;

      (( len f) + 1) = (( len f) + ( len <*( 'not' p)*>)) by FINSEQ_1: 39;

      then (( len f) + 1) = ( len ( Ant f2)) by A10, FINSEQ_1: 22;

      then

       A11: (( len f) + 1) in ( dom ( Ant f2)) by A10, Th10;

      

       A12: ( Suc f2) = ( 'not' p) by Th5;

      then

       A13: ( 'not' ( Suc f1)) = ( Suc f2) by Th5;

      (( Ant f2) . (( len f) + 1)) = ( 'not' p) by A10, FINSEQ_1: 42;

      then

       A14: |- f2 by A11, A12, Lm2, Th33;

      ( Ant f1) = ( Ant f2) by A10, Th5;

      then

       A15: |- (( Ant f1) ^ <*( 'not' ( Suc f1))*>) by A14, A5, A13, Th3;

      ( Ant (f ^ <*p*>)) = f by Th5;

      then |- f1 by A2, A3, A4, Th8, Th36;

      then |- (( Ant f1) ^ <*q*>) by A15, Th44;

      then |- ((f ^ <*(( 'not' p) 'or' q)*>) ^ <*q*>) by A3, A9, Th52;

      then

       A16: |- ((f ^ <*( 'not' (( 'not' ( 'not' p)) '&' ( 'not' q)))*>) ^ <*q*>) by QC_LANG2:def 3;

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

      set f5 = (( Ant f4) ^ <*p*>);

      set f6 = (( Ant f4) ^ <*( 'not' q)*>);

      

       A17: ( Ant f5) = ( Ant f4) & ( Suc f5) = p by Th5;

      

       A18: ( Ant f6) = ( Ant f4) & ( Suc f6) = ( 'not' q) by Th5;

      

       A19: ( Suc f4) = (( 'not' ( 'not' p)) '&' ( 'not' q)) by Th5;

      then |- (( Ant f4) ^ <*( 'not' ( 'not' p))*>) by A16, Th40, Th48;

      then

       A20: |- (( Ant f4) ^ <*p*>) by Th54;

       |- (( Ant f4) ^ <*( 'not' q)*>) by A16, A19, Th41, Th48;

      then |- (( Ant f4) ^ <*(p '&' ( 'not' q))*>) by A20, A17, A18, Th39;

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

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

      then

       A21: |- ((f ^ <*(p => q)*>) ^ <*q*>) by QC_LANG2:def 2;

      1 <= ( len (f ^ <*(p => q)*>)) by Th10;

      then |- (( Ant (f ^ <*(p => q)*>)) ^ <*q*>) by A1, A21, Th45;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:57

    

     Th56: (( 'not' p) . (x,y)) = ( 'not' (p . (x,y)))

    proof

      set S = [p, ( Sbst (x,y))];

      (S `1 ) = p & (S `2 ) = ( Sbst (x,y));

      then (( 'not' p) . (x,y)) = ( CQC_Sub [( 'not' p), ( Sbst (x,y))]) & ( Sub_not S) = [( 'not' p), ( Sbst (x,y))] by SUBSTUT1:def 20, SUBSTUT2:def 1;

      then (( 'not' p) . (x,y)) = ( 'not' ( CQC_Sub S)) by SUBSTUT1: 29;

      hence thesis by SUBSTUT2:def 1;

    end;

    theorem :: CALCUL_1:58

    (ex y st |- (f ^ <*(p . (x,y))*>)) implies |- (f ^ <*( Ex (x,p))*>)

    proof

      given y such that

       A1: |- (f ^ <*(p . (x,y))*>);

      set f1 = ((f ^ <*( All (x,( 'not' p)))*>) ^ <*( All (x,( 'not' p)))*>);

      

       A2: ( Ant f1) = (f ^ <*( All (x,( 'not' p)))*>) by Th5;

      (( len f) + 1) = (( len f) + ( len <*( All (x,( 'not' p)))*>)) by FINSEQ_1: 39;

      then (( len f) + 1) = ( len ( Ant f1)) by A2, FINSEQ_1: 22;

      then

       A3: (( len f) + 1) in ( dom ( Ant f1)) by A2, Th10;

      

       A4: ( Suc f1) = ( All (x,( 'not' p))) by Th5;

      (( Ant f1) . (( len f) + 1)) = ( All (x,( 'not' p))) by A2, FINSEQ_1: 42;

      then ( Suc f1) is_tail_of ( Ant f1) by A4, A3, Lm2;

      then |- ((f ^ <*( All (x,( 'not' p)))*>) ^ <*(( 'not' p) . (x,y))*>) by A2, A4, Th33, Th42;

      then |- ((f ^ <*( All (x,( 'not' p)))*>) ^ <*( 'not' (p . (x,y)))*>) by Th56;

      then |- ((f ^ <*(p . (x,y))*>) ^ <*( 'not' ( All (x,( 'not' p))))*>) by Th49;

      then

       A5: |- ((f ^ <*(p . (x,y))*>) ^ <*( Ex (x,p))*>) by QC_LANG2:def 5;

      1 <= ( len (f ^ <*(p . (x,y))*>)) by Th10;

      then |- (( Ant (f ^ <*(p . (x,y))*>)) ^ <*( Ex (x,p))*>) by A1, A5, Th45;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:59

    

     Th58: ( still_not-bound_in (f ^ g)) = (( still_not-bound_in f) \/ ( still_not-bound_in g))

    proof

      thus ( still_not-bound_in (f ^ g)) c= (( still_not-bound_in f) \/ ( still_not-bound_in g))

      proof

        let b be object;

        assume b in ( still_not-bound_in (f ^ g));

        then

        consider i, p such that

         A1: i in ( dom (f ^ g)) and

         A2: p = ((f ^ g) . i) & b in ( still_not-bound_in p) by Def5;

         A3:

        now

          given n be Nat such that

           A4: n in ( dom g) and

           A5: i = (( len f) + n);

          ((f ^ g) . i) = (g . n) by A4, A5, FINSEQ_1:def 7;

          then

           A6: b in ( still_not-bound_in g) by A2, A4, Def5;

          ( still_not-bound_in g) c= (( still_not-bound_in f) \/ ( still_not-bound_in g)) by XBOOLE_1: 7;

          hence thesis by A6;

        end;

        now

          assume

           A7: i in ( dom f);

          then ((f ^ g) . i) = (f . i) by FINSEQ_1:def 7;

          then

           A8: b in ( still_not-bound_in f) by A2, A7, Def5;

          ( still_not-bound_in f) c= (( still_not-bound_in f) \/ ( still_not-bound_in g)) by XBOOLE_1: 7;

          hence thesis by A8;

        end;

        hence thesis by A1, A3, FINSEQ_1: 25;

      end;

      thus (( still_not-bound_in f) \/ ( still_not-bound_in g)) c= ( still_not-bound_in (f ^ g))

      proof

        let b be object such that

         A9: b in (( still_not-bound_in f) \/ ( still_not-bound_in g));

         A10:

        now

          assume b in ( still_not-bound_in g);

          then

          consider i, p such that

           A11: i in ( dom g) & p = (g . i) and

           A12: b in ( still_not-bound_in p) by Def5;

          (( len f) + i) in ( dom (f ^ g)) & p = ((f ^ g) . (( len f) + i)) by A11, FINSEQ_1: 28, FINSEQ_1:def 7;

          hence thesis by A12, Def5;

        end;

        now

          assume b in ( still_not-bound_in f);

          then

          consider i, p such that

           A13: i in ( dom f) and

           A14: p = (f . i) and

           A15: b in ( still_not-bound_in p) by Def5;

          ( dom f) c= ( dom (f ^ g)) & p = ((f ^ g) . i) by A13, A14, FINSEQ_1: 26, FINSEQ_1:def 7;

          hence thesis by A13, A15, Def5;

        end;

        hence thesis by A9, A10, XBOOLE_0:def 3;

      end;

    end;

    theorem :: CALCUL_1:60

    

     Th59: ( still_not-bound_in <*p*>) = ( still_not-bound_in p)

    proof

       A1:

      now

        1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

        then

         A2: 1 in ( dom <*p*>) by FINSEQ_1: 38;

        

         A3: p = ( <*p*> . 1) by FINSEQ_1: 40;

        let b be object;

        assume b in ( still_not-bound_in p);

        hence b in ( still_not-bound_in <*p*>) by A2, A3, Def5;

      end;

      now

        let b be object;

        assume b in ( still_not-bound_in <*p*>);

        then

        consider i, q such that

         A4: i in ( dom <*p*>) and

         A5: q = ( <*p*> . i) & b in ( still_not-bound_in q) by Def5;

        i in ( Seg 1) by A4, FINSEQ_1: 38;

        then i = 1 by FINSEQ_1: 2, TARSKI:def 1;

        hence b in ( still_not-bound_in p) by A5, FINSEQ_1: 40;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: CALCUL_1:61

     |- ((f ^ <*(p . (x,y))*>) ^ <*q*>) & not y in ( still_not-bound_in ((f ^ <*( Ex (x,p))*>) ^ <*q*>)) implies |- ((f ^ <*( Ex (x,p))*>) ^ <*q*>)

    proof

      assume that

       A1: |- ((f ^ <*(p . (x,y))*>) ^ <*q*>) and

       A2: not y in ( still_not-bound_in ((f ^ <*( Ex (x,p))*>) ^ <*q*>));

      set f1 = ((f ^ <*( 'not' q)*>) ^ <*(( 'not' p) . (x,y))*>);

       |- ((f ^ <*( 'not' q)*>) ^ <*( 'not' (p . (x,y)))*>) by A1, Th46;

      then

       A3: |- ((f ^ <*( 'not' q)*>) ^ <*(( 'not' p) . (x,y))*>) by Th56;

      

       A4: not y in (( still_not-bound_in (f ^ <*( Ex (x,p))*>)) \/ ( still_not-bound_in <*q*>)) by A2, Th58;

      then not y in ( still_not-bound_in (f ^ <*( Ex (x,p))*>)) by XBOOLE_0:def 3;

      then

       A5: not y in (( still_not-bound_in f) \/ ( still_not-bound_in <*( Ex (x,p))*>)) by Th58;

      then not y in ( still_not-bound_in <*( Ex (x,p))*>) by XBOOLE_0:def 3;

      then not y in ( still_not-bound_in ( Ex (x,p))) by Th59;

      then not y in (( still_not-bound_in p) \ {x}) by QC_LANG3: 19;

      then not y in (( still_not-bound_in ( 'not' p)) \ {x}) by QC_LANG3: 7;

      then

       A6: not y in ( still_not-bound_in ( All (x,( 'not' p)))) by QC_LANG3: 12;

       not y in ( still_not-bound_in <*q*>) by A4, XBOOLE_0:def 3;

      then not y in ( still_not-bound_in q) by Th59;

      then not y in ( still_not-bound_in ( 'not' q)) by QC_LANG3: 7;

      then

       A7: not y in ( still_not-bound_in <*( 'not' q)*>) by Th59;

       not y in ( still_not-bound_in f) by A5, XBOOLE_0:def 3;

      then not y in (( still_not-bound_in f) \/ ( still_not-bound_in <*( 'not' q)*>)) by A7, XBOOLE_0:def 3;

      then not y in ( still_not-bound_in (f ^ <*( 'not' q)*>)) by Th58;

      then

       A8: not y in ( still_not-bound_in ( Ant f1)) by Th5;

      ( Suc f1) = (( 'not' p) . (x,y)) by Th5;

      then |- (( Ant f1) ^ <*( All (x,( 'not' p)))*>) by A3, A8, A6, Th43;

      then |- ((f ^ <*( 'not' q)*>) ^ <*( All (x,( 'not' p)))*>) by Th5;

      then |- ((f ^ <*( 'not' ( All (x,( 'not' p))))*>) ^ <*q*>) by Th48;

      hence thesis by QC_LANG2:def 5;

    end;

    theorem :: CALCUL_1:62

    

     Th61: ( still_not-bound_in f) = ( union { ( still_not-bound_in p) : ex i st i in ( dom f) & p = (f . i) })

    proof

      defpred P[ set] means ex p st $1 = ( still_not-bound_in p) & ex i st i in ( dom f) & p = (f . i);

      set X = { ( still_not-bound_in p) : ex i st i in ( dom f) & p = (f . i) };

       A1:

      now

        let b be object;

        assume b in ( union X);

        then

        consider Y be set such that

         A2: b in Y and

         A3: Y in X by TARSKI:def 4;

         P[Y] by A3;

        hence b in ( still_not-bound_in f) by A2, Def5;

      end;

      now

        let b be object;

        assume b in ( still_not-bound_in f);

        then

        consider i, p such that

         A4: i in ( dom f) & p = (f . i) and

         A5: b in ( still_not-bound_in p) by Def5;

        ( still_not-bound_in p) in X by A4;

        hence b in ( union X) by A5, TARSKI:def 4;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: CALCUL_1:63

    

     Th62: ( still_not-bound_in f) is finite

    proof

      defpred P[ object, object] means ex p st $2 = ( still_not-bound_in p) & p = (f . $1);

      consider n be Nat such that

       A1: ( dom f) = ( Seg n) by FINSEQ_1:def 2;

      set X = { ( still_not-bound_in p) : ex i st i in ( dom f) & p = (f . i) };

      consider F1 be Function such that

       A2: ( rng F1) = ( Seg n) and

       A3: ( dom F1) in omega by FINSET_1:def 1;

       A4:

      now

        let b be set;

        assume b in X;

        then ex p st b = ( still_not-bound_in p) & ex i st i in ( dom f) & p = (f . i);

        hence b is finite by CQC_SIM1: 19;

      end;

      

       A5: for a be object st a in ( dom f) holds ex b be object st P[a, b]

      proof

        let a be object;

        assume a in ( dom f);

        then (f . a) in ( rng f) by FUNCT_1: 3;

        then

        reconsider p = (f . a) as Element of ( CQC-WFF Al);

        take ( still_not-bound_in p);

        thus thesis;

      end;

      consider F2 be Function such that

       A6: ( dom F2) = ( dom f) & for b be object st b in ( dom f) holds P[b, (F2 . b)] from CLASSES1:sch 1( A5);

      set F = (F2 * F1);

       A7:

      now

        let b be object;

        assume b in X;

        then

        consider p such that

         A8: b = ( still_not-bound_in p) and

         A9: ex i st i in ( dom f) & p = (f . i);

        consider i such that

         A10: i in ( dom f) and

         A11: p = (f . i) by A9;

         P[i, (F2 . i)] by A6, A10;

        then b in ( rng F2) by A6, A8, A10, A11, FUNCT_1: 3;

        hence b in ( rng F) by A6, A1, A2, RELAT_1: 28;

      end;

      now

        let b be object;

        assume b in ( rng F);

        then b in ( rng F2) by A6, A1, A2, RELAT_1: 28;

        then

        consider a be object such that

         A12: a in ( dom F2) and

         A13: b = (F2 . a) by FUNCT_1:def 3;

        reconsider a as Element of NAT by A6, A12;

         P[a, (F2 . a)] by A6, A12;

        hence b in X by A6, A12, A13;

      end;

      then

       A14: ( rng F) = X by A7, TARSKI: 2;

      ( dom F) in omega by A6, A1, A2, A3, RELAT_1: 27;

      then X is finite by A14, FINSET_1:def 1;

      then ( union X) is finite by A4, FINSET_1: 7;

      hence thesis by Th61;

    end;

    theorem :: CALCUL_1:64

    

     Th63: ( card ( bound_QC-variables Al)) = ( card ( QC-symbols Al)) & not ( bound_QC-variables Al) is finite

    proof

       NAT c= ( QC-symbols Al) by QC_LANG1: 3;

      then

       A1: not ( QC-symbols Al) is finite;

      ( bound_QC-variables Al) = [: {4}, ( QC-symbols Al):] by QC_LANG1:def 4;

      then ( card ( bound_QC-variables Al)) = ( card [:( QC-symbols Al), {4}:]) by CARD_2: 4;

      hence thesis by A1, CARD_4: 19;

    end;

    theorem :: CALCUL_1:65

    

     Th64: ex x st not x in ( still_not-bound_in f)

    proof

      ( still_not-bound_in f) is finite by Th62;

      then ( still_not-bound_in f) <> ( bound_QC-variables Al) by Th63;

      then not (for b be object holds b in ( still_not-bound_in f) iff b in ( bound_QC-variables Al)) by TARSKI: 2;

      then

      consider b such that

       A1: not b in ( still_not-bound_in f) and

       A2: b in ( bound_QC-variables Al);

      reconsider x = b as bound_QC-variable of Al by A2;

      take x;

      thus thesis by A1;

    end;

    theorem :: CALCUL_1:66

    

     Th65: |- (f ^ <*( All (x,p))*>) implies |- (f ^ <*( All (x,( 'not' ( 'not' p))))*>)

    proof

      assume

       A1: |- (f ^ <*( All (x,p))*>);

      consider y0 such that

       A2: not y0 in ( still_not-bound_in (f ^ <*( All (x,p))*>)) by Th64;

      ( Ant (f ^ <*( All (x,p))*>)) = f & ( Suc (f ^ <*( All (x,p))*>)) = ( All (x,p)) by Th5;

      then |- (f ^ <*(p . (x,y0))*>) by A1, Th42;

      then |- (f ^ <*( 'not' ( 'not' (p . (x,y0))))*>) by Th53;

      then |- (f ^ <*( 'not' (( 'not' p) . (x,y0)))*>) by Th56;

      then

       A3: |- (f ^ <*(( 'not' ( 'not' p)) . (x,y0))*>) by Th56;

      set f1 = (f ^ <*(( 'not' ( 'not' p)) . (x,y0))*>);

      

       A4: not y0 in (( still_not-bound_in f) \/ ( still_not-bound_in <*( All (x,p))*>)) by A2, Th58;

      then not y0 in ( still_not-bound_in f) by XBOOLE_0:def 3;

      then

       A5: not y0 in ( still_not-bound_in ( Ant f1)) by Th5;

       not y0 in ( still_not-bound_in <*( All (x,p))*>) by A4, XBOOLE_0:def 3;

      then not y0 in ( still_not-bound_in ( All (x,p))) by Th59;

      then not y0 in (( still_not-bound_in p) \ {x}) by QC_LANG3: 12;

      then not y0 in (( still_not-bound_in ( 'not' p)) \ {x}) by QC_LANG3: 7;

      then not y0 in (( still_not-bound_in ( 'not' ( 'not' p))) \ {x}) by QC_LANG3: 7;

      then

       A6: not y0 in ( still_not-bound_in ( All (x,( 'not' ( 'not' p))))) by QC_LANG3: 12;

      ( Suc f1) = (( 'not' ( 'not' p)) . (x,y0)) by Th5;

      then |- (( Ant f1) ^ <*( All (x,( 'not' ( 'not' p))))*>) by A3, A5, A6, Th43;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:67

    

     Th66: |- (f ^ <*( All (x,( 'not' ( 'not' p))))*>) implies |- (f ^ <*( All (x,p))*>)

    proof

      assume

       A1: |- (f ^ <*( All (x,( 'not' ( 'not' p))))*>);

      consider y0 such that

       A2: not y0 in ( still_not-bound_in (f ^ <*( All (x,p))*>)) by Th64;

      ( Ant (f ^ <*( All (x,( 'not' ( 'not' p))))*>)) = f & ( Suc (f ^ <*( All (x,( 'not' ( 'not' p))))*>)) = ( All (x,( 'not' ( 'not' p)))) by Th5;

      then |- (f ^ <*(( 'not' ( 'not' p)) . (x,y0))*>) by A1, Th42;

      then |- (f ^ <*( 'not' (( 'not' p) . (x,y0)))*>) by Th56;

      then

       A3: |- (f ^ <*( 'not' ( 'not' (p . (x,y0))))*>) by Th56;

      set f1 = (f ^ <*(p . (x,y0))*>);

      

       A4: not y0 in (( still_not-bound_in f) \/ ( still_not-bound_in <*( All (x,p))*>)) by A2, Th58;

      then not y0 in ( still_not-bound_in f) by XBOOLE_0:def 3;

      then

       A5: not y0 in ( still_not-bound_in ( Ant f1)) by Th5;

       not y0 in ( still_not-bound_in <*( All (x,p))*>) by A4, XBOOLE_0:def 3;

      then

       A6: not y0 in ( still_not-bound_in ( All (x,p))) by Th59;

      ( Suc f1) = (p . (x,y0)) by Th5;

      then |- (( Ant f1) ^ <*( All (x,p))*>) by A3, A5, A6, Th43, Th54;

      hence thesis by Th5;

    end;

    theorem :: CALCUL_1:68

     |- (f ^ <*( All (x,p))*>) iff |- (f ^ <*( 'not' ( Ex (x,( 'not' p))))*>)

    proof

      thus |- (f ^ <*( All (x,p))*>) implies |- (f ^ <*( 'not' ( Ex (x,( 'not' p))))*>)

      proof

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

        then |- (f ^ <*( All (x,( 'not' ( 'not' p))))*>) by Th65;

        then |- (f ^ <*( 'not' ( 'not' ( All (x,( 'not' ( 'not' p))))))*>) by Th53;

        hence thesis by QC_LANG2:def 5;

      end;

      assume |- (f ^ <*( 'not' ( Ex (x,( 'not' p))))*>);

      then |- (f ^ <*( 'not' ( 'not' ( All (x,( 'not' ( 'not' p))))))*>) by QC_LANG2:def 5;

      then |- (f ^ <*( All (x,( 'not' ( 'not' p))))*>) by Th54;

      hence thesis by Th66;

    end;

    definition

      let f be FinSequence, p be set;

      :: original: is_tail_of

      redefine

      :: CALCUL_1:def16

      pred p is_tail_of f means ex i be Nat st i in ( dom f) & (f . i) = p;

      compatibility by Lm1, Lm2;

    end