qc_trans.miz



    begin

    reserve Al for QC-alphabet;

    reserve PHI for Consistent Subset of ( CQC-WFF Al),

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

A for non empty set,

J for interpretation of Al, A,

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

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

l for CQC-variable_list of k, Al,

P for QC-pred_symbol of k, Al,

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

b for QC-symbol of Al,

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

    definition

      let Al;

      let Al2 be QC-alphabet;

      :: QC_TRANS:def1

      attr Al2 is Al -expanding means

      : Def1: Al c= Al2;

    end

    registration

      let Al;

      cluster Al -expanding for QC-alphabet;

      existence by Def1;

    end

    registration

      let Al1,Al2 be countable QC-alphabet;

      cluster countableAl1 -expandingAl2 -expanding for QC-alphabet;

      existence

      proof

        set Al3 = (Al1 \/ Al2);

        Al1 = [: NAT , ( QC-symbols Al1):] & Al2 = [: NAT , ( QC-symbols Al2):] by QC_LANG1: 5;

        then

         A1: Al3 = [: NAT , (( QC-symbols Al1) \/ ( QC-symbols Al2)):] by ZFMISC_1: 97;

         NAT c= (( QC-symbols Al1) \/ ( QC-symbols Al2)) by XBOOLE_1: 10, QC_LANG1: 3;

        then

        reconsider Al3 as QC-alphabet by A1, QC_LANG1:def 1;

        take Al3;

        thus thesis by CARD_2: 85, XBOOLE_1: 7;

      end;

    end

    definition

      let Al,Al2 be QC-alphabet;

      let P be Subset of ( CQC-WFF Al);

      :: QC_TRANS:def2

      attr P is Al2 -Consistent means for S be Subset of ( CQC-WFF Al2) st P = S holds S is Consistent;

    end

    registration

      let Al;

      cluster non empty Consistent for Subset of ( CQC-WFF Al);

      existence

      proof

         {( VERUM Al)} is Consistent by HENMODEL: 13;

        hence thesis;

      end;

    end

    registration

      let Al;

      cluster Consistent -> Al -Consistent for Subset of ( CQC-WFF Al);

      coherence ;

      cluster Al -Consistent -> Consistent for Subset of ( CQC-WFF Al);

      coherence ;

    end

    reserve Al2 for Al -expanding QC-alphabet,

J2 for interpretation of Al2, A,

Jp for interpretation of Al, A,

v2 for Element of ( Valuations_in (Al2,A)),

