substut2.miz



    begin

    reserve Al for QC-alphabet;

    reserve a,b,b1 for object,

i,j,k,n for Nat,

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

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

P for QC-pred_symbol of k, Al,

l,ll for CQC-variable_list of k, Al,

Sub,Sub1 for CQC_Substitution of Al,

S,S1,S2 for Element of ( CQC-Sub-WFF Al),

P1,P2 for Element of ( QC-pred_symbols Al);

    theorem :: SUBSTUT2:1

    

     Th1: for Sub holds ex S st (S `1 ) = ( VERUM Al) & (S `2 ) = Sub

    proof

      let Sub;

      ( VERUM Al) = <* [ 0 , 0 ]*> by QC_LANG1:def 14;

      then

      reconsider S = [( VERUM Al), Sub] as Element of ( QC-Sub-WFF Al) by SUBSTUT1:def 16;

      take S;

      set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

      X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

      then

       A1: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

      (S `1 ) = ( VERUM Al);

      then

      reconsider S as Element of ( CQC-Sub-WFF Al) by A1;

      (S `2 ) = Sub;

      hence thesis;

    end;

    

     Lm1: for k,l be Nat st P is QC-pred_symbol of k, Al & P is QC-pred_symbol of l, Al holds k = l

    proof

      let k,l be Nat;

      assume

       A1: P is QC-pred_symbol of k, Al & P is QC-pred_symbol of l, Al;

      then P in (l -ary_QC-pred_symbols Al);

      then P in { P2 : ( the_arity_of P2) = l } by QC_LANG1:def 9;

      then

       A2: ex P2 st P2 = P & ( the_arity_of P2) = l;

      P in (k -ary_QC-pred_symbols Al) by A1;

      then P in { P1 : ( the_arity_of P1) = k } by QC_LANG1:def 9;

      then ex P1 st P1 = P & ( the_arity_of P1) = k;

      hence thesis by A2;

    end;

    theorem :: SUBSTUT2:2

    

     Th2: for Sub holds ex S st (S `1 ) = (P ! ll) & (S `2 ) = Sub

    proof

      let Sub;

      P is QC-pred_symbol of ( the_arity_of P), Al by QC_LANG3: 1;

      then k = ( the_arity_of P) by Lm1;

      then [( <*P*> ^ ll), Sub] in ( QC-Sub-WFF Al) & ( len ll) = ( the_arity_of P) by CARD_1:def 7, SUBSTUT1:def 16;

      then

      reconsider S = [(P ! ll), Sub] as Element of ( QC-Sub-WFF Al) by QC_LANG1:def 12;

      set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

      X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

      then

       A1: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

      take S;

      (S `1 ) = (P ! ll);

      then

      reconsider S as Element of ( CQC-Sub-WFF Al) by A1;

      (S `2 ) = Sub;

      hence thesis;

    end;

    theorem :: SUBSTUT2:3

    for k,l be Nat st P is QC-pred_symbol of k, Al & P is QC-pred_symbol of l, Al holds k = l by Lm1;

    theorem :: SUBSTUT2:4

    

     Th4: (for Sub holds ex S st (S `1 ) = p & (S `2 ) = Sub) implies for Sub holds ex S st (S `1 ) = ( 'not' p) & (S `2 ) = Sub

    proof

      assume

       A1: for Sub holds ex S st (S `1 ) = p & (S `2 ) = Sub;

      let Sub;

      consider S such that

       A2: (S `1 ) = p & (S `2 ) = Sub by A1;

      S = [p, Sub] by A2, SUBSTUT1: 10;

      then [p, Sub] in ( QC-Sub-WFF Al);

      then [( @ p), Sub] in ( QC-Sub-WFF Al) by QC_LANG1:def 13;

      then [( <* [1, 0 ]*> ^ ( @ p)), Sub] in ( QC-Sub-WFF Al) by SUBSTUT1:def 16;

      then

      reconsider S = [( 'not' p), Sub] as Element of ( QC-Sub-WFF Al) by QC_LANG1:def 15;

      set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

      X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

      then

       A3: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

      take S;

      (S `1 ) = ( 'not' p);

      then

      reconsider S as Element of ( CQC-Sub-WFF Al) by A3;

      (S `2 ) = Sub;

      hence thesis;

    end;

    theorem :: SUBSTUT2:5

    

     Th5: (for Sub holds ex S st (S `1 ) = p & (S `2 ) = Sub) & (for Sub holds ex S st (S `1 ) = q & (S `2 ) = Sub) implies for Sub holds ex S st (S `1 ) = (p '&' q) & (S `2 ) = Sub

    proof

      assume that

       A1: for Sub holds ex S st (S `1 ) = p & (S `2 ) = Sub and

       A2: for Sub holds ex S st (S `1 ) = q & (S `2 ) = Sub;

      let Sub;

      consider S1 such that

       A3: (S1 `1 ) = p & (S1 `2 ) = Sub by A1;

      consider S2 such that

       A4: (S2 `1 ) = q & (S2 `2 ) = Sub by A2;

      S2 = [q, Sub] by A4, SUBSTUT1: 10;

      then [q, Sub] in ( QC-Sub-WFF Al);

      then

       A5: [( @ q), Sub] in ( QC-Sub-WFF Al) by QC_LANG1:def 13;

      S1 = [p, Sub] by A3, SUBSTUT1: 10;

      then [p, Sub] in ( QC-Sub-WFF Al);

      then [( @ p), Sub] in ( QC-Sub-WFF Al) by QC_LANG1:def 13;

      then [(( <* [2, 0 ]*> ^ ( @ p)) ^ ( @ q)), Sub] in ( QC-Sub-WFF Al) by A5, SUBSTUT1:def 16;

      then

      reconsider S = [(p '&' q), Sub] as Element of ( QC-Sub-WFF Al) by QC_LANG1:def 16;

      set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

      X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

      then

       A6: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

      take S;

      (S `1 ) = (p '&' q);

      then

      reconsider S as Element of ( CQC-Sub-WFF Al) by A6;

      (S `2 ) = Sub;

      hence thesis;

    end;

    definition

      let Al, p, Sub;

      :: original: [

      redefine

      func [p,Sub] -> Element of [:( QC-WFF Al), ( vSUB Al):] ;

      coherence by ZFMISC_1:def 2;

    end

    theorem :: SUBSTUT2:6

    

     Th6: ( dom ( RestrictSub (x,( All (x,p)),Sub))) misses {x}

    proof

      set finSub = ( RestrictSub (x,( All (x,p)),Sub));

      now

        set q = ( All (x,p));

        set X = { y1 : y1 in ( still_not-bound_in q) & y1 is Element of ( dom Sub) & y1 <> x & y1 <> (Sub . y1) };

        assume ( dom finSub) meets {x};

        then

        consider b be object such that

         A1: b in ( dom finSub) and

         A2: b in {x} by XBOOLE_0: 3;

        finSub = (Sub | X) by SUBSTUT1:def 6;

        then finSub = (( @ Sub) | X) by SUBSTUT1:def 2;

        then ( @ finSub) = (( @ Sub) | X) by SUBSTUT1:def 2;

        then ( dom ( @ finSub)) = (( dom ( @ Sub)) /\ X) by RELAT_1: 61;

        then

         A3: ( dom ( @ finSub)) c= X by XBOOLE_1: 17;

        b in ( dom ( @ finSub)) by A1, SUBSTUT1:def 2;

        then b in X by A3;

        then ex y st y = b & y in ( still_not-bound_in q) & y is Element of ( dom Sub) & y <> x & y <> (Sub . y);

        hence contradiction by A2, TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: SUBSTUT2:7

    

     Th7: x in ( rng ( RestrictSub (x,( All (x,p)),Sub))) implies ( S_Bound [( All (x,p)), Sub]) = ( x. ( upVar (( RestrictSub (x,( All (x,p)),Sub)),p)))

    proof

      set finSub = ( RestrictSub (x,( All (x,p)),Sub));

      set S = [( All (x,p)), Sub];

      assume

       A1: x in ( rng finSub);

      reconsider q = (S `1 ) as Element of ( CQC-WFF Al);

      

       A2: (S `2 ) = Sub;

      ( bound_in q) = x & ( the_scope_of q) = p by QC_LANG2: 7;

      hence thesis by A1, A2, SUBSTUT1:def 36;

    end;

    theorem :: SUBSTUT2:8

    

     Th8: not x in ( rng ( RestrictSub (x,( All (x,p)),Sub))) implies ( S_Bound [( All (x,p)), Sub]) = x

    proof

      set finSub = ( RestrictSub (x,( All (x,p)),Sub));

      set S = [( All (x,p)), Sub];

      assume

       A1: not x in ( rng finSub);

      reconsider q = (S `1 ) as Element of ( CQC-WFF Al);

      (S `2 ) = Sub & ( bound_in q) = x by QC_LANG2: 7;

      hence thesis by A1, SUBSTUT1:def 36;

    end;

    theorem :: SUBSTUT2:9

    

     Th9: ( ExpandSub (x,p,( RestrictSub (x,( All (x,p)),Sub)))) = (( @ ( RestrictSub (x,( All (x,p)),Sub))) +* (x | ( S_Bound [( All (x,p)), Sub])))

    proof

      set finSub = ( RestrictSub (x,( All (x,p)),Sub));

       A1:

      now

        reconsider F = { [x, ( x. ( upVar (finSub,p)))]} as Function;

        ( dom F) = {x} by RELAT_1: 9;

        then ( dom finSub) misses ( dom F) by Th6;

        then ( dom ( @ finSub)) misses ( dom F) by SUBSTUT1:def 2;

        then

         A2: (( @ finSub) \/ F) = (( @ finSub) +* F) by FUNCT_4: 31;

        assume

         A3: x in ( rng finSub);

        then ( ExpandSub (x,p,finSub)) = (finSub \/ F) by SUBSTUT1:def 13;

        then { [x, ( x. ( upVar (finSub,p)))]} = (x .--> ( x. ( upVar (finSub,p)))) & ( ExpandSub (x,p,finSub)) = (( @ finSub) +* F) by A2, FUNCT_4: 82, SUBSTUT1:def 2;

        hence thesis by A3, Th7;

      end;

      now

        reconsider F = { [x, x]} as Function;

        ( dom F) = {x} by RELAT_1: 9;

        then ( dom finSub) misses ( dom F) by Th6;

        then ( dom ( @ finSub)) misses ( dom F) by SUBSTUT1:def 2;

        then

         A4: (( @ finSub) \/ F) = (( @ finSub) +* F) by FUNCT_4: 31;

        assume

         A5: not x in ( rng finSub);

        then ( ExpandSub (x,p,finSub)) = (finSub \/ F) by SUBSTUT1:def 13;

        then { [x, x]} = (x .--> x) & ( ExpandSub (x,p,finSub)) = (( @ finSub) +* F) by A4, FUNCT_4: 82, SUBSTUT1:def 2;

        hence thesis by A5, Th8;

      end;

      hence thesis by A1;

    end;

    theorem :: SUBSTUT2:10

    

     Th10: (S `2 ) = (( @ ( RestrictSub (x,( All (x,p)),Sub))) +* (x | ( S_Bound [( All (x,p)), Sub]))) & (S `1 ) = p implies [S, x] is quantifiable & ex S1 st S1 = [( All (x,p)), Sub]

    proof

      set Sub1 = (( @ ( RestrictSub (x,( All (x,p)),Sub))) +* (x | ( S_Bound [( All (x,p)), Sub])));

      reconsider Sub as CQC_Substitution of Al;

      assume that

       A1: (S `2 ) = Sub1 and

       A2: (S `1 ) = p;

      

       A3: ( [S, x] `2 ) = x & (( [S, x] `1 ) `1 ) = p by A2;

      

       A4: ( the_scope_of ( All (x,p))) = p & ( All (x,p)) is universal by QC_LANG1:def 21, QC_LANG2: 7;

      Sub1 = ( ExpandSub (x,p,( RestrictSub (x,( All (x,p)),Sub)))) & ( bound_in ( All (x,p))) = x by Th9, QC_LANG2: 7;

      then (( All (x,p)),Sub) PQSub Sub1 by A4, SUBSTUT1:def 14;

      then

      consider a such that

       A5: a = [ [( All (x,p)), Sub], Sub1] and

       A6: (( All (x,p)),Sub) PQSub Sub1;

      a in ( QSub Al) by A5, A6, SUBSTUT1:def 15;

      then

       A7: (( QSub Al) . [( All (x,p)), Sub]) = Sub1 by A5, FUNCT_1: 1;

      

       A8: (( [S, x] `1 ) `2 ) = Sub1 by A1;

      hence [S, x] is quantifiable by A7, A3, SUBSTUT1:def 22;

      

       A9: [S, x] is quantifiable by A7, A8, A3, SUBSTUT1:def 22;

      then

      reconsider Sub as second_Q_comp of [S, x] by A7, A8, A3, SUBSTUT1:def 23;

      take S1 = ( CQCSub_All ( [S, x],Sub));

      S1 = ( Sub_All ( [S, x],Sub)) by A9, SUBLEMMA:def 5;

      hence thesis by A3, A9, SUBSTUT1:def 24;

    end;

    theorem :: SUBSTUT2:11

    

     Th11: (for Sub holds ex S st (S `1 ) = p & (S `2 ) = Sub) implies for Sub holds ex S st (S `1 ) = ( All (x,p)) & (S `2 ) = Sub

    proof

      assume

       A1: for Sub holds ex S st (S `1 ) = p & (S `2 ) = Sub;

      let Sub;

      set Sub1 = (( @ ( RestrictSub (x,( All (x,p)),Sub))) +* (x | ( S_Bound [( All (x,p)), Sub])));

      Sub1 is CQC_Substitution of Al iff Sub1 is Element of ( PFuncs (( bound_QC-variables Al),( bound_QC-variables Al))) by SUBSTUT1:def 1;

      then

      reconsider Sub1 as CQC_Substitution of Al by PARTFUN1: 45;

      ex S st (S `1 ) = p & (S `2 ) = Sub1 by A1;

      then

      consider S1 such that

       A2: S1 = [( All (x,p)), Sub] by Th10;

      take S1;

      thus thesis by A2;

    end;

    theorem :: SUBSTUT2:12

    

     Th12: for p, Sub holds ex S st (S `1 ) = p & (S `2 ) = Sub

    proof

      defpred P[ Element of ( CQC-WFF Al)] means for Sub holds ex S st (S `1 ) = $1 & (S `2 ) = Sub;

      

       A1: for p, q, x, k holds for ll be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! ll)] & ( P[p] implies P[( 'not' p)]) & ( P[p] & P[q] implies P[(p '&' q)]) & ( P[p] implies P[( All (x,p))]) by Th1, Th2, Th4, Th5, Th11;

      thus for p holds P[p] from CQC_LANG:sch 1( A1);

    end;

    definition

      let Al, p, Sub;

      :: original: [

      redefine

      func [p,Sub] -> Element of ( CQC-Sub-WFF Al) ;

      coherence

      proof

        ex S st (S `1 ) = p & (S `2 ) = Sub by Th12;

        hence thesis by SUBSTUT1: 10;

      end;

    end

    notation

      let Al, x, y;

      synonym Sbst (x,y) for x .--> y;

    end

    definition

      let Al, x, y;

      :: original: Sbst

      redefine

      func Sbst (x,y) -> CQC_Substitution of Al ;

      coherence

      proof

        

         A1: (x .--> y) is CQC_Substitution of Al iff (x .--> y) is Element of ( PFuncs (( bound_QC-variables Al),( bound_QC-variables Al))) by SUBSTUT1:def 1;

        ( dom (x .--> y)) = {x} & ( rng (x .--> y)) = {y} by FUNCOP_1: 8;

        then (x .--> y) is PartFunc of ( bound_QC-variables Al), ( bound_QC-variables Al) by RELSET_1: 4;

        hence thesis by A1, PARTFUN1: 45;

      end;

    end

    begin

    definition

      let Al, p, x, y;

      :: SUBSTUT2:def1

      func p . (x,y) -> Element of ( CQC-WFF Al) equals ( CQC_Sub [p, ( Sbst (x,y))]);

      coherence ;

    end

    scheme :: SUBSTUT2:sch1

    CQCInd1 { Al() -> QC-alphabet , P[ set] } :

for p be Element of ( CQC-WFF Al()) holds P[p]

      provided

       A1: for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) = 0 holds P[p]

       and

       A2: for k st for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) = k holds P[p] holds for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) = (k + 1) holds P[p];

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

      defpred Q[ Nat] means for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) = $1 holds P[p];

      

       A3: for k be Nat st Q[k] holds Q[(k + 1)] by A2;

      

       A4: Q[ 0 ] by A1;

      for k holds Q[k] from NAT_1:sch 2( A4, A3);

      then Q[( QuantNbr p)];

      hence thesis;

    end;

    scheme :: SUBSTUT2:sch2

    CQCInd2 { Al() -> QC-alphabet , P[ set] } :

for p be Element of ( CQC-WFF Al()) holds P[p]

      provided

       A1: for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) <= 0 holds P[p]

       and

       A2: for k st for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) <= k holds P[p] holds for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) <= (k + 1) holds P[p];

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

      defpred Q[ Nat] means for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) <= $1 holds P[p];

      

       A3: for k st Q[k] holds Q[(k + 1)] by A2;

      

       A4: Q[ 0 ] by A1;

      for k holds Q[k] from NAT_1:sch 2( A4, A3);

      then Q[( QuantNbr p)];

      hence thesis;

    end;

    theorem :: SUBSTUT2:13

    (( VERUM Al) . (x,y)) = ( VERUM Al)

    proof

      set S = [( VERUM Al), ( Sbst (x,y))];

      S is Al -Sub_VERUM by SUBSTUT1:def 19;

      hence thesis by SUBLEMMA: 3;

    end;

    theorem :: SUBSTUT2:14

    ((P ! l) . (x,y)) = (P ! ( CQC_Subst (l,( Sbst (x,y))))) & ( QuantNbr (P ! l)) = ( QuantNbr ((P ! l) . (x,y)))

    proof

      set S = [(P ! l), ( Sbst (x,y))];

      S = ( Sub_P (P,l,( Sbst (x,y)))) by SUBSTUT1: 9;

      then

       A1: ((P ! l) . (x,y)) = (P ! ( CQC_Subst (l,( Sbst (x,y))))) by SUBLEMMA: 8;

      ( QuantNbr (P ! ( CQC_Subst (l,( Sbst (x,y)))))) = 0 by CQC_SIM1: 15;

      hence thesis by A1, CQC_SIM1: 15;

    end;

    theorem :: SUBSTUT2:15

    

     Th15: ( QuantNbr (P ! l)) = ( QuantNbr ( CQC_Sub [(P ! l), Sub]))

    proof

      set S = [(P ! l), Sub];

      S = ( Sub_P (P,l,Sub)) by SUBSTUT1: 9;

      then

       A1: ( CQC_Sub [(P ! l), Sub]) = (P ! ( CQC_Subst (l,Sub))) by SUBLEMMA: 8;

      ( QuantNbr (P ! ( CQC_Subst (l,Sub)))) = 0 by CQC_SIM1: 15;

      hence thesis by A1, CQC_SIM1: 15;

    end;

    definition

      let Al;

      let S be Element of ( QC-Sub-WFF Al);

      :: original: `2

      redefine

      func S `2 -> CQC_Substitution of Al ;

      coherence

      proof

        ex p be Element of ( QC-WFF Al), Sub st S = [p, Sub] by SUBSTUT1: 8;

        hence thesis;

      end;

    end

    theorem :: SUBSTUT2:16

    

     Th16: [( 'not' p), Sub] = ( Sub_not [p, Sub])

    proof

      set S = [p, Sub];

      ( Sub_not S) = [( 'not' (S `1 )), (S `2 )] by SUBSTUT1:def 20;

      hence thesis;

    end;

    theorem :: SUBSTUT2:17

    ( 'not' (p . (x,y))) = ( 'not' (p . (x,y))) & (( QuantNbr p) = ( QuantNbr (p . (x,y))) implies ( QuantNbr ( 'not' p)) = ( QuantNbr ( 'not' (p . (x,y)))))

    proof

      set S = [( 'not' p), ( Sbst (x,y))];

      

       A1: S = ( Sub_not [p, ( Sbst (x,y))]) by Th16;

      then

       A2: (( 'not' p) . (x,y)) = ( 'not' ( CQC_Sub [p, ( Sbst (x,y))])) by SUBSTUT1: 29;

      ( QuantNbr p) = ( QuantNbr (p . (x,y))) implies ( QuantNbr ( 'not' p)) = ( QuantNbr (( 'not' p) . (x,y)))

      proof

        assume

         A3: ( QuantNbr p) = ( QuantNbr (p . (x,y)));

        ( QuantNbr (( 'not' p) . (x,y))) = ( QuantNbr (p . (x,y))) by A2, CQC_SIM1: 16;

        hence thesis by A3, CQC_SIM1: 16;

      end;

      hence thesis by A1, SUBSTUT1: 29;

    end;

    theorem :: SUBSTUT2:18

    

     Th18: (for Sub holds ( QuantNbr p) = ( QuantNbr ( CQC_Sub [p, Sub]))) implies for Sub holds ( QuantNbr ( 'not' p)) = ( QuantNbr ( CQC_Sub [( 'not' p), Sub]))

    proof

      assume

       A1: for Sub holds ( QuantNbr p) = ( QuantNbr ( CQC_Sub [p, Sub]));

      let Sub;

      set S = [( 'not' p), Sub];

      S = ( Sub_not [p, Sub]) by Th16;

      

      then ( QuantNbr ( CQC_Sub S)) = ( QuantNbr ( 'not' ( CQC_Sub [p, Sub]))) by SUBSTUT1: 29

      .= ( QuantNbr ( CQC_Sub [p, Sub])) by CQC_SIM1: 16

      .= ( QuantNbr p) by A1;

      hence thesis by CQC_SIM1: 16;

    end;

    theorem :: SUBSTUT2:19

    

     Th19: [(p '&' q), Sub] = ( CQCSub_& ( [p, Sub], [q, Sub]))

    proof

      set S1 = [p, Sub];

      set S2 = [q, Sub];

      

       A1: (S1 `1 ) = p & (S2 `1 ) = q;

      

       A2: (S1 `2 ) = Sub & (S2 `2 ) = Sub;

      then ( CQCSub_& (S1,S2)) = ( Sub_& (S1,S2)) by SUBLEMMA:def 3;

      hence thesis by A2, A1, SUBSTUT1:def 21;

    end;

    theorem :: SUBSTUT2:20

    ((p '&' q) . (x,y)) = ((p . (x,y)) '&' (q . (x,y))) & (( QuantNbr p) = ( QuantNbr (p . (x,y))) & ( QuantNbr q) = ( QuantNbr (q . (x,y))) implies ( QuantNbr (p '&' q)) = ( QuantNbr ((p '&' q) . (x,y))))

    proof

      set S = [(p '&' q), ( Sbst (x,y))];

      set S1 = [p, ( Sbst (x,y))];

      set S2 = [q, ( Sbst (x,y))];

      

       A1: (S1 `2 ) = ( Sbst (x,y)) & (S2 `2 ) = ( Sbst (x,y));

      S = ( CQCSub_& (S1,S2)) by Th19;

      then

       A2: S = ( Sub_& (S1,S2)) by A1, SUBLEMMA:def 3;

      then

       A3: ((p '&' q) . (x,y)) = (( CQC_Sub S1) '&' ( CQC_Sub S2)) by A1, SUBSTUT1: 31;

      ( QuantNbr p) = ( QuantNbr (p . (x,y))) & ( QuantNbr q) = ( QuantNbr (q . (x,y))) implies ( QuantNbr (p '&' q)) = ( QuantNbr ((p '&' q) . (x,y)))

      proof

        assume

         A4: ( QuantNbr p) = ( QuantNbr (p . (x,y))) & ( QuantNbr q) = ( QuantNbr (q . (x,y)));

        ( QuantNbr ((p '&' q) . (x,y))) = (( QuantNbr (p . (x,y))) + ( QuantNbr (q . (x,y)))) by A3, CQC_SIM1: 17;

        hence thesis by A4, CQC_SIM1: 17;

      end;

      hence thesis by A1, A2, SUBSTUT1: 31;

    end;

    theorem :: SUBSTUT2:21

    

     Th21: (for Sub holds ( QuantNbr p) = ( QuantNbr ( CQC_Sub [p, Sub]))) & (for Sub holds ( QuantNbr q) = ( QuantNbr ( CQC_Sub [q, Sub]))) implies for Sub holds ( QuantNbr (p '&' q)) = ( QuantNbr ( CQC_Sub [(p '&' q), Sub]))

    proof

      assume that

       A1: for Sub holds ( QuantNbr p) = ( QuantNbr ( CQC_Sub [p, Sub])) and

       A2: for Sub holds ( QuantNbr q) = ( QuantNbr ( CQC_Sub [q, Sub]));

      let Sub;

      set S = [(p '&' q), Sub];

      set S1 = [p, Sub];

      set S2 = [q, Sub];

      

       A3: (S1 `2 ) = Sub & (S2 `2 ) = Sub;

      S = ( CQCSub_& (S1,S2)) by Th19;

      then S = ( Sub_& (S1,S2)) by A3, SUBLEMMA:def 3;

      then ( CQC_Sub S) = (( CQC_Sub S1) '&' ( CQC_Sub S2)) by A3, SUBSTUT1: 31;

      

      then ( QuantNbr ( CQC_Sub S)) = (( QuantNbr ( CQC_Sub S1)) + ( QuantNbr ( CQC_Sub S2))) by CQC_SIM1: 17

      .= (( QuantNbr p) + ( QuantNbr ( CQC_Sub S2))) by A1

      .= (( QuantNbr p) + ( QuantNbr q)) by A2;

      hence thesis by CQC_SIM1: 17;

    end;

    definition

      let Al;

      :: SUBSTUT2:def2

      func CFQ (Al) -> Function of ( CQC-Sub-WFF Al), ( vSUB Al) equals (( QSub Al) | ( CQC-Sub-WFF Al));

      coherence

      proof

        now

          let a be object;

          assume a in ( CQC-Sub-WFF Al);

          then

          consider p be Element of ( QC-WFF Al), Sub such that

           A1: a = [p, Sub] by SUBSTUT1: 8;

           A2:

          now

            set b = {} ;

            assume not p is universal;

            then (p,Sub) PQSub b by SUBSTUT1:def 14;

            then [ [p, Sub], b] in ( QSub Al) by SUBSTUT1:def 15;

            hence a in ( dom ( QSub Al)) by A1, FUNCT_1: 1;

          end;

          now

            set b = ( ExpandSub (( bound_in p),( the_scope_of p),( RestrictSub (( bound_in p),p,Sub))));

            assume p is universal;

            then (p,Sub) PQSub b by SUBSTUT1:def 14;

            then [ [p, Sub], b] in ( QSub Al) by SUBSTUT1:def 15;

            hence a in ( dom ( QSub Al)) by A1, FUNCT_1: 1;

          end;

          hence a in ( dom ( QSub Al)) by A2;

        end;

        then ( CQC-Sub-WFF Al) c= ( dom ( QSub Al));

        then

         A3: ( dom (( QSub Al) | ( CQC-Sub-WFF Al))) = ( CQC-Sub-WFF Al) by RELAT_1: 62;

        ( rng (( QSub Al) | ( CQC-Sub-WFF Al))) c= ( vSUB Al)

        proof

          let b be object;

          assume b in ( rng (( QSub Al) | ( CQC-Sub-WFF Al)));

          then

          consider a be object such that

           A4: a in ( dom (( QSub Al) | ( CQC-Sub-WFF Al))) & ((( QSub Al) | ( CQC-Sub-WFF Al)) . a) = b by FUNCT_1:def 3;

          

           A5: (( QSub Al) | ( CQC-Sub-WFF Al)) c= ( QSub Al) by RELAT_1: 59;

           [a, b] in (( QSub Al) | ( CQC-Sub-WFF Al)) by A4, FUNCT_1: 1;

          then

          consider p be Element of ( QC-WFF Al), Sub, b1 such that

           A6: [a, b] = [ [p, Sub], b1] and

           A7: (p,Sub) PQSub b1 by A5, SUBSTUT1:def 15;

           A8:

          now

            

             A9: b1 is CQC_Substitution of Al iff b1 is Element of ( PFuncs (( bound_QC-variables Al),( bound_QC-variables Al))) by SUBSTUT1:def 1;

            assume not p is universal;

            then b1 = {} by A7, SUBSTUT1:def 14;

            then b1 is PartFunc of ( bound_QC-variables Al), ( bound_QC-variables Al) by RELSET_1: 12;

            hence b is CQC_Substitution of Al by A9, A6, PARTFUN1: 45, XTUPLE_0: 1;

          end;

          now

            assume p is universal;

            then b1 = ( ExpandSub (( bound_in p),( the_scope_of p),( RestrictSub (( bound_in p),p,Sub)))) by A7, SUBSTUT1:def 14;

            hence b is CQC_Substitution of Al by A6, XTUPLE_0: 1;

          end;

          hence thesis by A8;

        end;

        hence thesis by A3, FUNCT_2: 2;

      end;

    end

    definition

      let Al, p, x, Sub;

      :: SUBSTUT2:def3

      func QScope (p,x,Sub) -> CQC-WFF-like Element of [:( QC-Sub-WFF Al), ( bound_QC-variables Al):] equals [ [p, (( CFQ Al) . [( All (x,p)), Sub])], x];

      coherence ;

    end

    definition

      let Al, p, x, Sub;

      :: SUBSTUT2:def4

      func Qsc (p,x,Sub) -> second_Q_comp of ( QScope (p,x,Sub)) equals Sub;

      coherence

      proof

        

         A1: ((( QScope (p,x,Sub)) `1 ) `2 ) = (( QSub Al) . [( All (x,p)), Sub]) by FUNCT_1: 49;

        

         A2: (( QScope (p,x,Sub)) `2 ) = x & ((( QScope (p,x,Sub)) `1 ) `1 ) = p;

        then ( QScope (p,x,Sub)) is quantifiable by A1, SUBSTUT1:def 22;

        hence thesis by A2, A1, SUBSTUT1:def 23;

      end;

    end

    theorem :: SUBSTUT2:22

    

     Th22: [( All (x,p)), Sub] = ( CQCSub_All (( QScope (p,x,Sub)),( Qsc (p,x,Sub)))) & ( QScope (p,x,Sub)) is quantifiable

    proof

      set S = [p, (( CFQ Al) . [( All (x,p)), Sub])];

      set B = [ [p, (( CFQ Al) . [( All (x,p)), Sub])], x];

      

       A1: (B `2 ) = x & ((B `1 ) `1 ) = p;

       [( All (x,p)), Sub] in ( CQC-Sub-WFF Al);

      then

       A2: [( All (x,p)), Sub] in ( dom ( CFQ Al)) by FUNCT_2:def 1;

      ((B `1 ) `2 ) = (( QSub Al) . [( All ((B `2 ),((B `1 ) `1 ))), Sub]) by A2, FUNCT_1: 47;

      then

       A3: B is quantifiable by SUBSTUT1:def 22;

      then ( CQCSub_All (( QScope (p,x,Sub)),( Qsc (p,x,Sub)))) = ( Sub_All (( QScope (p,x,Sub)),( Qsc (p,x,Sub)))) by SUBLEMMA:def 5;

      hence thesis by A1, A3, SUBSTUT1:def 24;

    end;

    theorem :: SUBSTUT2:23

    

     Th23: (for Sub holds ( QuantNbr p) = ( QuantNbr ( CQC_Sub [p, Sub]))) implies for Sub holds ( QuantNbr ( All (x,p))) = ( QuantNbr ( CQC_Sub [( All (x,p)), Sub]))

    proof

      assume

       A1: for Sub holds ( QuantNbr p) = ( QuantNbr ( CQC_Sub [p, Sub]));

      let Sub;

      set S1 = [( All (x,p)), Sub];

      set S = [p, (( CFQ Al) . [( All (x,p)), Sub])];

      set y = ( S_Bound ( @ ( CQCSub_All (( QScope (p,x,Sub)),( Qsc (p,x,Sub))))));

      

       A2: ( QScope (p,x,Sub)) is quantifiable by Th22;

      

       A3: ( Sub_All (( QScope (p,x,Sub)),( Qsc (p,x,Sub)))) = ( CQCSub_All (( QScope (p,x,Sub)),( Qsc (p,x,Sub)))) by Th22, SUBLEMMA:def 5

      .= S1 by Th22;

      then

       A4: S1 is Sub_universal by A2, SUBSTUT1:def 28;

      then

       A5: ( CQC_Sub S1) = ( CQCQuant (S1,( CQC_Sub ( CQCSub_the_scope_of S1)))) by SUBLEMMA: 28;

      ( CQCSub_the_scope_of S1) = ( Sub_the_scope_of ( Sub_All (( QScope (p,x,Sub)),( Qsc (p,x,Sub))))) by A3, A4, SUBLEMMA:def 6

      .= ( [S, x] `1 ) by A2, SUBSTUT1: 21

      .= S;

      then ( CQC_Sub S1) = ( CQCQuant (( CQCSub_All (( QScope (p,x,Sub)),( Qsc (p,x,Sub)))),( CQC_Sub S))) by A5, Th22;

      

      then ( QuantNbr ( CQC_Sub S1)) = ( QuantNbr ( All (y,( CQC_Sub S)))) by Th22, SUBLEMMA: 31

      .= (( QuantNbr ( CQC_Sub S)) + 1) by CQC_SIM1: 18

      .= (( QuantNbr p) + 1) by A1;

      hence thesis by CQC_SIM1: 18;

    end;

    theorem :: SUBSTUT2:24

    

     Th24: ( QuantNbr ( VERUM Al)) = ( QuantNbr ( CQC_Sub [( VERUM Al), Sub]))

    proof

       [( VERUM Al), Sub] is Al -Sub_VERUM by SUBSTUT1:def 19;

      hence thesis by SUBLEMMA: 3;

    end;

    theorem :: SUBSTUT2:25

    for p, Sub holds ( QuantNbr p) = ( QuantNbr ( CQC_Sub [p, Sub]))

    proof

      defpred P[ Element of ( CQC-WFF Al)] means for Sub holds ( QuantNbr $1) = ( QuantNbr ( CQC_Sub [$1, Sub]));

      

       A1: for r, s, x, k holds for l be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! l)] & ( P[r] implies P[( 'not' r)]) & ( P[r] & P[s] implies P[(r '&' s)]) & ( P[r] implies P[( All (x,r))]) by Th15, Th18, Th21, Th23, Th24;

      thus for r holds P[r] from CQC_LANG:sch 1( A1);

    end;

    theorem :: SUBSTUT2:26

    p is atomic implies ex k, P, ll st p = (P ! ll)

    proof

      assume p is atomic;

      then

      consider k be Nat, P be QC-pred_symbol of k, Al, l be QC-variable_list of k, Al such that

       A1: p = (P ! l) by QC_LANG1:def 18;

      

       A2: { (l . j) : 1 <= j & j <= ( len l) & (l . j) in ( fixed_QC-variables Al) } = {} by A1, CQC_LANG: 7;

      { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( free_QC-variables Al) } = {} by A1, CQC_LANG: 7;

      then

      reconsider l as CQC-variable_list of k, Al by A2, CQC_LANG: 5;

      take k, P, l;

      thus thesis by A1;

    end;

    scheme :: SUBSTUT2:sch3

    CQCInd3 { Al() -> QC-alphabet , P[ set] } :

for p be Element of ( CQC-WFF Al()) st ( QuantNbr p) = 0 holds P[p]

      provided

       A1: for r,s be Element of ( CQC-WFF Al()) holds for x be bound_QC-variable of Al() holds for k holds for l be CQC-variable_list of k, Al() holds for P be QC-pred_symbol of k, Al() holds P[( VERUM Al())] & P[(P ! l)] & (P[r] implies P[( 'not' r)]) & (P[r] & P[s] implies P[(r '&' s)]);

      defpred Prop[ Element of ( CQC-WFF Al())] means ( QuantNbr $1) = 0 implies P[$1];

      

       A2: for x be bound_QC-variable of Al(), p be Element of ( CQC-WFF Al()) st Prop[p] holds Prop[( All (x,p))]

      proof

        let x be bound_QC-variable of Al(), p be Element of ( CQC-WFF Al()) such that Prop[p];

        assume ( QuantNbr ( All (x,p))) = 0 ;

        then (( QuantNbr p) + 1) = 0 by CQC_SIM1: 18;

        hence thesis;

      end;

      for p,q be Element of ( CQC-WFF Al()) st Prop[p] & Prop[q] holds Prop[(p '&' q)]

      proof

        let p,q be Element of ( CQC-WFF Al()) such that

         A3: Prop[p] & Prop[q];

        assume ( QuantNbr (p '&' q)) = 0 ;

        then (( QuantNbr p) + ( QuantNbr q)) = 0 by CQC_SIM1: 17;

        hence thesis by A1, A3;

      end;

      then

       A4: for r,s be Element of ( CQC-WFF Al()) holds for x be bound_QC-variable of Al() holds for k holds for l be CQC-variable_list of k, Al() holds for P be QC-pred_symbol of k, Al() holds Prop[( VERUM Al())] & Prop[(P ! l)] & ( Prop[r] implies Prop[( 'not' r)]) & ( Prop[r] & Prop[s] implies Prop[(r '&' s)]) & ( Prop[r] implies Prop[( All (x,r))]) by A1, A2, CQC_SIM1: 16;

      for p be Element of ( CQC-WFF Al()) holds Prop[p] from CQC_LANG:sch 1( A4);

      hence thesis;

    end;

    begin

    reserve F1,F2,F3 for QC-formula of Al,

L for FinSequence;

    definition

      let Al;

      let G,H be QC-formula of Al;

      assume

       A1: G is_subformula_of H;

      :: SUBSTUT2:def5

      mode PATH of G,H -> FinSequence means

      : Def5: 1 <= ( len it ) & (it . 1) = G & (it . ( len it )) = H & for k st 1 <= k & k < ( len it ) holds ex G1,H1 be Element of ( QC-WFF Al) st (it . k) = G1 & (it . (k + 1)) = H1 & G1 is_immediate_constituent_of H1;

      existence

      proof

        ex n, L st 1 <= n & ( len L) = n & (L . 1) = G & (L . n) = H & for k st 1 <= k & k < n holds ex G1,H1 be Element of ( QC-WFF Al) st (L . k) = G1 & (L . (k + 1)) = H1 & G1 is_immediate_constituent_of H1 by A1, QC_LANG2:def 20;

        then

        consider L such that

         A2: ex n st 1 <= n & ( len L) = n & (L . 1) = G & (L . n) = H & for k st 1 <= k & k < n holds ex G1,H1 be Element of ( QC-WFF Al) st (L . k) = G1 & (L . (k + 1)) = H1 & G1 is_immediate_constituent_of H1;

        take L;

        thus thesis by A2;

      end;

    end

    theorem :: SUBSTUT2:27

    for L be PATH of F1, F2 st F1 is_subformula_of F2 & 1 <= i & i <= ( len L) holds ex F3 st F3 = (L . i) & F3 is_subformula_of F2

    proof

      let L be PATH of F1, F2;

      set n = ( len L);

      assume that

       A1: F1 is_subformula_of F2 and

       A2: 1 <= i and

       A3: i <= n;

      (n + 1) <= (n + i) by A2, XREAL_1: 6;

      then ((n + 1) + ( - 1)) <= ((n + i) + ( - 1)) by XREAL_1: 6;

      then

       A4: (n + ( - i)) <= (((n - 1) + i) + ( - i)) by XREAL_1: 6;

      (i + ( - i)) <= (n + ( - i)) by A3, XREAL_1: 6;

      then

      reconsider l = (n - i) as Element of NAT by INT_1: 3;

      defpred P[ Nat] means $1 <= (n - 1) implies ex F3 st F3 = (L . (n - $1)) & F3 is_subformula_of F2;

      

       A5: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A6: P[k];

        assume

         A7: (k + 1) <= (n - 1);

        then ((k + 1) + 1) <= ((n - 1) + 1) by XREAL_1: 6;

        then

         A8: ((2 + k) + ( - k)) <= (n + ( - k)) by XREAL_1: 6;

        then

        reconsider j = (n - k) as Element of NAT by INT_1: 3;

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

        then (n + ( - k)) <= ((n + k) + ( - k)) by XREAL_1: 6;

        then

         A9: (j - 1) < n by XREAL_1: 146, XXREAL_0: 2;

        

         A10: ((1 + 1) + ( - 1)) <= (j + ( - 1)) by A8, XREAL_1: 6;

        then

        reconsider j1 = (j - 1) as Element of NAT by INT_1: 3;

        (j1 + 1) = j;

        then

         A11: ex G1,H1 be Element of ( QC-WFF Al) st (L . j1) = G1 & (L . j) = H1 & G1 is_immediate_constituent_of H1 by A1, A10, A9, Def5;

        then

        reconsider F3 = (L . j1) as QC-formula of Al;

        take F3;

        k < (k + 1) by NAT_1: 13;

        then F3 is_proper_subformula_of F2 by A6, A7, A11, QC_LANG2: 63, XXREAL_0: 2;

        hence thesis by QC_LANG2:def 21;

      end;

      (L . n) = F2 by A1, Def5;

      then

       A12: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A12, A5);

      then ex F3 st F3 = (L . (n - l)) & F3 is_subformula_of F2 by A4;

      hence thesis;

    end;

    theorem :: SUBSTUT2:28

    

     Th28: for L be PATH of F1, p st F1 is_subformula_of p & 1 <= i & i <= ( len L) holds (L . i) is Element of ( CQC-WFF Al)

    proof

      let L be PATH of F1, p;

      set n = ( len L);

      assume that

       A1: F1 is_subformula_of p and

       A2: 1 <= i and

       A3: i <= n;

      (n + 1) <= (n + i) by A2, XREAL_1: 6;

      then ((n + 1) + ( - 1)) <= ((n + i) + ( - 1)) by XREAL_1: 6;

      then

       A4: (n + ( - i)) <= (((n - 1) + i) + ( - i)) by XREAL_1: 6;

      (i + ( - i)) <= (n + ( - i)) by A3, XREAL_1: 6;

      then

      reconsider l = (n - i) as Element of NAT by INT_1: 3;

      defpred P[ Nat] means $1 <= (n - 1) implies (L . (n - $1)) is Element of ( CQC-WFF Al);

      

       A5: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A6: P[k];

        assume

         A7: (k + 1) <= (n - 1);

        then ((k + 1) + 1) <= ((n - 1) + 1) by XREAL_1: 6;

        then

         A8: ((2 + k) + ( - k)) <= (n + ( - k)) by XREAL_1: 6;

        then

        reconsider j = (n - k) as Element of NAT by INT_1: 3;

        k < (k + 1) by NAT_1: 13;

        then

        reconsider q = (L . j) as Element of ( CQC-WFF Al) by A6, A7, XXREAL_0: 2;

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

        then (n + ( - k)) <= ((n + k) + ( - k)) by XREAL_1: 6;

        then

         A9: (j - 1) < n by XREAL_1: 146, XXREAL_0: 2;

        

         A10: ((1 + 1) + ( - 1)) <= (j + ( - 1)) by A8, XREAL_1: 6;

        then

        reconsider j1 = (j - 1) as Element of NAT by INT_1: 3;

        (j1 + 1) = j;

        then

        consider G1,H1 be Element of ( QC-WFF Al) such that

         A11: (L . j1) = G1 and

         A12: q = H1 & G1 is_immediate_constituent_of H1 by A1, A10, A9, Def5;

        

         A13: (ex F be Element of ( QC-WFF Al) st q = (G1 '&' F)) implies thesis by A11, CQC_LANG: 9;

        

         A14: (ex x st q = ( All (x,G1))) implies thesis by A11, CQC_LANG: 13;

        

         A15: (ex F be Element of ( QC-WFF Al) st q = (F '&' G1)) implies thesis by A11, CQC_LANG: 9;

        q = ( 'not' G1) implies thesis by A11, CQC_LANG: 8;

        hence thesis by A12, A13, A15, A14, QC_LANG2:def 19;

      end;

      

       A16: P[ 0 ] by A1, Def5;

      for k holds P[k] from NAT_1:sch 2( A16, A5);

      then (L . (n - l)) is Element of ( CQC-WFF Al) by A4;

      hence thesis;

    end;

    theorem :: SUBSTUT2:29

    

     Th29: for L be PATH of q, p st ( QuantNbr p) <= n & q is_subformula_of p & 1 <= i & i <= ( len L) holds ex r st r = (L . i) & ( QuantNbr r) <= n

    proof

      let L be PATH of q, p;

      set m = ( len L);

      assume that

       A1: ( QuantNbr p) <= n and

       A2: q is_subformula_of p and

       A3: 1 <= i and

       A4: i <= m;

      (i + ( - i)) <= (m + ( - i)) by A4, XREAL_1: 6;

      then

      reconsider l = (m - i) as Element of NAT by INT_1: 3;

      (m + 1) <= (m + i) by A3, XREAL_1: 6;

      then ((m + 1) + ( - 1)) <= ((m + i) + ( - 1)) by XREAL_1: 6;

      then

       A5: (m + ( - i)) <= (((m - 1) + i) + ( - i)) by XREAL_1: 6;

      defpred P[ Nat] means $1 <= (m - 1) implies ex r st r = (L . (m - $1)) & ( QuantNbr r) <= n;

      

       A6: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A7: P[k];

        assume

         A8: (k + 1) <= (m - 1);

        then ((k + 1) + 1) <= ((m - 1) + 1) by XREAL_1: 6;

        then

         A9: ((2 + k) + ( - k)) <= (m + ( - k)) by XREAL_1: 6;

        then

        reconsider j = (m - k) as Element of NAT by INT_1: 3;

        

         A10: ((1 + 1) + ( - 1)) <= (j + ( - 1)) by A9, XREAL_1: 6;

        then

        reconsider j1 = (j - 1) as Element of NAT by INT_1: 3;

        m <= (m + k) by NAT_1: 11;

        then (m + ( - k)) <= ((m + k) + ( - k)) by XREAL_1: 6;

        then

         A11: (j - 1) < m by XREAL_1: 146, XXREAL_0: 2;

        (j1 + 1) = j;

        then

        consider G1,H1 be Element of ( QC-WFF Al) such that

         A12: (L . j1) = G1 and

         A13: (L . j) = H1 & G1 is_immediate_constituent_of H1 by A2, A10, A11, Def5;

        reconsider r = G1 as Element of ( CQC-WFF Al) by A2, A10, A11, A12, Th28;

        k < (k + 1) by NAT_1: 13;

        then

        consider q such that

         A14: q = (L . j) and

         A15: ( QuantNbr q) <= n by A7, A8, XXREAL_0: 2;

         A16:

        now

          given x such that

           A17: q = ( All (x,G1));

          take r;

          (( QuantNbr r) + 1) <= n by A15, A17, CQC_SIM1: 18;

          then ( QuantNbr r) <= n by NAT_1: 13;

          hence thesis by A12;

        end;

         A18:

        now

          given F be Element of ( QC-WFF Al) such that

           A19: q = (F '&' G1);

          reconsider F as Element of ( CQC-WFF Al) by A19, CQC_LANG: 9;

          take r;

          n <= (n + ( QuantNbr F)) by NAT_1: 11;

          then

           A20: (n + ( - ( QuantNbr F))) <= ((n + ( QuantNbr F)) + ( - ( QuantNbr F))) by XREAL_1: 6;

          (( QuantNbr r) + ( QuantNbr F)) <= n by A15, A19, CQC_SIM1: 17;

          then ((( QuantNbr r) + ( QuantNbr F)) + ( - ( QuantNbr F))) <= (n + ( - ( QuantNbr F))) by XREAL_1: 6;

          hence thesis by A12, A20, XXREAL_0: 2;

        end;

         A21:

        now

          given F be Element of ( QC-WFF Al) such that

           A22: q = (G1 '&' F);

          reconsider F as Element of ( CQC-WFF Al) by A22, CQC_LANG: 9;

          take r;

          n <= (n + ( QuantNbr F)) by NAT_1: 11;

          then

           A23: (n + ( - ( QuantNbr F))) <= ((n + ( QuantNbr F)) + ( - ( QuantNbr F))) by XREAL_1: 6;

          (( QuantNbr r) + ( QuantNbr F)) <= n by A15, A22, CQC_SIM1: 17;

          then ((( QuantNbr r) + ( QuantNbr F)) + ( - ( QuantNbr F))) <= (n + ( - ( QuantNbr F))) by XREAL_1: 6;

          hence thesis by A12, A23, XXREAL_0: 2;

        end;

        now

          assume

           A24: q = ( 'not' G1);

          take r;

          ( QuantNbr r) <= n by A15, A24, CQC_SIM1: 16;

          hence thesis by A12;

        end;

        hence thesis by A14, A13, A21, A18, A16, QC_LANG2:def 19;

      end;

      (L . m) = p by A2, Def5;

      then

       A25: P[ 0 ] by A1;

      for k holds P[k] from NAT_1:sch 2( A25, A6);

      then ex r st r = (L . (m - l)) & ( QuantNbr r) <= n by A5;

      hence thesis;

    end;

    theorem :: SUBSTUT2:30

    ( QuantNbr p) = n & q is_subformula_of p implies ( QuantNbr q) <= n

    proof

      set L = the PATH of q, p;

      set m = ( len L);

      assume that

       A1: ( QuantNbr p) = n and

       A2: q is_subformula_of p;

      1 <= m by A2, Def5;

      then ex r st r = (L . 1) & ( QuantNbr r) <= n by A1, A2, Th29;

      hence thesis by A2, Def5;

    end;

    theorem :: SUBSTUT2:31

    for n, p st (for q st q is_subformula_of p holds ( QuantNbr q) = n) holds n = 0

    proof

      let n, p such that

       A1: for q st q is_subformula_of p holds ( QuantNbr q) = n;

      defpred P[ Element of ( CQC-WFF Al)] means $1 is_subformula_of p implies ( QuantNbr $1) = 0 ;

      

       A2: for x, r st P[r] holds P[( All (x,r))]

      proof

        let x, r such that P[r];

        now

          assume

           A3: ( All (x,r)) is_subformula_of p;

          r is_immediate_constituent_of ( All (x,r)) by QC_LANG2: 46;

          then r is_proper_subformula_of p by A3, QC_LANG2: 63;

          then r is_subformula_of p by QC_LANG2:def 21;

          then

           A4: ( QuantNbr r) = n by A1;

          ( QuantNbr ( All (x,r))) = n by A1, A3;

          then (n + ( - n)) = ((1 + n) + ( - n)) by A4, CQC_SIM1: 18;

          hence contradiction;

        end;

        hence thesis;

      end;

      

       A5: for r, s st P[r] & P[s] holds P[(r '&' s)]

      proof

        let r, s such that

         A6: P[r] & P[s];

        assume

         A7: (r '&' s) is_subformula_of p;

        s is_immediate_constituent_of (r '&' s) by QC_LANG2: 45;

        then

         A8: s is_proper_subformula_of p by A7, QC_LANG2: 63;

        r is_immediate_constituent_of (r '&' s) by QC_LANG2: 45;

        then r is_proper_subformula_of p by A7, QC_LANG2: 63;

        then ( QuantNbr (r '&' s)) = ( 0 + 0 ) by A6, A8, CQC_SIM1: 17, QC_LANG2:def 21;

        hence thesis;

      end;

      for r st P[r] holds P[( 'not' r)]

      proof

        let r such that

         A9: P[r];

        

         A10: r is_immediate_constituent_of ( 'not' r) by QC_LANG2: 43;

        assume ( 'not' r) is_subformula_of p;

        then r is_proper_subformula_of p by A10, QC_LANG2: 63;

        hence thesis by A9, CQC_SIM1: 16, QC_LANG2:def 21;

      end;

      then

       A11: for r, s, x, k holds for l be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! l)] & ( P[r] implies P[( 'not' r)]) & ( P[r] & P[s] implies P[(r '&' s)]) & ( P[r] implies P[( All (x,r))]) by A5, A2, CQC_SIM1: 14, CQC_SIM1: 15;

      

       A12: for r holds P[r] from CQC_LANG:sch 1( A11);

      ( QuantNbr p) = n by A1;

      hence thesis by A12;

    end;

    theorem :: SUBSTUT2:32

    for p st (for q st q is_subformula_of p holds for x, r holds q <> ( All (x,r))) holds ( QuantNbr p) = 0

    proof

      let p such that

       A1: for q st q is_subformula_of p holds for x, r holds q <> ( All (x,r));

      defpred P[ Element of ( CQC-WFF Al)] means $1 is_subformula_of p implies ( QuantNbr $1) = 0 ;

      

       A2: for r, s st P[r] & P[s] holds P[(r '&' s)]

      proof

        let r, s such that

         A3: P[r] & P[s];

        assume

         A4: (r '&' s) is_subformula_of p;

        s is_immediate_constituent_of (r '&' s) by QC_LANG2: 45;

        then

         A5: s is_proper_subformula_of p by A4, QC_LANG2: 63;

        r is_immediate_constituent_of (r '&' s) by QC_LANG2: 45;

        then r is_proper_subformula_of p by A4, QC_LANG2: 63;

        then ( QuantNbr (r '&' s)) = ( 0 + 0 ) by A3, A5, CQC_SIM1: 17, QC_LANG2:def 21;

        hence thesis;

      end;

      for r st P[r] holds P[( 'not' r)]

      proof

        let r such that

         A6: P[r];

        

         A7: r is_immediate_constituent_of ( 'not' r) by QC_LANG2: 43;

        assume ( 'not' r) is_subformula_of p;

        then r is_proper_subformula_of p by A7, QC_LANG2: 63;

        hence thesis by A6, CQC_SIM1: 16, QC_LANG2:def 21;

      end;

      then

       A8: for r, s, x, k holds for l be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! l)] & ( P[r] implies P[( 'not' r)]) & ( P[r] & P[s] implies P[(r '&' s)]) & ( P[r] implies P[( All (x,r))]) by A1, A2, CQC_SIM1: 14, CQC_SIM1: 15;

      for r holds P[r] from CQC_LANG:sch 1( A8);

      hence thesis;

    end;

    theorem :: SUBSTUT2:33

    

     Th33: for p st for q st q is_subformula_of p holds ( QuantNbr q) <> 1 holds ( QuantNbr p) = 0

    proof

      let p such that

       A1: for q st q is_subformula_of p holds ( QuantNbr q) <> 1;

      defpred P[ Element of ( CQC-WFF Al)] means $1 is_subformula_of p implies ( QuantNbr $1) = 0 ;

      

       A2: for x, r st P[r] holds P[( All (x,r))]

      proof

        let x, r such that

         A3: P[r];

        now

          assume

           A4: ( All (x,r)) is_subformula_of p;

          r is_immediate_constituent_of ( All (x,r)) by QC_LANG2: 46;

          then r is_proper_subformula_of p by A4, QC_LANG2: 63;

          then ( QuantNbr ( All (x,r))) = ( 0 + 1) by A3, CQC_SIM1: 18, QC_LANG2:def 21;

          hence contradiction by A1, A4;

        end;

        hence thesis;

      end;

      

       A5: for r, s st P[r] & P[s] holds P[(r '&' s)]

      proof

        let r, s such that

         A6: P[r] & P[s];

        assume

         A7: (r '&' s) is_subformula_of p;

        s is_immediate_constituent_of (r '&' s) by QC_LANG2: 45;

        then

         A8: s is_proper_subformula_of p by A7, QC_LANG2: 63;

        r is_immediate_constituent_of (r '&' s) by QC_LANG2: 45;

        then r is_proper_subformula_of p by A7, QC_LANG2: 63;

        then ( QuantNbr (r '&' s)) = ( 0 + 0 ) by A6, A8, CQC_SIM1: 17, QC_LANG2:def 21;

        hence thesis;

      end;

      for r st P[r] holds P[( 'not' r)]

      proof

        let r such that

         A9: P[r];

        

         A10: r is_immediate_constituent_of ( 'not' r) by QC_LANG2: 43;

        assume ( 'not' r) is_subformula_of p;

        then r is_proper_subformula_of p by A10, QC_LANG2: 63;

        hence thesis by A9, CQC_SIM1: 16, QC_LANG2:def 21;

      end;

      then

       A11: for r, s, x, k holds for l be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! l)] & ( P[r] implies P[( 'not' r)]) & ( P[r] & P[s] implies P[(r '&' s)]) & ( P[r] implies P[( All (x,r))]) by A5, A2, CQC_SIM1: 14, CQC_SIM1: 15;

      for r holds P[r] from CQC_LANG:sch 1( A11);

      hence thesis;

    end;

    theorem :: SUBSTUT2:34

    1 <= ( QuantNbr p) implies ex q st q is_subformula_of p & ( QuantNbr q) = 1 by Th33;