vp for Element of ( Valuations_in (Al,A));

    theorem :: QC_TRANS:1

    

     Th1: ( the_arity_of P) = ( len l)

    proof

      

      thus ( len l) = k by CARD_1:def 7

      .= ( the_arity_of P) by QC_LANG1: 11;

    end;

    theorem :: QC_TRANS:2

    

     Th2: ( QC-symbols Al) c= ( QC-symbols Al2)

    proof

      Al c= Al2 & Al = [: NAT , ( QC-symbols Al):] & Al2 = [: NAT , ( QC-symbols Al2):] by Def1, QC_LANG1: 5;

      hence ( QC-symbols Al) c= ( QC-symbols Al2) by ZFMISC_1: 115;

    end;

    theorem :: QC_TRANS:3

    

     Th3: ( QC-pred_symbols Al) c= ( QC-pred_symbols Al2)

    proof

      for Q be object st Q in ( QC-pred_symbols Al) holds Q in ( QC-pred_symbols Al2)

      proof

        let Q be object such that

         A1: Q in ( QC-pred_symbols Al);

        set preds = { [k, b] : 7 <= k };

        set preds2 = { [k, b2] where b2 be QC-symbol of Al2 : 7 <= k };

        consider k, b such that

         A2: Q = [k, b] & 7 <= k by A1;

        b in ( QC-symbols Al2) by Th2, TARSKI:def 3;

        hence Q in ( QC-pred_symbols Al2) by A2;

      end;

      hence thesis;

    end;

    theorem :: QC_TRANS:4

    

     Th4: ( bound_QC-variables Al) c= ( bound_QC-variables Al2)

    proof

      

       A1: ( QC-symbols Al) c= ( QC-symbols Al2) by Th2;

      thus thesis by A1, ZFMISC_1: 96;

    end;

    theorem :: QC_TRANS:5

    

     Th5: for k, l holds l is CQC-variable_list of k, Al2

    proof

      let k, l;

      ( rng l) c= ( bound_QC-variables Al) & ( bound_QC-variables Al) c= ( bound_QC-variables Al2) by Th4;

      then ( rng l) c= ( bound_QC-variables Al2);

      hence thesis by FINSEQ_1:def 4, XBOOLE_1: 1;

    end;

    theorem :: QC_TRANS:6

    

     Th6: P is QC-pred_symbol of k, Al2

    proof

      ( the_arity_of P) = k by QC_LANG1: 11;

      then

       A1: (P `1 ) = (7 + k) by QC_LANG1:def 8;

      reconsider P as QC-pred_symbol of Al2 by Th3, TARSKI:def 3;

      ( the_arity_of P) = k by QC_LANG1:def 8, A1;

      hence thesis by QC_LANG3: 1;

    end;

    theorem :: QC_TRANS:7

    

     Th7: for Al2 be Al -expanding QC-alphabet holds for p holds p is Element of ( CQC-WFF Al2)

    proof

      let Al2 be Al -expanding QC-alphabet;

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

      

       A1: P[( VERUM Al)]

      proof

        ( VERUM Al) = ( VERUM Al2);

        hence thesis;

      end;

      

       A2: for k, P, l holds P[(P ! l)]

      proof

        let k, P, l;

        

         A3: ( the_arity_of P) = ( len l) by Th1;

        P is QC-pred_symbol of k, Al2 & l is CQC-variable_list of k, Al2 by Th5, Th6;

        then

        consider P2 be QC-pred_symbol of k, Al2, l2 be CQC-variable_list of k, Al2 such that

         A4: P = P2 & l = l2;

        ( the_arity_of P2) = ( len l2) by Th1;

        then (P2 ! l2) = ( <*P2*> ^ l2) by QC_LANG1:def 12;

        hence thesis by A3, A4, QC_LANG1:def 12;

      end;

      

       A5: P[p] implies P[( 'not' p)]

      proof

        assume P[p];

        then

        consider q be Element of ( CQC-WFF Al2) such that

         A6: p = q;

        ( 'not' p) = ( 'not' q) by A6;

        hence thesis;

      end;

      

       A7: P[p] & P[q] implies P[(p '&' q)]

      proof

        assume P[p] & P[q];

        then

        consider t,u be Element of ( CQC-WFF Al2) such that

         A8: p = t & q = u;

        (p '&' q) = (t '&' u) by A8;

        hence thesis;

      end;

      

       A9: for x holds P[p] implies P[( All (x,p))]

      proof

        let x;

        assume P[p];

        then

        consider q be Element of ( CQC-WFF Al2) such that

         A10: p = q;

        x is bound_QC-variable of Al2 by Th4, TARSKI:def 3;

        then

        consider y be bound_QC-variable of Al2 such that

         A11: x = y;

        ( All (x,p)) = ( All (y,q)) by A10, A11;

        hence thesis;

      end;

      

       A12: 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)]) & ( P[r] implies P[( All (x,r))]) by A1, A2, A5, A7, A9;

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

      hence for p holds p is Element of ( CQC-WFF Al2);

    end;

    definition

      let Al;

      let Al2 be Al -expanding QC-alphabet;

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

      :: QC_TRANS:def3

      func Al2 -Cast (p) -> Element of ( CQC-WFF Al2) equals p;

      coherence by Th7;

    end

    definition

      let Al;

      let Al2 be Al -expanding QC-alphabet;

      let x be bound_QC-variable of Al;

      :: QC_TRANS:def4

      func Al2 -Cast (x) -> bound_QC-variable of Al2 equals x;

      coherence by Th4, TARSKI:def 3;

    end

    definition

      let Al;

      let Al2 be Al -expanding QC-alphabet;

      let k;

      let P be QC-pred_symbol of k, Al;

      :: QC_TRANS:def5

      func Al2 -Cast (P) -> QC-pred_symbol of k, Al2 equals P;

      coherence by Th6;

    end

    definition

      let Al;

      let Al2 be Al -expanding QC-alphabet;

      let k;

      let l be CQC-variable_list of k, Al;

      :: QC_TRANS:def6

      func Al2 -Cast (l) -> CQC-variable_list of k, Al2 equals l;

      coherence by Th5;

    end

    theorem :: QC_TRANS:8

    

     Th8: for p, r, x, P, l holds for Al2 be Al -expanding QC-alphabet holds (Al2 -Cast ( VERUM Al)) = ( VERUM Al2) & (Al2 -Cast (P ! l)) = ((Al2 -Cast P) ! (Al2 -Cast l)) & (Al2 -Cast ( 'not' p)) = ( 'not' (Al2 -Cast p)) & (Al2 -Cast (p '&' r)) = ((Al2 -Cast p) '&' (Al2 -Cast r)) & (Al2 -Cast ( All (x,p))) = ( All ((Al2 -Cast x),(Al2 -Cast p)))

    proof

      let p, r, x, P, l;

      let Al2 be Al -expanding QC-alphabet;

      

       A1: ( the_arity_of P) = ( len l) by Th1;

      

       A2: ( the_arity_of (Al2 -Cast P)) = ( len (Al2 -Cast l)) by Th1;

      thus (Al2 -Cast ( VERUM Al)) = ( VERUM Al2);

      

      thus (Al2 -Cast (P ! l)) = ( <*P*> ^ l) by A1, QC_LANG1:def 12

      .= ((Al2 -Cast P) ! (Al2 -Cast l)) by A2, QC_LANG1:def 12;

      thus (Al2 -Cast ( 'not' p)) = ( 'not' (Al2 -Cast p));

      thus (Al2 -Cast (p '&' r)) = ((Al2 -Cast p) '&' (Al2 -Cast r));

      thus (Al2 -Cast ( All (x,p))) = ( All ((Al2 -Cast x),(Al2 -Cast p)));

    end;

    begin

    theorem :: QC_TRANS:9

    

     Th9: Jp = (J2 | ( QC-pred_symbols Al)) & vp = (v2 | ( bound_QC-variables Al)) implies ((J2,v2) |= (Al2 -Cast r) iff (Jp,vp) |= r)

    proof

      defpred T[ Element of ( CQC-WFF Al)] means for J2, Jp, v2, vp holds Jp = (J2 | ( QC-pred_symbols Al)) & vp = (v2 | ( bound_QC-variables Al)) implies (((J2,v2) |= (Al2 -Cast $1)) iff (Jp,vp) |= $1);

      

       A1: T[( VERUM Al)]

      proof

        let J2, Jp, v2, vp;

        (J2,v2) |= ( VERUM Al2) by VALUAT_1: 32;

        hence thesis by VALUAT_1: 32;

      end;

      

       A2: for k, P, l holds T[(P ! l)]

      proof

        let k, P, l;

        let J2, Jp, v2, vp;

        assume

         A3: Jp = (J2 | ( QC-pred_symbols Al)) & vp = (v2 | ( bound_QC-variables Al));

        set p = (P ! l);

        ( the_arity_of P) = ( len l) by Th1;

        then

         A4: (P ! l) = ( <*P*> ^ l) by QC_LANG1:def 12;

        P is QC-pred_symbol of k, Al2 & l is CQC-variable_list of k, Al2 by Th5, Th6;

        then

        consider P2 be QC-pred_symbol of k, Al2, l2 be CQC-variable_list of k, Al2 such that

         A5: P = P2 & l = l2;

        

         A6: ( the_arity_of P2) = ( len l2) by Th1;

        

         A7: (v2 *' l2) = (vp *' l)

        proof

          

           A8: ( bound_QC-variables Al) c= ( bound_QC-variables Al2) by Th4;

          

           A9: for j st 1 <= j & j <= ( len l) holds (l . j) in ( bound_QC-variables Al) iff (l . j) in ( bound_QC-variables Al2)

          proof

            let j such that

             A10: 1 <= j & j <= ( len l);

            thus (l . j) in ( bound_QC-variables Al) implies (l . j) in ( bound_QC-variables Al2) by A8;

            hereby

              assume (l . j) in ( bound_QC-variables Al2);

              ( len l) = k by CARD_1:def 7;

              then j in ( Seg k) by A10, FINSEQ_1: 1;

              then j in ( dom l) by FINSEQ_1: 89;

              hence (l . j) in ( bound_QC-variables Al) by FUNCT_1: 102;

            end;

          end;

          set t1 = { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( bound_QC-variables Al) };

          set t2 = { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( bound_QC-variables Al2) };

          

           A11: t1 = t2

          proof

            thus t1 c= t2

            proof

              let x be object;

              assume x in t1;

              then

              consider i such that

               A12: x = (l . i) & 1 <= i & i <= ( len l) & (l . i) in ( bound_QC-variables Al);

              x = (l . i) & 1 <= i & i <= ( len l) & (l . i) in ( bound_QC-variables Al2) by A9, A12;

              hence x in t2;

            end;

            thus t2 c= t1

            proof

              let x be object;

              assume x in t2;

              then

              consider i such that

               A13: x = (l . i) & 1 <= i & i <= ( len l) & (l . i) in ( bound_QC-variables Al2);

              x = (l . i) & 1 <= i & i <= ( len l) & (l . i) in ( bound_QC-variables Al) by A9, A13;

              hence x in t1;

            end;

          end;

          

           A14: ( still_not-bound_in l) = ( still_not-bound_in l2) by A5, A11;

          

           A15: (vp | ( still_not-bound_in l)) = (v2 | (( bound_QC-variables Al) /\ ( still_not-bound_in l))) by A3, RELAT_1: 71

          .= (v2 | ( still_not-bound_in l)) by XBOOLE_1: 28;

          (v2 *' l2) = (l * (vp | ( still_not-bound_in l))) by A5, A14, A15, SUBLEMMA: 59

          .= (vp *' l) by SUBLEMMA: 59;

          hence thesis;

        end;

        

         A16: (J2,v2) |= (Al2 -Cast (P ! l)) implies (Jp,vp) |= (P ! l)

        proof

          assume (J2,v2) |= (Al2 -Cast (P ! l));

          then (J2,v2) |= (P2 ! l2) by A4, A5, A6, QC_LANG1:def 12;

          then (( Valid ((P2 ! l2),J2)) . v2) = TRUE by VALUAT_1:def 7;

          then ((l2 'in' (J2 . P2)) . v2) = TRUE by VALUAT_1: 6;

          then

           A17: (vp *' l) in (J2 . P2) by A7, VALUAT_1:def 4;

          (vp *' l) in (Jp . P) by FUNCT_1: 49, A3, A5, A17;

          then ((l 'in' (Jp . P)) . vp) = TRUE by VALUAT_1:def 4;

          then (( Valid ((P ! l),Jp)) . vp) = TRUE by VALUAT_1: 6;

          hence thesis by VALUAT_1:def 7;

        end;

        ( not (J2,v2) |= (Al2 -Cast (P ! l))) implies ( not (Jp,vp) |= (P ! l))

        proof

          assume not (J2,v2) |= (Al2 -Cast (P ! l));

          then not (J2,v2) |= (P2 ! l2) by A4, A5, A6, QC_LANG1:def 12;

          then not (( Valid ((P2 ! l2),J2)) . v2) = TRUE by VALUAT_1:def 7;

          then not ((l2 'in' (J2 . P2)) . v2) = TRUE by VALUAT_1: 6;

          then

           A18: not (vp *' l) in (J2 . P2) by A7, VALUAT_1:def 4;

           not (vp *' l) in (Jp . P) by FUNCT_1: 49, A3, A5, A18;

          then not ((l 'in' (Jp . P)) . vp) = TRUE by VALUAT_1:def 4;

          then not (( Valid ((P ! l),Jp)) . vp) = TRUE by VALUAT_1: 6;

          hence thesis by VALUAT_1:def 7;

        end;

        hence thesis by A16;

      end;

      

       A19: for p holds T[p] implies T[( 'not' p)]

      proof

        let p;

        assume

         A20: T[p];

        let J2, Jp, v2, vp;

        assume

         A21: Jp = (J2 | ( QC-pred_symbols Al)) & vp = (v2 | ( bound_QC-variables Al));

        per cases ;

          suppose

           A22: not (J2,v2) |= (Al2 -Cast p);

          then

           A23: not (Jp,vp) |= p by A20, A21;

          (J2,v2) |= ( 'not' (Al2 -Cast p)) by A22, VALUAT_1: 17;

          hence thesis by A23, VALUAT_1: 17;

        end;

          suppose

           A24: (J2,v2) |= (Al2 -Cast p);

          then

           A25: (Jp,vp) |= p by A20, A21;

           not (J2,v2) |= ( 'not' (Al2 -Cast p)) by VALUAT_1: 17, A24;

          hence thesis by A25, VALUAT_1: 17;

        end;

      end;

      

       A26: for p, r holds ( T[p] & T[r]) implies T[(p '&' r)]

      proof

        let p, r;

        assume

         A27: T[p] & T[r];

        let J2, Jp, v2, vp;

        assume

         A28: Jp = (J2 | ( QC-pred_symbols Al)) & vp = (v2 | ( bound_QC-variables Al));

        

         A29: (J2,v2) |= (Al2 -Cast (p '&' r)) implies (Jp,vp) |= (p '&' r)

        proof

          assume (J2,v2) |= (Al2 -Cast (p '&' r));

          then (J2,v2) |= ((Al2 -Cast p) '&' (Al2 -Cast r));

          then (J2,v2) |= (Al2 -Cast p) & (J2,v2) |= (Al2 -Cast r) by VALUAT_1: 18;

          then (Jp,vp) |= p & (Jp,vp) |= r by A27, A28;

          hence (Jp,vp) |= (p '&' r) by VALUAT_1: 18;

        end;

        (Jp,vp) |= (p '&' r) implies (J2,v2) |= (Al2 -Cast (p '&' r))

        proof

          assume (Jp,vp) |= (p '&' r);

          then (Jp,vp) |= p & (Jp,vp) |= r by VALUAT_1: 18;

          then (J2,v2) |= (Al2 -Cast p) & (J2,v2) |= (Al2 -Cast r) by A27, A28;

          then (J2,v2) |= ((Al2 -Cast p) '&' (Al2 -Cast r)) by VALUAT_1: 18;

          hence (J2,v2) |= (Al2 -Cast (p '&' r));

        end;

        hence thesis by A29;

      end;

      

       A30: for x, r holds T[r] implies T[( All (x,r))]

      proof

        let x, r;

        assume

         A31: T[r];

        let J2, Jp, v2, vp;

        assume

         A32: Jp = (J2 | ( QC-pred_symbols Al)) & vp = (v2 | ( bound_QC-variables Al));

        

         A33: (J2,v2) |= (Al2 -Cast ( All (x,r))) implies (Jp,vp) |= ( All (x,r))

        proof

          assume (J2,v2) |= (Al2 -Cast ( All (x,r)));

          then

           A34: (J2,v2) |= ( All ((Al2 -Cast x),(Al2 -Cast r)));

          for vp1 be Element of ( Valuations_in (Al,A)) st for y be bound_QC-variable of Al st x <> y holds (vp1 . y) = (vp . y) holds (Jp,vp1) |= r

          proof

            let vp1 be Element of ( Valuations_in (Al,A)) such that

             A35: for y be bound_QC-variable of Al st x <> y holds (vp1 . y) = (vp . y);

            set s = ((Al2 -Cast x) .--> (vp1 . x));

            

             A36: s = ( {(Al2 -Cast x)} --> (vp1 . x)) by FUNCOP_1:def 9;

            set v21 = (v2 +* s);

            v2 is Element of ( Funcs (( bound_QC-variables Al2),A)) by VALUAT_1:def 1;

            then

             A37: ( dom v2) = ( bound_QC-variables Al2) & ( rng v2) c= A by FUNCT_2: 92;

            ( dom s) = {(Al2 -Cast x)} by A36;

            then ( dom v21) = (( dom v2) \/ {(Al2 -Cast x)}) by FUNCT_4:def 1;

            then

             A38: ( dom v21) = ( bound_QC-variables Al2) by A37, XBOOLE_1: 12;

            

             A39: (( rng v2) \/ {(vp1 . x)}) c= A by A37, XBOOLE_1: 8;

            ( rng s) = {(vp1 . x)} by A36, FUNCOP_1: 8;

            then ( rng v21) c= (( rng v2) \/ {(vp1 . x)}) by FUNCT_4: 17;

            then ( rng v21) c= A by A39;

            then v21 is Element of ( Funcs (( bound_QC-variables Al2),A)) by A38, FUNCT_2:def 2;

            then

            reconsider v21 as Element of ( Valuations_in (Al2,A)) by VALUAT_1:def 1;

            for y be bound_QC-variable of Al2 st (Al2 -Cast x) <> y holds (v21 . y) = (v2 . y) by FUNCT_4: 83;

            then

             A40: (J2,v21) |= (Al2 -Cast r) by A34, VALUAT_1: 29;

            vp1 is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

            

            then

             A41: ( dom vp1) = ( bound_QC-variables Al) by FUNCT_2: 92

            .= (( dom v21) /\ ( bound_QC-variables Al)) by A38, Th4, XBOOLE_1: 28;

            for c be object st c in ( dom vp1) holds (vp1 . c) = (v21 . c)

            proof

              let c be object such that

               A42: c in ( dom vp1);

              per cases ;

                suppose

                 A43: c = (Al2 -Cast x);

                then c in ( dom s) by FUNCOP_1: 74;

                

                hence (v21 . c) = (s . c) by FUNCT_4: 13

                .= (vp1 . c) by A43, FUNCOP_1: 72;

              end;

                suppose

                 A44: c <> (Al2 -Cast x);

                reconsider c as bound_QC-variable of Al by A41, A42, XBOOLE_0:def 4;

                (v21 . c) = (v2 . c) by A44, FUNCT_4: 83

                .= ((v2 | ( bound_QC-variables Al)) . c) by FUNCT_1: 49

                .= (vp1 . c) by A32, A35, A44;

                hence thesis;

              end;

            end;

            then (v21 | ( bound_QC-variables Al)) = vp1 by FUNCT_1: 46, A41;

            hence (Jp,vp1) |= r by A32, A31, A40;

          end;

          hence (Jp,vp) |= ( All (x,r)) by VALUAT_1: 29;

        end;

        (Jp,vp) |= ( All (x,r)) implies (J2,v2) |= (Al2 -Cast ( All (x,r)))

        proof

          assume

           A45: (Jp,vp) |= ( All (x,r));

          for v21 be Element of ( Valuations_in (Al2,A)) st for y be bound_QC-variable of Al2 st (Al2 -Cast x) <> y holds (v21 . y) = (v2 . y) holds (J2,v21) |= (Al2 -Cast r)

          proof

            let v21 be Element of ( Valuations_in (Al2,A)) such that

             A46: for y be bound_QC-variable of Al2 st (Al2 -Cast x) <> y holds (v21 . y) = (v2 . y);

            set s = (x .--> (v21 . (Al2 -Cast x)));

            

             A47: s = ( {x} --> (v21 . (Al2 -Cast x))) by FUNCOP_1:def 9;

            set vp1 = (vp +* s);

            vp is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

            then

             A48: ( dom vp) = ( bound_QC-variables Al) & ( rng vp) c= A by FUNCT_2: 92;

            ( dom s) = {x} by A47;

            then ( dom vp1) = (( dom vp) \/ {x}) by FUNCT_4:def 1;

            then

             A49: ( dom vp1) = ( bound_QC-variables Al) by A48, XBOOLE_1: 12;

            

             A50: (( rng vp) \/ {(v21 . (Al2 -Cast x))}) c= A by A48, XBOOLE_1: 8;

            ( rng s) = {(v21 . (Al2 -Cast x))} by A47, FUNCOP_1: 8;

            then ( rng vp1) c= (( rng vp) \/ {(v21 . (Al2 -Cast x))}) by FUNCT_4: 17;

            then ( rng vp1) c= A by A50;

            then vp1 is Element of ( Funcs (( bound_QC-variables Al),A)) by A49, FUNCT_2:def 2;

            then

            reconsider vp1 as Element of ( Valuations_in (Al,A)) by VALUAT_1:def 1;

            for y be bound_QC-variable of Al st x <> y holds (vp1 . y) = (vp . y) by FUNCT_4: 83;

            then

             A51: (Jp,vp1) |= r by A45, VALUAT_1: 29;

            v21 is Element of ( Funcs (( bound_QC-variables Al2),A)) by VALUAT_1:def 1;

            then

             A52: ( dom v21) = ( bound_QC-variables Al2) by FUNCT_2: 92;

            vp1 is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

            

            then

             A53: ( dom vp1) = ( bound_QC-variables Al) by FUNCT_2: 92

            .= (( dom v21) /\ ( bound_QC-variables Al)) by A52, Th4, XBOOLE_1: 28;

            for c be object st c in ( dom vp1) holds (vp1 . c) = (v21 . c)

            proof

              let c be object such that

               A54: c in ( dom vp1);

              per cases ;

                suppose

                 A55: c = x;

                then c in ( dom s) by FUNCOP_1: 74;

                

                then (vp1 . c) = (s . x) by A55, FUNCT_4: 13

                .= (v21 . c) by A55, FUNCOP_1: 72;

                hence (vp1 . c) = (v21 . c);

              end;

                suppose

                 A56: c <> x;

                

                 A57: c in ( bound_QC-variables Al) by A53, A54, XBOOLE_0:def 4;

                vp1 is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

                then ( dom vp1) = ( bound_QC-variables Al) by FUNCT_2: 92;

                then

                 A58: ( dom vp1) c= ( bound_QC-variables Al2) by Th4;

                (vp1 . c) = (vp . c) by A56, FUNCT_4: 83

                .= (v2 . c) by A32, A57, FUNCT_1: 49

                .= (v21 . c) by A56, A46, A54, A58;

                hence thesis;

              end;

            end;

            then (v21 | ( bound_QC-variables Al)) = vp1 by FUNCT_1: 46, A53;

            hence (J2,v21) |= (Al2 -Cast r) by A32, A31, A51;

          end;

          then (J2,v2) |= ( All ((Al2 -Cast x),(Al2 -Cast r))) by VALUAT_1: 29;

          hence (J2,v2) |= (Al2 -Cast ( All (x,r)));

        end;

        hence thesis by A33;

      end;

      

       A59: 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 T[( VERUM Al)] & T[(P ! l)] & ( T[r] implies T[( 'not' r)]) & ( T[r] & T[s] implies T[(r '&' s)]) & ( T[r] implies T[( All (x,r))]) by A1, A2, A19, A26, A30;

      for r be Element of ( CQC-WFF Al) holds T[r] from CQC_LANG:sch 1( A59);

      hence thesis;

    end;

    theorem :: QC_TRANS:10

    for Al2 be Al -expanding QC-alphabet, THETA be Subset of ( CQC-WFF Al2) st PHI c= THETA holds for A2 be non empty set, J2 be interpretation of Al2, A2, v2 be Element of ( Valuations_in (Al2,A2)) st (J2,v2) |= THETA holds ex A, J, v st (J,v) |= PHI

    proof

      let Al2 be Al -expanding QC-alphabet, THETA be Subset of ( CQC-WFF Al2) such that

       A1: PHI c= THETA;

      let A2 be non empty set, J2 be interpretation of Al2, A2, v2 be Element of ( Valuations_in (Al2,A2)) such that

       A2: (J2,v2) |= THETA;

      set A = A2;

      

       A3: ( QC-pred_symbols Al) c= ( QC-pred_symbols Al2) by Th3;

      set Jp = (J2 | ( QC-pred_symbols Al));

      reconsider Jp as Function of ( QC-pred_symbols Al), ( relations_on A) by A3, FUNCT_2: 32;

      for P be Element of ( QC-pred_symbols Al), r be Element of ( relations_on A) st (Jp . P) = r holds r = ( empty_rel A) or ( the_arity_of P) = ( the_arity_of r)

      proof

        let P be Element of ( QC-pred_symbols Al), r be Element of ( relations_on A) such that

         A4: (Jp . P) = r;

        P is Element of ( QC-pred_symbols Al2) by Th3, TARSKI:def 3;

        then

        consider Q be Element of ( QC-pred_symbols Al2) such that

         A5: P = Q;

        

         A6: (P `1 ) = (7 + ( the_arity_of P)) & (Q `1 ) = (7 + ( the_arity_of Q)) by QC_LANG1:def 8;

        (Jp . P) = (J2 . Q) by A5, FUNCT_1: 49;

        hence thesis by A4, A5, A6, VALUAT_1:def 5;

      end;

      then

      reconsider Jp as interpretation of Al, A by VALUAT_1:def 5;

      

       A7: ( bound_QC-variables Al) c= ( bound_QC-variables Al2) by Th4;

      set vp = (v2 | ( bound_QC-variables Al));

      reconsider vp as Function of ( bound_QC-variables Al), A by A7, FUNCT_2: 32;

      

       A8: ( Funcs (( bound_QC-variables Al),A)) = ( Valuations_in (Al,A)) by VALUAT_1:def 1;

      reconsider vp as Element of ( Valuations_in (Al,A)) by A8, FUNCT_2: 8;

      for r be Element of ( CQC-WFF Al) holds r in PHI implies (Jp,vp) |= r

      proof

        let r be Element of ( CQC-WFF Al) such that

         A9: r in PHI;

        (J2,v2) |= (Al2 -Cast r) by A1, A2, A9, CALCUL_1:def 11;

        hence thesis by Th9;

      end;

      hence thesis by CALCUL_1:def 11;

    end;

    theorem :: QC_TRANS:11

    

     Th11: for f be FinSequence of ( CQC-WFF Al2), g be FinSequence of ( CQC-WFF Al) st f = g holds ( Ant f) = ( Ant g) & ( Suc f) = ( Suc g)

    proof

      let f be FinSequence of ( CQC-WFF Al2), g be FinSequence of ( CQC-WFF Al) such that

       A1: f = g;

      per cases ;

        suppose

         A2: ( len f) > 0 ;

        then

        consider k be Nat such that

         A3: ( len f) = (k + 1) by NAT_1: 6;

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

        

        thus ( Ant f) = (g | ( Seg k)) by A1, A2, A3, CALCUL_1:def 1

        .= ( Ant g) by A1, A2, A3, CALCUL_1:def 1;

        ( Suc f) = (g . ( len g)) by A1, A2, CALCUL_1:def 2

        .= ( Suc g) by A1, A2, CALCUL_1:def 2;

        hence thesis;

      end;

        suppose

         A4: not ( len f) > 0 ;

        

        thus ( Ant f) = {} by A4, CALCUL_1:def 1

        .= ( Ant g) by A1, A4, CALCUL_1:def 1;

        

        thus ( Suc f) = ( VERUM Al2) by A4, CALCUL_1:def 2

        .= ( VERUM Al)

        .= ( Suc g) by A1, A4, CALCUL_1:def 2;

      end;

    end;

    theorem :: QC_TRANS:12

    

     Th12: for p holds ( still_not-bound_in p) = ( still_not-bound_in (Al2 -Cast p))

    proof

      defpred A[ Element of ( CQC-WFF Al)] means ( still_not-bound_in $1) = ( still_not-bound_in (Al2 -Cast $1));

      

       A1: A[( VERUM Al)]

      proof

        

        thus ( still_not-bound_in ( VERUM Al)) = {} by QC_LANG3: 3

        .= ( still_not-bound_in ( VERUM Al2)) by QC_LANG3: 3

        .= ( still_not-bound_in (Al2 -Cast ( VERUM Al)));

      end;

      

       A2: for k, P, l holds A[(P ! l)]

      proof

        let k, P, l;

        

         A3: ( still_not-bound_in l) = ( still_not-bound_in (Al2 -Cast l))

        proof

          for x be object st x in ( still_not-bound_in l) holds x in ( still_not-bound_in (Al2 -Cast l))

          proof

            let x be object such that

             A4: x in ( still_not-bound_in l);

            consider n such that

             A5: x = (l . n) & 1 <= n & n <= ( len l) & (l . n) in ( bound_QC-variables Al) by A4;

            set y = (l . n);

            reconsider y as bound_QC-variable of Al by A5;

            y = (Al2 -Cast y);

            hence thesis by A5;

          end;

          hence ( still_not-bound_in l) c= ( still_not-bound_in (Al2 -Cast l));

          for x be object st x in ( still_not-bound_in (Al2 -Cast l)) holds x in ( still_not-bound_in l)

          proof

            let x be object such that

             A6: x in ( still_not-bound_in (Al2 -Cast l));

            consider n such that

             A7: x = ((Al2 -Cast l) . n) & 1 <= n & n <= ( len (Al2 -Cast l)) & ((Al2 -Cast l) . n) in ( bound_QC-variables Al2) by A6;

            set y = ((Al2 -Cast l) . n);

            ( rng l) c= ( bound_QC-variables Al) & ( dom l) = ( Seg ( len l)) by FINSEQ_1:def 3;

            then y = (l . n) & n in ( dom l) & l is FinSequence of ( bound_QC-variables Al) by A7, FINSEQ_1: 1, FINSEQ_1:def 4;

            then y in ( bound_QC-variables Al) by FINSEQ_2: 11;

            hence thesis by A7;

          end;

          hence ( still_not-bound_in (Al2 -Cast l)) c= ( still_not-bound_in l);

        end;

        

        thus ( still_not-bound_in (P ! l)) = ( still_not-bound_in l) by QC_LANG3: 5

        .= ( still_not-bound_in ((Al2 -Cast P) ! (Al2 -Cast l))) by A3, QC_LANG3: 5

        .= ( still_not-bound_in (Al2 -Cast (P ! l))) by Th8;

      end;

      

       A8: for p holds A[p] implies A[( 'not' p)]

      proof

        let p such that

         A9: A[p];

        

        thus ( still_not-bound_in ( 'not' p)) = ( still_not-bound_in p) by QC_LANG3: 7

        .= ( still_not-bound_in ( 'not' (Al2 -Cast p))) by A9, QC_LANG3: 7

        .= ( still_not-bound_in (Al2 -Cast ( 'not' p)));

      end;

      

       A10: for p, q holds A[p] & A[q] implies A[(p '&' q)]

      proof

        let p, q such that

         A11: A[p] & A[q];

        set p2 = (Al2 -Cast p);

        set q2 = (Al2 -Cast q);

        reconsider p2, q2 as Element of ( CQC-WFF Al2);

        (p '&' q) is conjunctive & (p2 '&' q2) is conjunctive;

        then

         A12: p = ( the_left_argument_of (p '&' q)) & q = ( the_right_argument_of (p '&' q)) & p2 = ( the_left_argument_of (p2 '&' q2)) & q2 = ( the_right_argument_of (p2 '&' q2)) by QC_LANG1:def 25, QC_LANG1:def 26;

        

        hence ( still_not-bound_in (p '&' q)) = (( still_not-bound_in p) \/ ( still_not-bound_in q)) by QC_LANG1:def 20, QC_LANG3: 9

        .= ( still_not-bound_in (Al2 -Cast (p '&' q))) by A11, A12, QC_LANG1:def 20, QC_LANG3: 9;

      end;

      for x, p holds A[p] implies A[( All (x,p))]

      proof

        let x, p such that

         A13: A[p];

        set x2 = (Al2 -Cast x);

        set p2 = (Al2 -Cast p);

        reconsider p2 as Element of ( CQC-WFF Al2);

        reconsider x2 as bound_QC-variable of Al2;

        ( All (x,p)) is universal & ( All (x2,p2)) is universal;

        then

         A14: p = ( the_scope_of ( All (x,p))) & x = ( bound_in ( All (x,p))) & p2 = ( the_scope_of ( All (x2,p2))) & x2 = ( bound_in ( All (x2,p2))) by QC_LANG1:def 27, QC_LANG1:def 28;

        

        then ( still_not-bound_in ( All (x,p))) = (( still_not-bound_in p) \ {x}) by QC_LANG3: 11, QC_LANG1:def 21

        .= ( still_not-bound_in (Al2 -Cast ( All (x,p)))) by A13, A14, QC_LANG1:def 21, QC_LANG3: 11;

        hence thesis;

      end;

      then

       A15: for p, q, x, k, l, P holds A[( VERUM Al)] & A[(P ! l)] & ( A[p] implies A[( 'not' p)]) & ( A[p] & A[q] implies A[(p '&' q)]) & ( A[p] implies A[( All (x,p))]) by A1, A2, A8, A10;

      for p holds A[p] from CQC_LANG:sch 1( A15);

      hence thesis;

    end;

    theorem :: QC_TRANS:13

    

     Th13: for p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2, x2 be bound_QC-variable of Al2, x, p st p = p2 & S = S2 & x = x2 holds ( RestrictSub (x,p,S)) = ( RestrictSub (x2,p2,S2))

    proof

      let p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2, x2 be bound_QC-variable of Al2, x, p such that

       A1: p = p2 & S = S2 & x = x2;

      set rset = { y where y be bound_QC-variable of Al : y in ( still_not-bound_in p) & y is Element of ( dom S) & y <> x & y <> (S . y) };

      set rset2 = { y2 where y2 be bound_QC-variable of Al2 : y2 in ( still_not-bound_in p2) & y2 is Element of ( dom S2) & y2 <> x2 & y2 <> (S2 . y2) };

      rset = rset2

      proof

        for s be object st s in rset holds s in rset2

        proof

          let s be object such that

           A2: s in rset;

          consider y be bound_QC-variable of Al such that

           A3: s = y & y in ( still_not-bound_in p) & y is Element of ( dom S) & y <> x & y <> (S . y) by A2;

          reconsider y as bound_QC-variable of Al2 by Th4, TARSKI:def 3;

          p2 = (Al2 -Cast p) by A1;

          then y in ( still_not-bound_in p2) & y is Element of ( dom S2) & y <> x2 & y <> (S2 . y) by A1, A3, Th12;

          hence s in rset2 by A3;

        end;

        hence rset c= rset2;

        for s2 be object st s2 in rset2 holds s2 in rset

        proof

          let s2 be object such that

           A4: s2 in rset2;

          consider y2 be bound_QC-variable of Al2 such that

           A5: s2 = y2 & y2 in ( still_not-bound_in p2) & y2 is Element of ( dom S2) & y2 <> x2 & y2 <> (S2 . y2) by A4;

          p2 = (Al2 -Cast p) by A1;

          then

           A6: y2 in ( still_not-bound_in p) by A5, Th12;

          then

          reconsider y2 as bound_QC-variable of Al;

          thus s2 in rset by A1, A5, A6;

        end;

        hence rset2 c= rset;

      end;

      then (S | rset) = (S2 | rset2) & (S | rset) = ( RestrictSub (x,p,S)) & (S2 | rset2) = ( RestrictSub (x2,p2,S2)) by A1, SUBSTUT1:def 6;

      hence thesis;

    end;

    theorem :: QC_TRANS:14

    

     Th14: for p2 be Element of ( CQC-WFF Al2), S be finite CQC_Substitution of Al, S2 be finite CQC_Substitution of Al2, p st S = S2 & p = p2 holds ( upVar (S,p)) = ( upVar (S2,p2))

    proof

      let p2 be Element of ( CQC-WFF Al2), S be finite CQC_Substitution of Al, S2 be finite CQC_Substitution of Al2, p such that

       A1: S = S2 & p = p2;

      

       A2: ( Sub_Var S) = ( Sub_Var S2)

      proof

        for s be object st s in ( Sub_Var S) holds s in ( Sub_Var S2)

        proof

          let s be object such that

           A3: s in ( Sub_Var S);

          s in { t where t be QC-symbol of Al : ( x. t) in ( rng S) } by A3, SUBSTUT1:def 10;

          then

          consider s2 be QC-symbol of Al such that

           A4: s = s2 & ( x. s2) in ( rng S);

          s2 in ( QC-symbols Al) & ( QC-symbols Al) c= ( QC-symbols Al2) by Th2;

          then

          consider s3 be QC-symbol of Al2 such that

           A5: s3 = s2;

          ( x. s2) = [4, s2] by QC_LANG3:def 2

          .= ( x. s3) by A5, QC_LANG3:def 2;

          then s3 in { t where t be QC-symbol of Al2 : ( x. t) in ( rng S2) } by A1, A4;

          hence thesis by A4, A5, SUBSTUT1:def 10;

        end;

        hence ( Sub_Var S) c= ( Sub_Var S2);

        for s be object st s in ( Sub_Var S2) holds s in ( Sub_Var S)

        proof

          let s be object such that

           A6: s in ( Sub_Var S2);

          s in { t where t be QC-symbol of Al2 : ( x. t) in ( rng S2) } by A6, SUBSTUT1:def 10;

          then

          consider s2 be QC-symbol of Al2 such that

           A7: s = s2 & ( x. s2) in ( rng S2);

          

           A8: ( rng ( @ S)) c= ( bound_QC-variables Al) by SUBSTUT1: 39;

          ( x. s2) in ( rng ( @ S)) by A1, A7, SUBSTUT1:def 2;

          then ( x. s2) in ( bound_QC-variables Al) by A8;

          then [4, s2] in [: {4}, ( QC-symbols Al):] by QC_LANG3:def 2;

          then s2 in ( QC-symbols Al) by ZFMISC_1: 87;

          then

          consider s3 be QC-symbol of Al such that

           A9: s3 = s2;

          ( x. s2) = [4, s2] by QC_LANG3:def 2

          .= ( x. s3) by A9, QC_LANG3:def 2;

          then s3 in { t where t be QC-symbol of Al : ( x. t) in ( rng S) } by A1, A7;

          hence thesis by A7, A9, SUBSTUT1:def 10;

        end;

        hence ( Sub_Var S2) c= ( Sub_Var S);

      end;

      defpred P[ Element of ( QC-WFF Al)] means for q2 be Element of ( CQC-WFF Al2) st $1 = q2 holds ( Bound_Vars $1) = ( Bound_Vars q2);

      

       A10: P[( VERUM Al)]

      proof

        let q2 be Element of ( CQC-WFF Al2) such that

         A11: q2 = ( VERUM Al);

        q2 = ( VERUM Al2) by A11;

        

        hence ( Bound_Vars q2) = {} by SUBSTUT1: 2

        .= ( Bound_Vars ( VERUM Al)) by SUBSTUT1: 2;

      end;

      

       A12: for k, P, l holds P[(P ! l)]

      proof

        let k, P, l;

        set P2 = (Al2 -Cast P);

        set l2 = (Al2 -Cast l);

        let q2 be Element of ( CQC-WFF Al2) such that

         A13: (P ! l) = q2;

        

         A14: q2 = (Al2 -Cast (P ! l)) by A13

        .= (P2 ! l2) by Th8;

        

        thus ( Bound_Vars (P ! l)) = ( still_not-bound_in (P ! l)) by SUBLEMMA: 43

        .= ( still_not-bound_in (Al2 -Cast (P ! l))) by Th12

        .= ( still_not-bound_in (P2 ! l2)) by Th8

        .= ( Bound_Vars q2) by A14, SUBLEMMA: 43;

      end;

      

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

      proof

        let r, s such that

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

        set q = (r '&' s);

        set r2 = (Al2 -Cast r);

        set s2 = (Al2 -Cast s);

        let q2 be Element of ( CQC-WFF Al2) such that

         A17: (r '&' s) = q2;

        

         A18: q2 = (r2 '&' s2) by A17;

        then q is conjunctive & q2 is conjunctive;

        then

         A19: ( the_left_argument_of q) = r & ( the_right_argument_of q) = s & ( the_left_argument_of q2) = r2 & ( the_right_argument_of q2) = s2 by A18, QC_LANG1:def 25, QC_LANG1:def 26;

        

         A20: ( Bound_Vars r) = ( Bound_Vars r2) & ( Bound_Vars s) = ( Bound_Vars s2) by A16;

        

        thus ( Bound_Vars q) = (( Bound_Vars r) \/ ( Bound_Vars s)) by A19, SUBSTUT1: 5, QC_LANG1:def 20

        .= ( Bound_Vars q2) by A18, A19, A20, SUBSTUT1: 5, QC_LANG1:def 20;

      end;

      

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

      proof

        let r such that

         A22: P[r];

        set q = ( 'not' r);

        set r2 = (Al2 -Cast r);

        let q2 be Element of ( CQC-WFF Al2) such that

         A23: q = q2;

        

         A24: q2 = ( 'not' r2) by A23;

        then q is negative & q2 is negative;

        then

         A25: ( the_argument_of q) = r & ( the_argument_of q2) = r2 by A24, QC_LANG1:def 24;

        

        thus ( Bound_Vars q) = ( Bound_Vars r) by A25, SUBSTUT1: 4, QC_LANG1:def 19

        .= ( Bound_Vars r2) by A22

        .= ( Bound_Vars q2) by A24, A25, SUBSTUT1: 4, QC_LANG1:def 19;

      end;

      

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

      proof

        let x, r such that

         A27: P[r];

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

        set r2 = (Al2 -Cast r);

        set x2 = (Al2 -Cast x);

        let q2 be Element of ( CQC-WFF Al2) such that

         A28: q = q2;

        

         A29: q2 = ( All (x2,r2)) by A28;

        then q is universal & q2 is universal;

        then

         A30: ( the_scope_of q) = r & ( bound_in q) = x & ( the_scope_of q2) = r2 & ( bound_in q2) = x2 by A29, QC_LANG1:def 27, QC_LANG1:def 28;

        

        thus ( Bound_Vars q) = (( Bound_Vars r) \/ {x}) by A30, SUBSTUT1: 6, QC_LANG1:def 21

        .= (( Bound_Vars r2) \/ {x2}) by A27

        .= ( Bound_Vars q2) by A29, A30, SUBSTUT1: 6, QC_LANG1:def 21;

      end;

      

       A31: for r, s, x, k, l, P 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 A10, A12, A15, A21, A26;

      

       A32: for q be Element of ( CQC-WFF Al) holds P[q] from CQC_LANG:sch 1( A31);

      

       A33: ( Dom_Bound_Vars p) = ( Dom_Bound_Vars p2)

      proof

        for s be object st s in ( Dom_Bound_Vars p) holds s in ( Dom_Bound_Vars p2)

        proof

          let s be object such that

           A34: s in ( Dom_Bound_Vars p);

          s in { b where b be QC-symbol of Al : ( x. b) in ( Bound_Vars p) } by A34, SUBSTUT1:def 9;

          then

          consider s2 be QC-symbol of Al such that

           A35: s = s2 & ( x. s2) in ( Bound_Vars p);

          ( x. s2) in ( Bound_Vars p2) by A1, A32, A35;

          then ( x. s2) in ( bound_QC-variables Al2);

          then [4, s2] in [: {4}, ( QC-symbols Al2):] by QC_LANG3:def 2;

          then s2 in ( QC-symbols Al2) by ZFMISC_1: 87;

          then

          consider s3 be QC-symbol of Al2 such that

           A36: s3 = s2;

          ( x. s2) = [4, s2] by QC_LANG3:def 2

          .= ( x. s3) by A36, QC_LANG3:def 2;

          then ( x. s3) in ( Bound_Vars p2) by A1, A32, A35;

          then s3 in { b where b be QC-symbol of Al2 : ( x. b) in ( Bound_Vars p2) };

          hence thesis by A35, A36, SUBSTUT1:def 9;

        end;

        hence ( Dom_Bound_Vars p) c= ( Dom_Bound_Vars p2);

        for s be object st s in ( Dom_Bound_Vars p2) holds s in ( Dom_Bound_Vars p)

        proof

          let s be object such that

           A37: s in ( Dom_Bound_Vars p2);

          s in { b where b be QC-symbol of Al2 : ( x. b) in ( Bound_Vars p2) } by A37, SUBSTUT1:def 9;

          then

          consider s2 be QC-symbol of Al2 such that

           A38: s = s2 & ( x. s2) in ( Bound_Vars p2);

          ( x. s2) in ( Bound_Vars p) by A1, A32, A38;

          then ( x. s2) in ( bound_QC-variables Al);

          then [4, s2] in [: {4}, ( QC-symbols Al):] by QC_LANG3:def 2;

          then s2 in ( QC-symbols Al) by ZFMISC_1: 87;

          then

          consider s3 be QC-symbol of Al such that

           A39: s3 = s2;

          ( x. s2) = [4, s2] by QC_LANG3:def 2

          .= ( x. s3) by A39, QC_LANG3:def 2;

          then ( x. s3) in ( Bound_Vars p) by A1, A32, A38;

          then s3 in { b where b be QC-symbol of Al : ( x. b) in ( Bound_Vars p) };

          hence thesis by A38, A39, SUBSTUT1:def 9;

        end;

        hence ( Dom_Bound_Vars p2) c= ( Dom_Bound_Vars p);

      end;

      

       A40: ( NSub (p,S)) = ( NAT \ (( Dom_Bound_Vars p) \/ ( Sub_Var S))) by SUBSTUT1:def 11

      .= ( NSub (p2,S2)) by A2, A33, SUBSTUT1:def 11;

      

      thus ( upVar (S,p)) = the Element of ( NSub (p,S)) by SUBSTUT1:def 12

      .= ( upVar (S2,p2)) by A40, SUBSTUT1:def 12;

    end;

    theorem :: QC_TRANS:15

    

     Th15: for p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2, x2 be bound_QC-variable of Al2, x, p st p = p2 & S = S2 & x = x2 holds ( ExpandSub (x,p,( RestrictSub (x,( All (x,p)),S)))) = ( ExpandSub (x2,p2,( RestrictSub (x2,( All (x2,p2)),S2))))

    proof

      let p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2, x2 be bound_QC-variable of Al2, x, p such that

       A1: p = p2 & S = S2 & x = x2;

      set rsub = ( RestrictSub (x,( All (x,p)),S));

      set rsub2 = ( RestrictSub (x2,( All (x2,p2)),S2));

      set esub = ( ExpandSub (x,p,rsub));

      set esub2 = ( ExpandSub (x2,p2,rsub2));

      set uv = ( upVar (rsub,p));

      set uv2 = ( upVar (rsub2,p2));

      

       A2: ( x. uv) = [4, uv] by QC_LANG3:def 2

      .= [4, uv2] by A1, Th13, Th14

      .= ( x. uv2) by QC_LANG3:def 2;

      per cases ;

        suppose

         A3: not x in ( rng rsub);

        then not x2 in ( rng rsub2) by A1, Th13;

        

        hence esub2 = (rsub2 \/ { [x2, x2]}) by SUBSTUT1:def 13

        .= (rsub \/ { [x, x]}) by A1, Th13

        .= esub by A3, SUBSTUT1:def 13;

      end;

        suppose

         A4: x in ( rng rsub);

        then x2 in ( rng rsub2) by A1, Th13;

        

        hence esub2 = (rsub2 \/ { [x2, ( x. uv2)]}) by SUBSTUT1:def 13

        .= (rsub \/ { [x, ( x. uv)]}) by A1, Th13, A2

        .= esub by A4, SUBSTUT1:def 13;

      end;

    end;

    theorem :: QC_TRANS:16

    

     Th16: for Z be Element of ( CQC-Sub-WFF Al), Z2 be Element of ( CQC-Sub-WFF Al2) st (Z `1 ) is universal & (Z2 `1 ) is universal & ( bound_in (Z `1 )) = ( bound_in (Z2 `1 )) & ( the_scope_of (Z `1 )) = ( the_scope_of (Z2 `1 )) & Z = Z2 holds ( S_Bound ( @ Z)) = ( S_Bound ( @ Z2))

    proof

      let Z be Element of ( CQC-Sub-WFF Al), Z2 be Element of ( CQC-Sub-WFF Al2) such that

       A1: (Z `1 ) is universal & (Z2 `1 ) is universal & ( bound_in (Z `1 )) = ( bound_in (Z2 `1 )) & ( the_scope_of (Z `1 )) = ( the_scope_of (Z2 `1 )) & Z = Z2;

      set p = (( @ Z) `1 );

      set p2 = (( @ Z2) `1 );

      set S = (( @ Z) `2 );

      set S2 = (( @ Z2) `2 );

      reconsider p as Element of ( CQC-WFF Al) by A1, SUBSTUT1:def 35;

      reconsider p2 as Element of ( CQC-WFF Al2) by A1, SUBSTUT1:def 35;

      reconsider S as CQC_Substitution of Al;

      reconsider S2 as CQC_Substitution of Al2;

      set x = ( bound_in p);

      set x2 = ( bound_in p2);

      set q = ( the_scope_of p);

      set q2 = ( the_scope_of p2);

      p is universal by A1, SUBSTUT1:def 35;

      then p = ( All (x,q)) by QC_LANG2: 6;

      then

      reconsider q as Element of ( CQC-WFF Al) by CQC_LANG: 13;

      p2 is universal by A1, SUBSTUT1:def 35;

      then p2 = ( All (x2,q2)) by QC_LANG2: 6;

      then

      reconsider q2 as Element of ( CQC-WFF Al2) by CQC_LANG: 13;

      reconsider x as bound_QC-variable of Al;

      reconsider x2 as bound_QC-variable of Al2;

      

       A2: p = (Z `1 ) by SUBSTUT1:def 35

      .= p2 by A1, SUBSTUT1:def 35;

      

       A3: S = (Z `2 ) by SUBSTUT1:def 35

      .= S2 by A1, SUBSTUT1:def 35;

      

       A4: x = ( bound_in (Z `1 )) by SUBSTUT1:def 35

      .= x2 by A1, SUBSTUT1:def 35;

      

       A5: q = ( the_scope_of (Z `1 )) by SUBSTUT1:def 35

      .= q2 by A1, SUBSTUT1:def 35;

      set rsub = ( RestrictSub (x,p,S));

      set rsub2 = ( RestrictSub (x2,p2,S2));

      per cases ;

        suppose

         A6: not x in ( rng rsub);

        then not x2 in ( rng rsub2) by A2, A3, A4, Th13;

        

        hence ( S_Bound ( @ Z2)) = x2 by SUBSTUT1:def 36

        .= ( S_Bound ( @ Z)) by A4, A6, SUBSTUT1:def 36;

      end;

        suppose

         A7: x in ( rng rsub);

        then x2 in ( rng rsub2) by A2, A3, A4, Th13;

        

        then ( S_Bound ( @ Z2)) = ( x. ( upVar (rsub2,q2))) by SUBSTUT1:def 36

        .= [4, ( upVar (rsub2,q2))] by QC_LANG3:def 2

        .= [4, ( upVar (rsub,q))] by A5, A2, A3, A4, Th13, Th14

        .= ( x. ( upVar (rsub,q))) by QC_LANG3:def 2

        .= ( S_Bound ( @ Z)) by A7, SUBSTUT1:def 36;

        hence thesis;

      end;

    end;

    theorem :: QC_TRANS:17

    

     Th17: for p2 be Element of ( CQC-WFF Al2), x2,y2 be bound_QC-variable of Al2, p, x, y st p = p2 & x = x2 & y = y2 holds (p . (x,y)) = (p2 . (x2,y2))

    proof

      defpred P[ Element of ( CQC-WFF Al)] means for p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2 st $1 = p2 & S = S2 holds ( CQC_Sub [$1, S]) = ( CQC_Sub [p2, S2]);

      

       A1: P[( VERUM Al)]

      proof

        set p = ( VERUM Al);

        let p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2 such that

         A2: p = p2 & S = S2;

        

         A3: ( VERUM Al2) = p2 by A2;

        

         A4: [p, S] is Al -Sub_VERUM & [p2, S2] is Al2 -Sub_VERUM by A3, SUBSTUT1:def 19;

        

        thus ( CQC_Sub [p, S]) = ( VERUM Al2) by A4, SUBLEMMA: 3

        .= ( CQC_Sub [p2, S2]) by A4, SUBLEMMA: 3;

      end;

      

       A5: for k, P, l holds P[(P ! l)]

      proof

        let k, P, l;

        set P2 = (Al2 -Cast P);

        set l2 = (Al2 -Cast l);

        reconsider P2 as QC-pred_symbol of k, Al2;

        reconsider l2 as CQC-variable_list of k, Al2;

        let p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2 such that

         A6: (P ! l) = p2 & S = S2;

        

         A7: p2 = (Al2 -Cast (P ! l)) by A6

        .= (P2 ! l2) by Th8;

        set p = (P ! l);

        reconsider p as Element of ( CQC-WFF Al);

        set sub = ( CQC_Subst (l,S));

        

         A8: sub = ( CQC_Subst ((Al2 -Cast l),S2))

        proof

          

           A9: ( len sub) = ( len l) by SUBSTUT1:def 3

          .= ( len ( CQC_Subst ((Al2 -Cast l),S2))) by SUBSTUT1:def 3;

          for n be Nat st n in ( dom sub) holds (sub . n) = (( CQC_Subst ((Al2 -Cast l),S2)) . n)

          proof

            let n be Nat such that

             A10: n in ( dom sub);

            n in ( Seg ( len sub)) by A10, FINSEQ_1:def 3;

            then 1 <= n & n <= ( len sub) by FINSEQ_1: 1;

            then

             A11: 1 <= n & n <= ( len l) by SUBSTUT1:def 3;

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

            per cases ;

              suppose

               A12: (l . n) in ( dom S);

              (sub . n) = (S . (l . n)) by A11, A12, SUBSTUT1:def 3

              .= (( CQC_Subst ((Al2 -Cast l),S2)) . n) by A6, A11, A12, SUBSTUT1:def 3;

              hence thesis;

            end;

              suppose

               A13: not (l . n) in ( dom S);

              (sub . n) = (l . n) by A11, A13, SUBSTUT1:def 3

              .= (( CQC_Subst ((Al2 -Cast l),S2)) . n) by A6, A11, A13, SUBSTUT1:def 3;

              hence thesis;

            end;

          end;

          hence thesis by A9, FINSEQ_2: 9;

        end;

        ( the_arity_of P) = ( len l) & ( the_arity_of P2) = ( len l2) by Th1;

        then

         A14: [(P ! l), S] = ( Sub_P (P,l,S)) & [(P2 ! l2), S2] = ( Sub_P (P2,l2,S2)) by SUBSTUT1:def 18;

        (P ! l) is atomic & (P2 ! l2) is atomic;

        then

         A15: P = ( the_pred_symbol_of (P ! l)) & P2 = ( the_pred_symbol_of (P2 ! l2)) by QC_LANG1:def 22;

        

         A16: ( [(P ! l), S] `1 ) = (P ! l) & ( [(P ! l), S] `2 ) = S & ( [(P2 ! l2), S2] `1 ) = (P2 ! l2) & ( [(P2 ! l2), S2] `2 ) = S2 & ( Sub_the_arguments_of [(P ! l), S]) = l & ( Sub_the_arguments_of [(P2 ! l2), S2]) = l2 by A14, SUBSTUT1:def 29;

        

        thus ( CQC_Sub [(P ! l), S]) = (Al2 -Cast (P ! ( CQC_Subst (l,S)))) by A14, A15, A16, SUBLEMMA: 6

        .= ((Al2 -Cast P) ! (Al2 -Cast ( CQC_Subst (l,S)))) by Th8

        .= ( CQC_Sub [p2, S2]) by A7, A8, A14, A15, A16, SUBLEMMA: 6;

      end;

      

       A17: for q st P[q] holds P[( 'not' q)]

      proof

        let q such that

         A18: P[q];

        set p = ( 'not' q);

        reconsider p as Element of ( CQC-WFF Al);

        set q2 = (Al2 -Cast q);

        reconsider q2 as Element of ( CQC-WFF Al2);

        let p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2 such that

         A19: ( 'not' q) = p2 & S = S2;

        

         A20: ( [q, S] `1 ) = q & ( [q, S] `2 ) = S & ( [q2, S2] `1 ) = q2 & ( [q2, S2] `2 ) = S2;

        

        thus ( CQC_Sub [( 'not' q), S]) = ( CQC_Sub ( Sub_not [q, S])) by A20, SUBSTUT1:def 20

        .= (Al2 -Cast ( 'not' ( CQC_Sub [q, S]))) by SUBSTUT1: 29

        .= ( 'not' ( CQC_Sub [q2, S2])) by A18, A19

        .= ( CQC_Sub ( Sub_not [q2, S2])) by SUBSTUT1: 29

        .= ( CQC_Sub [( 'not' q2), S2]) by A20, SUBSTUT1:def 20

        .= ( CQC_Sub [p2, S2]) by A19;

      end;

      

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

      proof

        let r, s such that

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

        set r2 = (Al2 -Cast r);

        set s2 = (Al2 -Cast s);

        reconsider r2, s2 as Element of ( CQC-WFF Al2);

        let p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2 such that

         A23: (r '&' s) = p2 & S = S2;

        

         A24: ( CQC_Sub [r, S]) = ( CQC_Sub [r2, S2]) & ( CQC_Sub [s, S]) = ( CQC_Sub [s2, S2]) by A22, A23;

        

         A25: ( [r, S] `1 ) = r & ( [r, S] `2 ) = S & ( [s, S] `1 ) = s & ( [s, S] `2 ) = S & ( [r2, S2] `1 ) = r2 & ( [r2, S2] `2 ) = S2 & ( [s2, S2] `1 ) = s2 & ( [s2, S2] `2 ) = S2;

        

        thus ( CQC_Sub [(r '&' s), S]) = ( CQC_Sub ( CQCSub_& ( [r, S], [s, S]))) by SUBSTUT2: 19

        .= (Al2 -Cast (( CQC_Sub [r, S]) '&' ( CQC_Sub [s, S]))) by A25, SUBLEMMA: 23

        .= ((Al2 -Cast ( CQC_Sub [r, S])) '&' (Al2 -Cast ( CQC_Sub [s, S])))

        .= ( CQC_Sub ( CQCSub_& ( [r2, S2], [s2, S2]))) by A24, A25, SUBLEMMA: 23

        .= ( CQC_Sub [(r2 '&' s2), S2]) by SUBSTUT2: 19

        .= ( CQC_Sub [p2, S2]) by A23;

      end;

      for z be bound_QC-variable of Al, q st P[q] holds P[( All (z,q))]

      proof

        let z be bound_QC-variable of Al, q such that

         A26: P[q];

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

        set q2 = (Al2 -Cast q);

        set z2 = (Al2 -Cast z);

        reconsider p as Element of ( CQC-WFF Al);

        let p2 be Element of ( CQC-WFF Al2), S be CQC_Substitution of Al, S2 be CQC_Substitution of Al2 such that

         A27: ( All (z,q)) = p2 & S = S2;

        set qsc = ( Qsc (q,z,S));

        set qsc2 = ( Qsc (q2,z2,S2));

        set sub = [( All (z,q)), S];

        set sub2 = [( All (z2,q2)), S2];

        set qscope = [q, (( CFQ Al) . sub)];

        set qscope2 = [q2, (( CFQ Al2) . sub2)];

        

         A28: ( QScope (q,z,S)) = [qscope, z] by SUBSTUT2:def 3;

        reconsider qscope as Element of ( CQC-Sub-WFF Al);

        reconsider qsc as second_Q_comp of [qscope, z] by SUBSTUT2:def 3;

        

         A29: ( QScope (q2,z2,S2)) = [qscope2, z2] by SUBSTUT2:def 3;

        reconsider qscope2 as Element of ( CQC-Sub-WFF Al2);

        reconsider qsc2 as second_Q_comp of [qscope2, z2] by SUBSTUT2:def 3;

        

         A30: sub = ( CQCSub_All ( [qscope, z],qsc)) & [qscope, z] is quantifiable & sub2 = ( CQCSub_All ( [qscope2, z2],qsc2)) & [qscope2, z2] is quantifiable by A28, A29, SUBSTUT2: 22;

        set expandsub = ( ExpandSub (z,q,( RestrictSub (z,( All (z,q)),S))));

        set expandsub2 = ( ExpandSub (z2,q2,( RestrictSub (z2,( All (z2,q2)),S2))));

        

         A31: ( All (z,q)) is universal & ( All (z2,q2)) is universal;

        then z = ( bound_in ( All (z,q))) & q = ( the_scope_of ( All (z,q))) & z2 = ( bound_in ( All (z2,q2))) & q2 = ( the_scope_of ( All (z2,q2))) by QC_LANG1:def 27, QC_LANG1:def 28;

        then (( All (z,q)),S) PQSub expandsub & (( All (z2,q2)),S2) PQSub expandsub2 by A31, SUBSTUT1:def 14;

        then [sub, expandsub] in ( QSub Al) & [sub2, expandsub2] in ( QSub Al2) by SUBSTUT1:def 15;

        then [sub, expandsub] in (( QSub Al) | ( CQC-Sub-WFF Al)) & [sub2, expandsub2] in (( QSub Al2) | ( CQC-Sub-WFF Al2)) by RELAT_1:def 11;

        then

         A32: [sub, expandsub] in ( CFQ Al) & [sub2, expandsub2] in ( CFQ Al2) by SUBSTUT2:def 2;

        set scope = ( CQCSub_the_scope_of sub);

        set scope2 = ( CQCSub_the_scope_of sub2);

        

         A33: ( bound_in (sub `1 )) = z by A31, QC_LANG1:def 27

        .= ( bound_in (sub2 `1 )) by A31, QC_LANG1:def 27;

        

         A34: ( the_scope_of (sub `1 )) = q by A31, QC_LANG1:def 28

        .= ( the_scope_of (sub2 `1 )) by A31, QC_LANG1:def 28;

        

         A35: expandsub = expandsub2 by A27, Th15;

        

         A36: ( CQC_Sub qscope) = ( CQC_Sub [q, expandsub]) by A32, FUNCT_1: 1

        .= ( CQC_Sub qscope2) by A26, A32, A35, FUNCT_1: 1;

        ( CQC_Sub [p, S]) = ( CQCQuant (sub,( CQC_Sub scope))) by A30, SUBLEMMA: 27, SUBLEMMA: 28

        .= ( Quant (sub,( CQC_Sub scope))) by A30, SUBLEMMA: 27, SUBLEMMA:def 7

        .= ( All (( S_Bound ( @ sub)),( CQC_Sub scope))) by SUBSTUT1:def 37

        .= (Al2 -Cast ( All (( S_Bound ( @ sub)),( CQC_Sub qscope)))) by A30, SUBLEMMA: 30

        .= ( All (( S_Bound ( @ sub2)),( CQC_Sub qscope2))) by A36, A27, A31, A33, A34, Th16

        .= ( All (( S_Bound ( @ sub2)),( CQC_Sub scope2))) by A30, SUBLEMMA: 30

        .= ( Quant (sub2,( CQC_Sub scope2))) by SUBSTUT1:def 37

        .= ( CQCQuant (sub2,( CQC_Sub scope2))) by A30, SUBLEMMA: 27, SUBLEMMA:def 7

        .= ( CQC_Sub [p2, S2]) by A27, A30, SUBLEMMA: 27, SUBLEMMA: 28;

        hence thesis;

      end;

      then

       A37: for r, s, x, k, l, P 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, A5, A17, A21;

      

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

      let p2 be Element of ( CQC-WFF Al2), x2,y2 be bound_QC-variable of Al2, p, x, y such that

       A39: p = p2 & x = x2 & y = y2;

      

      thus (p . (x,y)) = ( CQC_Sub [p, ( Sbst (x,y))]) by SUBSTUT2:def 1

      .= ( CQC_Sub [p2, ( Sbst (x2,y2))]) by A38, A39

      .= (p2 . (x2,y2)) by SUBSTUT2:def 1;

    end;

    theorem :: QC_TRANS:18

    

     Th18: for PHI be Consistent Subset of ( CQC-WFF Al2) st PHI is Subset of ( CQC-WFF Al) holds PHI is Al -Consistent

    proof

      let PHI be Consistent Subset of ( CQC-WFF Al2) such that PHI is Subset of ( CQC-WFF Al);

      for S be Subset of ( CQC-WFF Al) st PHI = S holds S is Consistent

      proof

        let S be Subset of ( CQC-WFF Al) such that

         A1: PHI = S;

        assume

         A2: S is Inconsistent;

        PHI |- ( 'not' ( VERUM Al2))

        proof

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

           A3: ( rng f) c= S & |- (f ^ <*( 'not' ( VERUM Al))*>) by A2, GOEDELCP: 24, HENMODEL:def 1;

          set f2 = f;

          for x be object st x in ( rng f2) holds x in ( CQC-WFF Al2)

          proof

            let x be object such that

             A4: x in ( rng f2);

            x in PHI by A1, A3, A4;

            hence x in ( CQC-WFF Al2);

          end;

          then

          reconsider f2 as FinSequence of ( CQC-WFF Al2) by FINSEQ_1:def 4, TARSKI:def 3;

          consider PR such that

           A5: PR is a_proof & (f ^ <*( 'not' ( VERUM Al))*>) = ((PR . ( len PR)) `1 ) by A3, CALCUL_1:def 9;

          

           A6: PR <> {} & for n be Nat st 1 <= n & n <= ( len PR) holds (PR,n) is_a_correct_step by A5, CALCUL_1:def 8;

          set PR2 = PR;

          PR2 is FinSequence of [:( set_of_CQC-WFF-seq Al2), Proof_Step_Kinds :]

          proof

            for p be object holds p in ( CQC-WFF Al) implies p in ( CQC-WFF Al2)

            proof

              let p be object;

              assume p in ( CQC-WFF Al);

              then p is Element of ( CQC-WFF Al2) by Th7;

              hence thesis;

            end;

            then

             A7: ( CQC-WFF Al) c= ( CQC-WFF Al2) & ( rng PR2) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

            for x be object holds x in ( set_of_CQC-WFF-seq Al) implies x in ( set_of_CQC-WFF-seq Al2)

            proof

              let x be object;

              assume x in ( set_of_CQC-WFF-seq Al);

              then

              reconsider x as FinSequence of ( CQC-WFF Al) by CALCUL_1:def 6;

              ( rng x) c= ( CQC-WFF Al2) by A7;

              then x is FinSequence of ( CQC-WFF Al2) by FINSEQ_1:def 4;

              hence thesis by CALCUL_1:def 6;

            end;

            then ( set_of_CQC-WFF-seq Al) c= ( set_of_CQC-WFF-seq Al2);

            then [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] c= [:( set_of_CQC-WFF-seq Al2), Proof_Step_Kinds :] by ZFMISC_1: 95;

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

            hence thesis by FINSEQ_1:def 4;

          end;

          then

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

          

           A8: PR2 is a_proof

          proof

            for n be Nat st 1 <= n & n <= ( len PR2) holds (PR2,n) is_a_correct_step

            proof

              let n be Nat such that

               A9: 1 <= n & n <= ( len PR2);

              

               A10: (for i st 1 <= i & i < n holds ((PR2 . i) `1 ) in ( set_of_CQC-WFF-seq Al2)) & (((PR2 . n) `1 ) in ( set_of_CQC-WFF-seq Al2))

              proof

                thus for i st 1 <= i & i < n holds ((PR2 . i) `1 ) in ( set_of_CQC-WFF-seq Al2)

                proof

                  let i such that

                   A11: 1 <= i & i < n;

                  set k = (( len PR2) - n);

                  reconsider k as Element of NAT by A9, NAT_1: 21;

                  ( len PR2) = (n + k);

                  then

                   A12: 1 <= i & i <= ( len PR2) by A11, NAT_1: 12;

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

                  then i in ( dom PR2) by A12, FINSEQ_1: 1;

                  then (PR2 . i) in ( rng PR2) by FUNCT_1:def 3;

                  hence ((PR2 . i) `1 ) in ( set_of_CQC-WFF-seq Al2) by MCART_1: 10;

                end;

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

                then n in ( dom PR2) by A9, FINSEQ_1: 1;

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

                hence ((PR2 . n) `1 ) in ( set_of_CQC-WFF-seq Al2) by MCART_1: 10;

              end;

              

               A13: (PR,n) is_a_correct_step by A5, CALCUL_1:def 8, A9;

              ((PR . n) `2 ) = 0 or ... or ((PR . n) `2 ) = 9 by CALCUL_1: 31, A9;

              per cases ;

                suppose

                 A14: ((PR2 . n) `2 ) = 0 ;

                then

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

                 A15: (( Suc g2) is_tail_of ( Ant g2) & ((PR2 . n) `1 ) = g2) by A13, CALCUL_1:def 7;

                g2 is FinSequence of ( CQC-WFF Al2) by A10, A15, CALCUL_1:def 6;

                then

                consider g be FinSequence of ( CQC-WFF Al2) such that

                 A16: g = g2;

                

                 A17: ( Suc g) = ( Suc g2) & ( Ant g) = ( Ant g2) by A16, Th11;

                thus thesis by A14, A15, A16, A17, CALCUL_1:def 7;

              end;

                suppose

                 A18: ((PR2 . n) `2 ) = 1;

                then

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

                 A19: (((PR . n) `1 ) = (g2 ^ <*( VERUM Al)*>)) by A13, CALCUL_1:def 7;

                (g2 ^ <*( VERUM Al)*>) is FinSequence of ( CQC-WFF Al2) by A10, A19, CALCUL_1:def 6;

                then

                consider gp be FinSequence of ( CQC-WFF Al2) such that

                 A20: gp = (g2 ^ <*( VERUM Al)*>);

                ( len gp) <> 0 by A20;

                then

                consider g be FinSequence of ( CQC-WFF Al2), v be Element of ( CQC-WFF Al2) such that

                 A21: gp = (g ^ <*v*>) by FINSEQ_2: 19;

                v = ( VERUM Al2) by A20, A21, FINSEQ_2: 17;

                hence thesis by A18, A19, A20, A21, CALCUL_1:def 7;

              end;

                suppose

                 A22: ((PR2 . n) `2 ) = 2;

                then

                consider i be Nat, g2,h2 be FinSequence of ( CQC-WFF Al) such that

                 A23: (1 <= i & i < n & ( Ant g2) is_Subsequence_of ( Ant h2) & ( Suc g2) = ( Suc h2) & ((PR2 . i) `1 ) = g2 & ((PR2 . n) `1 ) = h2) by A13, CALCUL_1:def 7;

                g2 in ( set_of_CQC-WFF-seq Al2) & h2 in ( set_of_CQC-WFF-seq Al2) by A10, A23;

                then h2 is FinSequence of ( CQC-WFF Al2) & g2 is FinSequence of ( CQC-WFF Al2) by CALCUL_1:def 6;

                then

                consider g,h be FinSequence of ( CQC-WFF Al2) such that

                 A24: g = g2 & h = h2;

                

                 A25: ( Suc g) = ( Suc g2) by A24, Th11

                .= ( Suc h) by A23, A24, Th11;

                consider N be Subset of NAT such that

                 A26: ( Ant g2) c= ( Seq (( Ant h2) | N)) by A23, CALCUL_1:def 4;

                (( Ant h2) | N) = (( Ant h) | N) by A24, Th11;

                then ( Ant g) c= ( Seq (( Ant h) | N)) by A24, A26, Th11;

                then

                 A27: ( Ant g) is_Subsequence_of ( Ant h) by CALCUL_1:def 4;

                thus thesis by A22, A23, A24, A25, A27, CALCUL_1:def 7;

              end;

                suppose

                 A28: ((PR2 . n) `2 ) = 3;

                then

                consider i,j be Nat, g,h be FinSequence of ( CQC-WFF Al) such that

                 A29: (1 <= i & i < n & 1 <= j & j < i & ( len g) > 1 & ( len h) > 1 & ( Ant ( Ant g)) = ( Ant ( Ant h)) & ( 'not' ( Suc ( Ant g))) = ( Suc ( Ant h)) & ( Suc g) = ( Suc h) & g = ((PR2 . j) `1 ) & h = ((PR2 . i) `1 ) & (( Ant ( Ant g)) ^ <*( Suc g)*>) = ((PR2 . n) `1 )) by A13, CALCUL_1:def 7;

                ((PR2 . j) `1 ) = g & ((PR2 . i) `1 ) = h & j < n by A29, XXREAL_0: 2;

                then g in ( set_of_CQC-WFF-seq Al2) & h in ( set_of_CQC-WFF-seq Al2) by A10, A29;

                then h is FinSequence of ( CQC-WFF Al2) & g is FinSequence of ( CQC-WFF Al2) by CALCUL_1:def 6;

                then

                consider g2,h2 be FinSequence of ( CQC-WFF Al2) such that

                 A30: g2 = g & h2 = h;

                

                 A31: ( Ant g2) = ( Ant g) & ( Ant h2) = ( Ant h) by A30, Th11;

                

                then

                 A32: ( Ant ( Ant g2)) = ( Ant ( Ant g)) by Th11

                .= ( Ant ( Ant h2)) by A29, A31, Th11;

                

                 A33: ( 'not' ( Suc ( Ant g2))) = ( 'not' (Al2 -Cast ( Suc ( Ant g)))) by A31, Th11

                .= ( Suc ( Ant h2)) by A29, A31, Th11;

                

                 A34: ( Suc g2) = ( Suc g) by A30, Th11

                .= ( Suc h2) by A29, A30, Th11;

                

                 A35: ((PR2 . n) `1 ) = (( Ant ( Ant g)) ^ <*( Suc g2)*>) by A29, A30, Th11

                .= (( Ant ( Ant g2)) ^ <*( Suc g2)*>) by A31, Th11;

                thus thesis by A28, A29, A30, A32, A33, A34, A35, CALCUL_1:def 7;

              end;

                suppose

                 A36: ((PR2 . n) `2 ) = 4;

                then

                consider i,j be Nat, g,h be FinSequence of ( CQC-WFF Al), p be Element of ( CQC-WFF Al) such that

                 A37: (1 <= i & i < n & 1 <= j & j < i & ( len g) > 1 & ( Ant g) = ( Ant h) & ( Suc ( Ant g)) = ( 'not' p) & ( 'not' ( Suc g)) = ( Suc h) & g = ((PR2 . j) `1 ) & h = ((PR2 . i) `1 ) & (( Ant ( Ant g)) ^ <*p*>) = ((PR2 . n) `1 )) by A13, CALCUL_1:def 7;

                ((PR2 . j) `1 ) = g & ((PR2 . i) `1 ) = h & j < n by A37, XXREAL_0: 2;

                then g in ( set_of_CQC-WFF-seq Al2) & h in ( set_of_CQC-WFF-seq Al2) by A10, A37;

                then h is FinSequence of ( CQC-WFF Al2) & g is FinSequence of ( CQC-WFF Al2) by CALCUL_1:def 6;

                then

                consider g2,h2 be FinSequence of ( CQC-WFF Al2) such that

                 A38: g2 = g & h2 = h;

                

                 A39: ( Ant g2) = ( Ant g) by A38, Th11

                .= ( Ant h2) by A37, A38, Th11;

                ( Ant g2) = ( Ant g) by A38, Th11;

                then

                 A40: ( Suc ( Ant g2)) = ( 'not' (Al2 -Cast p)) by A37, Th11;

                

                 A41: ( 'not' ( Suc g2)) = ( 'not' (Al2 -Cast ( Suc g))) by A38, Th11

                .= ( Suc h2) by A37, A38, Th11;

                ( Ant g2) = ( Ant g) by A38, Th11;

                then (( Ant ( Ant g2)) ^ <*(Al2 -Cast p)*>) = ((PR2 . n) `1 ) by Th11, A37;

                hence thesis by A36, A37, A38, A39, A40, A41, CALCUL_1:def 7;

              end;

                suppose

                 A42: ((PR2 . n) `2 ) = 5;

                then

                consider i,j be Nat, g,h be FinSequence of ( CQC-WFF Al) such that

                 A43: (1 <= i & i < n & 1 <= j & j < i & ( Ant g) = ( Ant h) & g = ((PR2 . j) `1 ) & h = ((PR2 . i) `1 ) & (( Ant g) ^ <*(( Suc g) '&' ( Suc h))*>) = ((PR2 . n) `1 )) by A13, CALCUL_1:def 7;

                ((PR2 . j) `1 ) = g & ((PR2 . i) `1 ) = h & j < n by A43, XXREAL_0: 2;

                then g in ( set_of_CQC-WFF-seq Al2) & h in ( set_of_CQC-WFF-seq Al2) by A10, A43;

                then h is FinSequence of ( CQC-WFF Al2) & g is FinSequence of ( CQC-WFF Al2) by CALCUL_1:def 6;

                then

                consider g2,h2 be FinSequence of ( CQC-WFF Al2) such that

                 A44: g = g2 & h = h2;

                (Al2 -Cast ( Suc g)) = ( Suc g2) & (Al2 -Cast ( Suc h)) = ( Suc h2) by A44, Th11;

                then

                 A45: (( Ant g2) ^ <*(( Suc g2) '&' ( Suc h2))*>) = ((PR2 . n) `1 ) by A43, A44, Th11;

                ( Ant g2) = ( Ant g) by A44, Th11

                .= ( Ant h2) by A43, A44, Th11;

                hence thesis by A42, A43, A44, A45, CALCUL_1:def 7;

              end;

                suppose

                 A46: ((PR2 . n) `2 ) = 6;

                then

                consider i be Nat, g be FinSequence of ( CQC-WFF Al), p,q be Element of ( CQC-WFF Al) such that

                 A47: (1 <= i & i < n & (p '&' q) = ( Suc g) & g = ((PR2 . i) `1 ) & (( Ant g) ^ <*p*>) = ((PR2 . n) `1 )) by A13, CALCUL_1:def 7;

                g in ( set_of_CQC-WFF-seq Al2) by A10, A47;

                then g is FinSequence of ( CQC-WFF Al2) by CALCUL_1:def 6;

                then

                consider g2 be FinSequence of ( CQC-WFF Al2) such that

                 A48: g = g2;

                

                 A49: ( Suc g2) = ((Al2 -Cast p) '&' (Al2 -Cast q)) by A47, A48, Th11;

                (( Ant g2) ^ <*p*>) = ((PR2 . n) `1 ) by A47, A48, Th11;

                hence thesis by A46, A47, A48, A49, CALCUL_1:def 7;

              end;

                suppose

                 A50: ((PR2 . n) `2 ) = 7;

                then

                consider i be Nat, g be FinSequence of ( CQC-WFF Al), p,q be Element of ( CQC-WFF Al) such that

                 A51: (1 <= i & i < n & (p '&' q) = ( Suc g) & g = ((PR2 . i) `1 ) & (( Ant g) ^ <*q*>) = ((PR2 . n) `1 )) by A13, CALCUL_1:def 7;

                g in ( set_of_CQC-WFF-seq Al2) by A10, A51;

                then g is FinSequence of ( CQC-WFF Al2) by CALCUL_1:def 6;

                then

                reconsider g2 = g as FinSequence of ( CQC-WFF Al2);

                

                 A52: ( Suc g2) = ((Al2 -Cast p) '&' (Al2 -Cast q)) by A51, Th11;

                (( Ant g2) ^ <*(Al2 -Cast q)*>) = ((PR2 . n) `1 ) by A51, Th11;

                hence thesis by A50, A51, A52, CALCUL_1:def 7;

              end;

                suppose

                 A53: ((PR2 . n) `2 ) = 8;

                then

                consider i be Nat, g be FinSequence of ( CQC-WFF Al), p be Element of ( CQC-WFF Al), x,y be bound_QC-variable of Al such that

                 A54: (1 <= i & i < n & ( Suc g) = ( All (x,p)) & g = ((PR2 . i) `1 ) & (( Ant g) ^ <*(p . (x,y))*>) = ((PR2 . n) `1 )) by A13, CALCUL_1:def 7;

                g in ( set_of_CQC-WFF-seq Al2) by A10, A54;

                then g is FinSequence of ( CQC-WFF Al2) by CALCUL_1:def 6;

                then

                consider g2 be FinSequence of ( CQC-WFF Al2) such that

                 A55: g = g2;

                p is Element of ( CQC-WFF Al2) & x is bound_QC-variable of Al2 & y is bound_QC-variable of Al2 by Th4, Th7, TARSKI:def 3;

                then

                consider q be Element of ( CQC-WFF Al2), a,b be bound_QC-variable of Al2 such that

                 A56: a = x & b = y & q = p;

                

                 A57: ((PR2 . n) `1 ) = (( Ant g) ^ <*(q . (a,b))*>) by A54, A56, Th17

                .= (( Ant g2) ^ <*(q . (a,b))*>) by A55, Th11;

                ( Suc g2) = ( All (a,q)) by A54, A55, A56, Th11;

                hence thesis by A53, A54, A55, A57, CALCUL_1:def 7;

              end;

                suppose

                 A58: ((PR2 . n) `2 ) = 9;

                then

                consider i be Nat, g be FinSequence of ( CQC-WFF Al), p be Element of ( CQC-WFF Al), x,y be bound_QC-variable of Al such that

                 A59: (1 <= i & i < n & ( Suc g) = (p . (x,y)) & not y in ( still_not-bound_in ( Ant g)) & not y in ( still_not-bound_in ( All (x,p))) & g = ((PR2 . i) `1 ) & (( Ant g) ^ <*( All (x,p))*>) = ((PR2 . n) `1 )) by A13, CALCUL_1:def 7;

                g in ( set_of_CQC-WFF-seq Al2) by A10, A59;

                then g is FinSequence of ( CQC-WFF Al2) by CALCUL_1:def 6;

                then

                consider g2 be FinSequence of ( CQC-WFF Al2) such that

                 A60: g = g2;

                p is Element of ( CQC-WFF Al2) & x is bound_QC-variable of Al2 & y is bound_QC-variable of Al2 by Th4, Th7, TARSKI:def 3;

                then

                consider q be Element of ( CQC-WFF Al2), a,b be bound_QC-variable of Al2 such that

                 A61: q = p & a = x & b = y;

                

                 A62: ( Suc g2) = ( Suc g) by A60, Th11

                .= (q . (a,b)) by A59, A61, Th17;

                

                 A63: ( still_not-bound_in ( All (x,p))) = ( still_not-bound_in (Al2 -Cast ( All (x,p)))) by Th12

                .= ( still_not-bound_in ( All (a,q))) by A61;

                

                 A64: not b in ( still_not-bound_in ( Ant g2))

                proof

                  assume b in ( still_not-bound_in ( Ant g2));

                  then

                  consider i be Nat, r be Element of ( CQC-WFF Al2) such that

                   A65: i in ( dom ( Ant g2)) & r = (( Ant g2) . i) & b in ( still_not-bound_in r) by CALCUL_1:def 5;

                  

                   A66: ( dom ( Ant g2)) = ( dom ( Ant g)) by A60, Th11;

                  r = (( Ant g) . i) by A60, A65, Th11;

                  then

                  reconsider r as Element of ( CQC-WFF Al) by A65, A66, FINSEQ_2: 11;

                  i in ( dom ( Ant g)) & (Al2 -Cast r) = (( Ant g) . i) & b in ( still_not-bound_in (Al2 -Cast r)) by A60, A65, Th11;

                  then i in ( dom ( Ant g)) & r = (( Ant g) . i) & y in ( still_not-bound_in r) by A61, Th12;

                  hence contradiction by A59, CALCUL_1:def 5;

                end;

                (( Ant g2) ^ <*( All (a,q))*>) = ((PR2 . n) `1 ) by A59, A60, A61, Th11;

                hence thesis by A58, A59, A60, A61, A62, A63, A64, CALCUL_1:def 7;

              end;

            end;

            hence thesis by A6, CALCUL_1:def 8;

          end;

           |- (f2 ^ <*( 'not' ( VERUM Al2))*>) by A5, A8, CALCUL_1:def 9;

          hence thesis by A1, A3, HENMODEL:def 1;

        end;

        hence contradiction by GOEDELCP: 24;

      end;

      hence thesis;

    end;

    begin

    theorem :: QC_TRANS:19

    

     Th19: for p holds ex Al1 be countable QC-alphabet st p is Element of ( CQC-WFF Al1) & Al is Al1 -expanding

    proof

      defpred P[ Element of ( CQC-WFF Al)] means ex Al1 be countable QC-alphabet st $1 is Element of ( CQC-WFF Al1) & Al is Al1 -expanding;

      

       A1: P[( VERUM Al)]

      proof

        set Al1 = [: NAT , NAT :];

        reconsider Al1 as countable QC-alphabet by QC_LANG1:def 1, CARD_4: 7;

         NAT c= ( QC-symbols Al) & Al = [: NAT , ( QC-symbols Al):] by QC_LANG1: 3, QC_LANG1: 5;

        then Al1 c= Al by ZFMISC_1: 95;

        then

        reconsider Al as Al1 -expanding QC-alphabet by Def1;

        ( VERUM Al1) = ( VERUM Al);

        hence thesis;

      end;

      

       A2: for k, P, l holds P[(P ! l)]

      proof

        let k, P, l;

        ( bound_QC-variables Al) c= ( QC-variables Al) & ( QC-variables Al) c= [: NAT , ( QC-symbols Al):] by QC_LANG1: 4;

        then ( bound_QC-variables Al) c= [: NAT , ( QC-symbols Al):];

        then

        consider A,B be set such that

         A3: A is finite & A c= NAT & B is finite & B c= ( QC-symbols Al) & ( rng l) c= [:A, B:] by FINSET_1: 13, XBOOLE_1: 1;

         [:A, B:] c= [: NAT , B:] by A3, ZFMISC_1: 95;

        then

         A4: ( rng l) c= [: NAT , B:] by A3;

        set Al1 = (( [: NAT , NAT :] \/ [: NAT , {(P `2 )}:]) \/ [: NAT , B:]);

         [: NAT , NAT :] is countable & [: NAT , {(P `2 )}:] is countable by CARD_4: 7;

        then

         A5: ( [: NAT , NAT :] \/ [: NAT , {(P `2 )}:]) is countable & [: NAT , B:] is countable by A3, CARD_2: 85, CARD_4: 7;

        

         A6: Al1 = ( [: NAT , ( NAT \/ {(P `2 )}):] \/ [: NAT , B:]) by ZFMISC_1: 97

        .= [: NAT , (( NAT \/ {(P `2 )}) \/ B):] by ZFMISC_1: 97;

         NAT c= ( NAT \/ {(P `2 )}) & ( NAT \/ {(P `2 )}) c= (( NAT \/ {(P `2 )}) \/ B) by XBOOLE_1: 7;

        then

        reconsider Al1 as countable QC-alphabet by A5, A6, QC_LANG1:def 1, CARD_2: 85, XBOOLE_1: 1;

        P in [: NAT , ( QC-symbols Al):] by TARSKI:def 3, QC_LANG1: 6;

        then

        consider a,b be object such that

         A7: a in NAT & b in ( QC-symbols Al) & P = [a, b] by ZFMISC_1:def 2;

        (P `2 ) in ( QC-symbols Al) by A7;

        then {(P `2 )} c= ( QC-symbols Al) & NAT c= NAT & NAT c= ( QC-symbols Al) by QC_LANG1: 3, ZFMISC_1: 31;

        then [: NAT , {(P `2 )}:] c= [: NAT , ( QC-symbols Al):] & [: NAT , NAT :] c= [: NAT , ( QC-symbols Al):] by ZFMISC_1: 95;

        then ( [: NAT , NAT :] \/ [: NAT , {(P `2 )}:]) c= [: NAT , ( QC-symbols Al):] & [: NAT , B:] c= [: NAT , ( QC-symbols Al):] by A3, ZFMISC_1: 95, XBOOLE_1: 8;

        then Al1 c= [: NAT , ( QC-symbols Al):] by XBOOLE_1: 8;

        then Al1 c= Al by QC_LANG1: 5;

        then

        reconsider Al as Al1 -expanding QC-alphabet by Def1;

         [: NAT , (( NAT \/ {(P `2 )}) \/ B):] = [: NAT , ( QC-symbols Al1):] by A6, QC_LANG1: 5;

        then

         A8: ( QC-symbols Al1) = (( NAT \/ {(P `2 )}) \/ B) by ZFMISC_1: 110;

        set P2 = [a, b];

        b = (P `2 ) by A7;

        then b in {(P `2 )} by TARSKI:def 1;

        then b in ( NAT \/ {(P `2 )}) by XBOOLE_0:def 3;

        then

        reconsider b as QC-symbol of Al1 by A8, XBOOLE_0:def 3;

        reconsider a as Element of NAT by A7;

        

         A9: (P `1 ) = (7 + ( the_arity_of P)) & (P `1 ) = a by A7, QC_LANG1:def 8;

        then 7 <= a by NAT_1: 11;

        then [a, b] in { [n, x] where x be QC-symbol of Al1 : 7 <= n };

        then

        reconsider P2 as QC-pred_symbol of Al1;

        (P2 `1 ) = (7 + k) by A9, QC_LANG1: 11;

        then ( the_arity_of P2) = k by QC_LANG1:def 8;

        then P2 in { Q where Q be QC-pred_symbol of Al1 : ( the_arity_of Q) = k };

        then

        reconsider P2 as QC-pred_symbol of k, Al1;

        set l2 = l;

        for s be object st s in ( rng l2) holds s in ( bound_QC-variables Al1)

        proof

          let s be object such that

           A10: s in ( rng l2);

          consider s1,s2 be object such that

           A11: s1 in {4} & s2 in ( QC-symbols Al) & s = [s1, s2] by A10, ZFMISC_1:def 2;

          B c= ( QC-symbols Al1) by A8, XBOOLE_1: 7;

          then

           A12: [: NAT , B:] c= [: NAT , ( QC-symbols Al1):] by ZFMISC_1: 95;

          s in [: NAT , B:] by A4, A10;

          then

          consider s3,s4 be object such that

           A13: s3 in NAT & s4 in ( QC-symbols Al1) & s = [s3, s4] by A12, ZFMISC_1:def 2;

          s = [s1, s4] by A11, A13, XTUPLE_0: 1;

          hence thesis by A11, A13, ZFMISC_1:def 2;

        end;

        then

         A14: ( rng l2) c= ( bound_QC-variables Al1);

        reconsider l2 as CQC-variable_list of k, Al1 by A14, FINSEQ_1:def 4, XBOOLE_1: 1;

        (P2 ! l2) = (Al -Cast (P2 ! l2))

        .= ((Al -Cast P2) ! (Al -Cast l2)) by Th8

        .= (P ! l) by A7;

        then (P ! l) is Element of ( CQC-WFF Al1) & Al is Al1 -expanding;

        hence thesis;

      end;

      

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

      proof

        let r such that

         A16: P[r];

        consider Al1 be countable QC-alphabet such that

         A17: r is Element of ( CQC-WFF Al1) & Al is Al1 -expanding by A16;

        reconsider Al as Al1 -expanding QC-alphabet by A17;

        consider r2 be Element of ( CQC-WFF Al1) such that

         A18: r = r2 by A17;

        ( 'not' r2) = ( 'not' r) by A18;

        hence thesis by A17;

      end;

      

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

      proof

        let r, s such that

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

        consider Al1,Al2 be countable QC-alphabet such that

         A21: r is Element of ( CQC-WFF Al1) & s is Element of ( CQC-WFF Al2) & Al is Al1 -expanding & Al is Al2 -expanding by A20;

        set Al3 = (Al1 \/ Al2);

        Al1 = [: NAT , ( QC-symbols Al1):] & Al2 = [: NAT , ( QC-symbols Al2):] by QC_LANG1: 5;

        then

         A22: Al3 = [: NAT , (( QC-symbols Al1) \/ ( QC-symbols Al2)):] by ZFMISC_1: 97;

         NAT c= (( QC-symbols Al1) \/ ( QC-symbols Al2)) by XBOOLE_1: 10, QC_LANG1: 3;

        then

        reconsider Al3 as QC-alphabet by A22, QC_LANG1:def 1;

        reconsider Al3 as countableAl1 -expandingAl2 -expanding QC-alphabet by Def1, CARD_2: 85, XBOOLE_1: 7;

        consider r2 be Element of ( CQC-WFF Al1), s2 be Element of ( CQC-WFF Al2) such that

         A23: r2 = r & s2 = s by A21;

        reconsider r2 as Element of ( CQC-WFF Al3) by Th7;

        reconsider s2 as Element of ( CQC-WFF Al3) by Th7;

        Al1 c= Al & Al2 c= Al by A21;

        then

        reconsider Al as Al3 -expanding QC-alphabet by Def1, XBOOLE_1: 8;

        (r2 '&' s2) = (r '&' s) by A23;

        then (r '&' s) is Element of ( CQC-WFF Al3) & Al is Al3 -expanding;

        hence thesis;

      end;

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

      proof

        let x, r such that

         A24: P[r];

        consider Al1 be countable QC-alphabet such that

         A25: r is Element of ( CQC-WFF Al1) & Al is Al1 -expanding by A24;

        consider s1,s2 be object such that

         A26: s1 in {4} & s2 in ( QC-symbols Al) & x = [s1, s2] by ZFMISC_1:def 2;

        set Al2 = [: NAT , (( QC-symbols Al1) \/ {s2}):];

        

         A27: Al1 = [: NAT , ( QC-symbols Al1):] & ( QC-symbols Al1) c= (( QC-symbols Al1) \/ {s2}) & NAT c= ( QC-symbols Al1) by QC_LANG1: 3, QC_LANG1: 5, XBOOLE_1: 7;

        then Al1 c= Al2 & NAT c= (( QC-symbols Al1) \/ {s2}) by ZFMISC_1: 95;

        then

        reconsider Al2 as Al1 -expanding QC-alphabet by Def1, QC_LANG1:def 1;

        

         A28: Al2 = ( [: NAT , ( QC-symbols Al1):] \/ [: NAT , {s2}:]) & [: NAT , ( QC-symbols Al1):] c= Al by A25, A27, ZFMISC_1: 97;

         [: NAT , ( QC-symbols Al1):] is countable & [: NAT , {s2}:] is countable by QC_LANG1: 5, CARD_4: 7;

        then

        reconsider Al2 as countableAl1 -expanding QC-alphabet by A28, CARD_2: 85;

         {s2} c= ( QC-symbols Al) by A26, ZFMISC_1: 31;

        then [: NAT , {s2}:] c= [: NAT , ( QC-symbols Al):] & Al = [: NAT , ( QC-symbols Al):] by QC_LANG1: 5, ZFMISC_1: 96;

        then

        reconsider Al as Al2 -expanding QC-alphabet by Def1, A28, XBOOLE_1: 8;

        consider r2 be Element of ( CQC-WFF Al1) such that

         A29: r = r2 by A25;

        reconsider r2 as Element of ( CQC-WFF Al2) by Th7;

        

         A30: x = [4, s2] by A26, TARSKI:def 1;

        Al2 = [: NAT , ( QC-symbols Al2):] by QC_LANG1: 5;

        then ( QC-symbols Al2) = (( QC-symbols Al1) \/ {s2}) & s2 in {s2} by TARSKI:def 1, ZFMISC_1: 110;

        then s2 in ( QC-symbols Al2) by XBOOLE_0:def 3;

        then x is bound_QC-variable of Al2 by A30, ZFMISC_1: 105;

        then

        consider x2 be bound_QC-variable of Al2 such that

         A31: x = x2;

        ( All (x2,r2)) = ( All (x,r)) by A29, A31;

        then ( All (x,r)) is Element of ( CQC-WFF Al2) & Al is Al2 -expanding;

        hence thesis;

      end;

      then

       A32: for r, s, x, k, l, P 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, A15, A19;

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

      hence thesis;

    end;

    theorem :: QC_TRANS:20

    

     Th20: for PHI be finite Subset of ( CQC-WFF Al) holds ex Al1 be countable QC-alphabet st PHI is finite Subset of ( CQC-WFF Al1) & Al is Al1 -expanding

    proof

      let PHI be finite Subset of ( CQC-WFF Al);

      defpred P[ set] means $1 is finite Subset of ( CQC-WFF Al) implies ex Al1 be countable QC-alphabet st $1 is finite Subset of ( CQC-WFF Al1) & Al is Al1 -expanding;

      

       A1: PHI is finite;

      

       A2: P[ {} ]

      proof

        set Al1 = [: NAT , NAT :];

        reconsider Al1 as countable QC-alphabet by QC_LANG1:def 1, CARD_4: 7;

        Al = [: NAT , ( QC-symbols Al):] & NAT c= ( QC-symbols Al) by QC_LANG1: 3, QC_LANG1: 5;

        then Al is Al1 -expanding & {} is finite Subset of ( CQC-WFF Al1) by XBOOLE_1: 2, ZFMISC_1: 96;

        hence thesis;

      end;

      

       A3: for x,B be set st x in PHI & B c= PHI & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that

         A4: x in PHI & B c= PHI & P[B];

        reconsider x as Element of ( CQC-WFF Al) by A4;

        reconsider B as finite Subset of ( CQC-WFF Al) by A4, XBOOLE_1: 1;

        consider Al1 be countable QC-alphabet such that

         A5: x is Element of ( CQC-WFF Al1) & Al is Al1 -expanding by Th19;

        consider Al2 be countable QC-alphabet such that

         A6: B is finite Subset of ( CQC-WFF Al2) & Al is Al2 -expanding by A4;

        set Al3 = (Al1 \/ Al2);

        Al1 = [: NAT , ( QC-symbols Al1):] & Al2 = [: NAT , ( QC-symbols Al2):] by QC_LANG1: 5;

        then

         A7: Al3 = [: NAT , (( QC-symbols Al1) \/ ( QC-symbols Al2)):] by ZFMISC_1: 97;

         NAT c= (( QC-symbols Al1) \/ ( QC-symbols Al2)) by QC_LANG1: 3, XBOOLE_1: 10;

        then

        reconsider Al3 as QC-alphabet by A7, QC_LANG1:def 1;

        reconsider Al3 as countableAl1 -expandingAl2 -expanding QC-alphabet by Def1, CARD_2: 85, XBOOLE_1: 7;

        consider x2 be Element of ( CQC-WFF Al1) such that

         A8: x = x2 by A5;

        for s be object st s in B holds s in ( CQC-WFF Al3)

        proof

          let s be object such that

           A9: s in B;

          consider s2 be Element of ( CQC-WFF Al2) such that

           A10: s = s2 by A6, A9;

          s2 is Element of ( CQC-WFF Al3) by Th7;

          hence s in ( CQC-WFF Al3) by A10;

        end;

        then x2 is Element of ( CQC-WFF Al3) & B c= ( CQC-WFF Al3) by Th7;

        then {x2} c= ( CQC-WFF Al3) & B c= ( CQC-WFF Al3) by ZFMISC_1: 31;

        then

         A11: (B \/ {x}) c= ( CQC-WFF Al3) by A8, XBOOLE_1: 8;

        Al1 c= Al & Al2 c= Al by A5, A6;

        then Al is Al3 -expanding QC-alphabet by Def1, XBOOLE_1: 8;

        hence thesis by A11;

      end;

       P[PHI] from FINSET_1:sch 2( A1, A2, A3);

      hence thesis;

    end;

    registration

      let Al;

      let PHI be finite Subset of ( CQC-WFF Al);

      cluster ( still_not-bound_in PHI) -> finite;

      coherence

      proof

        deffunc snb( Element of ( CQC-WFF Al)) = ( still_not-bound_in $1);

        

         A1: for x be set st x in { snb(p) : p in PHI } holds x is finite

        proof

          let x be set such that

           A2: x in { ( still_not-bound_in p) : p in PHI };

          ex p st x = ( still_not-bound_in p) & p in PHI by A2;

          hence x is finite by CQC_SIM1: 19;

        end;

        

         A3: PHI is finite;

        { snb(p) : p in PHI } is finite from FRAENKEL:sch 21( A3);

        then ( union { snb(p) : p in PHI }) is finite by A1, FINSET_1: 7;

        hence ( still_not-bound_in PHI) is finite by GOEDELCP:def 8;

      end;

    end

    theorem :: QC_TRANS:21

    

     Th21: for THETA be Subset of ( CQC-WFF Al2) st PHI = THETA holds for A, J, v st (J,v) |= PHI holds ex A2 be non empty set, J2 be interpretation of Al2, A2, v2 be Element of ( Valuations_in (Al2,A2)) st (J2,v2) |= THETA

    proof

      let THETA be Subset of ( CQC-WFF Al2) such that

       A1: PHI = THETA;

      let A, J, v such that

       A2: (J,v) |= PHI;

      set J2 = ((( QC-pred_symbols Al2) --> ( empty_rel A)) +* J);

      

       A3: ( dom J) = ( QC-pred_symbols Al) & ( dom (( QC-pred_symbols Al2) --> ( empty_rel A))) = ( QC-pred_symbols Al2) by FUNCT_2:def 1;

      then ( dom J2) = (( QC-pred_symbols Al) \/ ( QC-pred_symbols Al2)) by FUNCT_4:def 1;

      then

       A4: ( dom J2) = ( QC-pred_symbols Al2) by Th3, XBOOLE_1: 12;

      J in ( Funcs (( QC-pred_symbols Al),( relations_on A))) by FUNCT_2: 8;

      then ( rng J) c= ( relations_on A) by FUNCT_2: 92;

      then (( rng (( QC-pred_symbols Al2) --> ( empty_rel A))) \/ ( rng J)) c= ( relations_on A) & ( rng J2) c= (( rng (( QC-pred_symbols Al2) --> ( empty_rel A))) \/ ( rng J)) by FUNCT_4: 17, XBOOLE_1: 8;

      then

      reconsider J2 as Function of ( QC-pred_symbols Al2), ( relations_on A) by A4, FUNCT_2: 2, XBOOLE_1: 1;

      

       A5: J = (J2 | ( QC-pred_symbols Al)) by A3, FUNCT_4: 23;

      for P2 be Element of ( QC-pred_symbols Al2), r be Element of ( relations_on A) st (J2 . P2) = r holds r = ( empty_rel A) or ( the_arity_of P2) = ( the_arity_of r)

      proof

        let P2 be Element of ( QC-pred_symbols Al2), r be Element of ( relations_on A) such that

         A6: (J2 . P2) = r;

        per cases ;

          suppose P2 in ( QC-pred_symbols Al);

          then

          consider P be QC-pred_symbol of Al such that

           A7: P = P2;

          

           A8: (J . P) = r by A3, A6, A7, FUNCT_4: 13;

          (7 + ( the_arity_of P2)) = (P `1 ) by A7, QC_LANG1:def 8

          .= (7 + ( the_arity_of P)) by QC_LANG1:def 8;

          hence thesis by A8, VALUAT_1:def 5;

        end;

          suppose not P2 in ( QC-pred_symbols Al);

          then not P2 in ( dom J) by FUNCT_2:def 1;

          

          then (J2 . P2) = ((( QC-pred_symbols Al2) --> ( empty_rel A)) . P2) by FUNCT_4: 11

          .= ( empty_rel A);

          hence thesis by A6;

        end;

      end;

      then

      reconsider J2 as interpretation of Al2, A by VALUAT_1:def 5;

      set a = the Element of A;

      set v2 = ((( bound_QC-variables Al2) --> a) +* v);

      v in ( Valuations_in (Al,A));

      then v in ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

      then

       A9: ( dom v) = ( bound_QC-variables Al) & ( dom (( bound_QC-variables Al2) --> a)) = ( bound_QC-variables Al2) by FUNCT_2: 92;

      then ( dom v2) = (( bound_QC-variables Al) \/ ( bound_QC-variables Al2)) by FUNCT_4:def 1;

      then

       A10: ( dom v2) = ( bound_QC-variables Al2) by Th4, XBOOLE_1: 12;

      v in ( Valuations_in (Al,A));

      then v in ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

      then ( rng v) c= A by FUNCT_2: 92;

      then (( rng (( bound_QC-variables Al2) --> a)) \/ ( rng v)) c= A & ( rng v2) c= (( rng (( bound_QC-variables Al2) --> a)) \/ ( rng v)) by FUNCT_4: 17, XBOOLE_1: 8;

      then

      reconsider v2 as Function of ( bound_QC-variables Al2), A by A10, FUNCT_2: 2, XBOOLE_1: 1;

      

       A11: v = (v2 | ( bound_QC-variables Al)) by A9, FUNCT_4: 23;

      v2 in ( Funcs (( bound_QC-variables Al2),A)) by FUNCT_2: 8;

      then

      reconsider v2 as Element of ( Valuations_in (Al2,A)) by VALUAT_1:def 1;

      for p2 be Element of ( CQC-WFF Al2) st p2 in THETA holds (J2,v2) |= p2

      proof

        let p2 be Element of ( CQC-WFF Al2) such that

         A12: p2 in THETA;

        consider p such that

         A13: p = p2 & p in PHI by A1, A12;

        (J,v) |= p by A2, A13, CALCUL_1:def 11;

        then (J2,v2) |= (Al2 -Cast p) by A5, A11, Th9;

        hence thesis by A13;

      end;

      hence thesis by CALCUL_1:def 11;

    end;

    theorem :: QC_TRANS:22

    

     Th22: for CHI be Subset of ( CQC-WFF Al) st CHI c= PHI holds CHI is Consistent

    proof

      let CHI be Subset of ( CQC-WFF Al) such that

       A1: CHI c= PHI;

      assume CHI is Inconsistent;

      then ex f be FinSequence of ( CQC-WFF Al) st ( rng f) c= CHI & |- (f ^ <*( 'not' ( VERUM Al))*>) by HENMODEL:def 1, GOEDELCP: 24;

      then PHI |- ( 'not' ( VERUM Al)) by A1, HENMODEL:def 1, XBOOLE_1: 1;

      hence contradiction by GOEDELCP: 24;

    end;

    theorem :: QC_TRANS:23

    PHI is Al2 -Consistent

    proof

      let PSI be Subset of ( CQC-WFF Al2) such that

       A1: PHI = PSI;

      for CHI be Subset of ( CQC-WFF Al2) st CHI c= PSI & CHI is finite holds CHI is Consistent

      proof

        let CHI be Subset of ( CQC-WFF Al2) such that

         A2: CHI c= PSI & CHI is finite;

        reconsider CHI as finite Subset of ( CQC-WFF Al) by A1, A2, XBOOLE_1: 1;

        consider Al1 be countable QC-alphabet such that

         A3: CHI is finite Subset of ( CQC-WFF Al1) & Al is Al1 -expanding by Th20;

        reconsider Al as Al1 -expanding QC-alphabet by A3;

        reconsider CHI as finite Subset of ( CQC-WFF Al);

        reconsider PHI as Consistent Subset of ( CQC-WFF Al);

        reconsider CHI as Consistent Subset of ( CQC-WFF Al) by A1, A2, Th22;

        CHI is Al1 -Consistent by Th18;

        then

        reconsider CHI as Consistent Subset of ( CQC-WFF Al1) by A3;

        ( still_not-bound_in CHI) is finite;

        then

        consider CZ be Consistent Subset of ( CQC-WFF Al1), JH be Henkin_interpretation of CZ such that

         A4: (JH,( valH Al1)) |= CHI by GOEDELCP: 34;

        Al1 c= Al & Al c= Al2 by Def1;

        then

        reconsider Al2 as Al1 -expanding QC-alphabet by Def1, XBOOLE_1: 1;

        consider CHI2 be Subset of ( CQC-WFF Al2) such that

         A5: CHI = CHI2;

        ex A be non empty set, J2 be interpretation of Al2, A, v2 be Element of ( Valuations_in (Al2,A)) st (J2,v2) |= CHI2 by A4, A5, Th21;

        hence thesis by A5, HENMODEL: 12;

      end;

      hence thesis by HENMODEL: 7;

    end;