cqc_lang.miz

    begin

    reserve A for QC-alphabet;

    reserve i,j,k for Nat;



     Lm1: for x be bound_QC-variable of A holds not x in ( fixed_QC-variables A)

    proof

      let x be bound_QC-variable of A;

      x in ( bound_QC-variables A);

      then x in [: {4}, ( QC-symbols A):] by QC_LANG1:def 4;

      then

      consider x1,x2 be object such that

       A1: x1 in {4} and x2 in ( QC-symbols A) and

       A2: x = [x1, x2] by ZFMISC_1:def 2;



       A3: x1 = 4 by A1, TARSKI:def 1;

      assume x in ( fixed_QC-variables A);

      then x in [: {5}, ( QC-symbols A):] by QC_LANG1:def 5;

      then

      consider c1,c2 be object such that

       A4: c1 in {5} and c2 in ( QC-symbols A) and

       A5: x = [c1, c2] by ZFMISC_1:def 2;

      c1 = 5 by A4, TARSKI:def 1;

      hence contradiction by A2, A5, A3, XTUPLE_0: 1;

    end;

    theorem :: CQC_LANG:1



     Th1: for x be set holds x in ( QC-variables A) iff x in ( fixed_QC-variables A) or x in ( free_QC-variables A) or x in ( bound_QC-variables A)

    proof

      let x be set;

      thus x in ( QC-variables A) implies x in ( fixed_QC-variables A) or x in ( free_QC-variables A) or x in ( bound_QC-variables A)

      proof

        assume x in ( QC-variables A);

        then x in ( [: {6}, NAT :] \/ [: {4, 5}, ( QC-symbols A):]) by QC_LANG1:def 3;

        then x in [: {6}, NAT :] or x in [: {4, 5}, ( QC-symbols A):] by XBOOLE_0:def 3;

        then

        consider x1,x2 be object such that

         A1: (x1 in {6} & x2 in NAT & x = [x1, x2]) or (x1 in {4, 5} & x2 in ( QC-symbols A) & x = [x1, x2]) by ZFMISC_1:def 2;

        (x1 in {6} & x2 in NAT & x = [x1, x2]) or ((x1 = 4 or x1 = 5) & x2 in ( QC-symbols A) & x = [x1, x2]) by A1, TARSKI:def 2;

        then ((x1 in {4} & x2 in ( QC-symbols A)) or (x1 in {5} & x2 in ( QC-symbols A)) or (x1 in {6} & x2 in NAT )) & x = [x1, x2] by TARSKI:def 1;

        then x in [: {4}, ( QC-symbols A):] or x in [: {5}, ( QC-symbols A):] or x in [: {6}, NAT :] by ZFMISC_1:def 2;

        hence thesis by QC_LANG1:def 4, QC_LANG1:def 5, QC_LANG1:def 6;

      end;

      thus thesis;

    end;

    definition

      let A;

      mode Substitution of A is PartFunc of ( free_QC-variables A), ( QC-variables A);

    end

    reserve f for Substitution of A;

    definition

      let A;

      let l be FinSequence of ( QC-variables A);

      let f;

      :: CQC_LANG:def1

      func Subst (l,f) -> FinSequence of ( QC-variables A) means

      : Def1: ( len it ) = ( len l) & for k st 1 <= k & k <= ( len l) holds ((l . k) in ( dom f) implies (it . k) = (f . (l . k))) & ( not (l . k) in ( dom f) implies (it . k) = (l . k));

      existence

      proof

        defpred P[ set, object] means ((l . $1) in ( dom f) implies $2 = (f . (l . $1))) & ( not (l . $1) in ( dom f) implies $2 = (l . $1));



         A1: for k be Nat st k in ( Seg ( len l)) holds ex y be object st P[k, y]

        proof

          let k be Nat;

          assume k in ( Seg ( len l));

          (l . k) in ( dom f) implies thesis;

          hence thesis;

        end;

        consider s be FinSequence such that

         A2: ( dom s) = ( Seg ( len l)) and

         A3: for k be Nat st k in ( Seg ( len l)) holds P[k, (s . k)] from FINSEQ_1:sch 1( A1);

        ( rng s) c= ( QC-variables A)

        proof

          let y be object;

          assume y in ( rng s);

          then

          consider x be object such that

           A4: x in ( dom s) and

           A5: (s . x) = y by FUNCT_1:def 3;

          reconsider x as Nat by A4;

           A6:

          now

            per cases ;

              case (l . x) in ( dom f);

              hence (s . x) = (f . (l . x)) & (f . (l . x)) in ( QC-variables A) by A2, A3, A4, PARTFUN1: 4;

            end;

              case not (l . x) in ( dom f);

              hence (s . x) = (l . x) by A2, A3, A4;

            end;

          end;

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

          hence thesis by A2, A4, A5, A6, FINSEQ_2: 11;

        end;

        then

        reconsider s as FinSequence of ( QC-variables A) by FINSEQ_1:def 4;

        take s;

        thus ( len s) = ( len l) by A2, FINSEQ_1:def 3;

        let k;

        assume 1 <= k & k <= ( len l);

        then k in ( dom l) by FINSEQ_3: 25;

        then k in ( Seg ( len l)) by FINSEQ_1:def 3;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let l1,l2 be FinSequence of ( QC-variables A) such that

         A7: ( len l1) = ( len l) and

         A8: for k st 1 <= k & k <= ( len l) holds ((l . k) in ( dom f) implies (l1 . k) = (f . (l . k))) & ( not (l . k) in ( dom f) implies (l1 . k) = (l . k)) and

         A9: ( len l2) = ( len l) and

         A10: for k st 1 <= k & k <= ( len l) holds ((l . k) in ( dom f) implies (l2 . k) = (f . (l . k))) & ( not (l . k) in ( dom f) implies (l2 . k) = (l . k));

        now

          let k be Nat;

          assume

           A11: 1 <= k & k <= ( len l);



           A12: not (l . k) in ( dom f) implies (l1 . k) = (l . k) by A8, A11;

          (l . k) in ( dom f) implies (l1 . k) = (f . (l . k)) by A8, A11;

          hence (l1 . k) = (l2 . k) by A10, A11, A12;

        end;

        hence thesis by A7, A9, FINSEQ_1: 14;

      end;

    end

    registration

      let A, k;

      let l be QC-variable_list of k, A;

      let f;

      cluster ( Subst (l,f)) -> k -element;

      coherence

      proof

        ( len ( Subst (l,f))) = ( len l) & ( len l) = k by Def1, CARD_1:def 7;

        hence thesis by CARD_1:def 7;

      end;

    end

    theorem :: CQC_LANG:2



     Th2: for x be bound_QC-variable of A, a be free_QC-variable of A holds (a .--> x) is Substitution of A

    proof

      let x be bound_QC-variable of A;

      let a be free_QC-variable of A;

      set f = (a .--> x);

      ( rng f) = {x} by FUNCOP_1: 8;

      then

       A1: ( rng f) c= ( QC-variables A) by ZFMISC_1: 31;

      ( dom f) c= ( free_QC-variables A) by ZFMISC_1: 31;

      hence thesis by A1, RELSET_1: 4;

    end;

    definition

      let A;

      let a be free_QC-variable of A, x be bound_QC-variable of A;

      :: original: .-->

      redefine

      func a .--> x -> Substitution of A ;

      coherence by Th2;

    end

    theorem :: CQC_LANG:3



     Th3: for x be bound_QC-variable of A, a be free_QC-variable of A, l,ll be FinSequence of ( QC-variables A) holds f = (a .--> x) & ll = ( Subst (l,f)) & 1 <= k & k <= ( len l) implies ((l . k) = a implies (ll . k) = x) & ((l . k) <> a implies (ll . k) = (l . k))

    proof

      let x be bound_QC-variable of A, a be free_QC-variable of A, l,ll be FinSequence of ( QC-variables A);

      set f9 = (a .--> x);

      assume

       A1: f = (a .--> x) & ll = ( Subst (l,f)) & 1 <= k & k <= ( len l);

      thus (l . k) = a implies (ll . k) = x

      proof



         A2: (f9 . a) = x by FUNCOP_1: 72;

        assume

         A3: (l . k) = a;

        then (l . k) in {a} by TARSKI:def 1;

        then (l . k) in ( dom f9);

        hence thesis by A1, A3, A2, Def1;

      end;

      assume (l . k) <> a;

      then not (l . k) in {a} by TARSKI:def 1;

      then not (l . k) in ( dom f9);

      hence thesis by A1, Def1;

    end;

    definition

      let A;

      :: CQC_LANG:def2

      func CQC-WFF (A) -> Subset of ( QC-WFF A) equals { s where s be QC-formula of A : ( Fixed s) = {} & ( Free s) = {} };

      coherence

      proof

        set F = { s where s be QC-formula of A : ( Fixed s) = {} & ( Free s) = {} };

        F c= ( QC-WFF A)

        proof

          let x be object;

          assume x in F;

          then ex s be QC-formula of A st s = x & ( Fixed s) = {} & ( Free s) = {} ;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let A;

      cluster ( CQC-WFF A) -> non empty;

      coherence

      proof

        ( Fixed ( VERUM A)) = {} & ( Free ( VERUM A)) = {} by QC_LANG3: 53, QC_LANG3: 63;

        then ( VERUM A) in { s where s be QC-formula of A : ( Fixed s) = {} & ( Free s) = {} };

        hence thesis;

      end;

    end

    theorem :: CQC_LANG:4



     Th4: for p be Element of ( QC-WFF A) holds p is Element of ( CQC-WFF A) iff ( Fixed p) = {} & ( Free p) = {}

    proof

      let p be Element of ( QC-WFF A);

      thus p is Element of ( CQC-WFF A) implies ( Fixed p) = {} & ( Free p) = {}

      proof

        assume p is Element of ( CQC-WFF A);

        then p in ( CQC-WFF A);

        then ex s be QC-formula of A st s = p & ( Fixed s) = {} & ( Free s) = {} ;

        hence thesis;

      end;

      assume ( Fixed p) = {} & ( Free p) = {} ;

      then p in ( CQC-WFF A);

      hence thesis;

    end;

    registration

      let A;

      let k be Nat;

      cluster ( bound_QC-variables A) -valued for QC-variable_list of k, A;

      existence

      proof

        set null = 0 ;

        reconsider null as QC-symbol of A by QC_LANG1: 3;

        set l = (k |-> ( x. null));

        ( rng l) c= ( QC-variables A)

        proof

          let y be object;

          assume y in ( rng l);

          then

          consider x be object such that

           A2: x in ( dom l) and

           A3: (l . x) = y by FUNCT_1:def 3;

          y = ( x. null) by A2, A3, FINSEQ_2: 57;

          hence thesis;

        end;

        then

        reconsider l as QC-variable_list of k, A by FINSEQ_1:def 4;

        take l;

        let x be object;

        assume x in ( rng l);

        then

        consider i be object such that

         A4: i in ( dom l) and

         A5: x = (l . i) by FUNCT_1:def 3;

        reconsider i as Nat by A4;

        (l . i) = ( x. null) by A4, FINSEQ_2: 57;

        hence thesis by A5;

      end;

    end

    definition

      let A;

      let k be Nat;

      mode CQC-variable_list of k,A is ( bound_QC-variables A) -valued QC-variable_list of k, A;

    end

    theorem :: CQC_LANG:5



     Th5: for l be QC-variable_list of k, A holds l is CQC-variable_list of k, A iff { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( free_QC-variables A) } = {} & { (l . j) : 1 <= j & j <= ( len l) & (l . j) in ( fixed_QC-variables A) } = {}

    proof

      let l be QC-variable_list of k, A;

      set FR = { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( free_QC-variables A) };

      set FI = { (l . j) : 1 <= j & j <= ( len l) & (l . j) in ( fixed_QC-variables A) };

      thus l is CQC-variable_list of k, A implies FR = {} & FI = {}

      proof

        assume l is CQC-variable_list of k, A;

        then

        reconsider l as CQC-variable_list of k, A;

        now

          set x = the Element of FR;

          assume FR <> {} ;

          then x in FR;

          then

          consider i such that x = (l . i) and

           A1: 1 <= i & i <= ( len l) and

           A2: (l . i) in ( free_QC-variables A);

          i in ( dom l) by A1, FINSEQ_3: 25;

          then ( rng l) c= ( bound_QC-variables A) & (l . i) in ( rng l) by FUNCT_1:def 3, RELAT_1:def 19;

          hence contradiction by A2, QC_LANG3: 34;

        end;

        hence FR = {} ;

        now

          set x = the Element of FI;

          assume FI <> {} ;

          then x in FI;

          then

          consider i such that x = (l . i) and

           A3: 1 <= i & i <= ( len l) and

           A4: (l . i) in ( fixed_QC-variables A);

          i in ( dom l) by A3, FINSEQ_3: 25;

          then ( rng l) c= ( bound_QC-variables A) & (l . i) in ( rng l) by FUNCT_1:def 3, RELAT_1:def 19;

          hence contradiction by A4, QC_LANG3: 33;

        end;

        hence thesis;

      end;

      assume that

       A5: FR = {} and

       A6: FI = {} ;

      l is ( bound_QC-variables A) -valued

      proof

        let x be object;



         A7: ( rng l) c= ( QC-variables A) by FINSEQ_1:def 4;

        assume x in ( rng l);

        then

        consider i be object such that

         A8: i in ( dom l) and

         A9: (l . i) = x by FUNCT_1:def 3;

        reconsider i as Nat by A8;



         A10: 1 <= i & i <= ( len l) by A8, FINSEQ_3: 25;

         A11:

        now

          assume x in ( fixed_QC-variables A);

          then x in FI by A9, A10;

          hence contradiction by A6;

        end;

         A12:

        now

          assume x in ( free_QC-variables A);

          then x in FR by A9, A10;

          hence contradiction by A5;

        end;

        (l . i) in ( rng l) by A8, FUNCT_1:def 3;

        hence thesis by A9, A7, A11, A12, Th1;

      end;

      hence thesis;

    end;

    theorem :: CQC_LANG:6



     Th6: ( VERUM A) is Element of ( CQC-WFF A)

    proof

      ( Fixed ( VERUM A)) = {} & ( Free ( VERUM A)) = {} by QC_LANG3: 53, QC_LANG3: 63;

      hence thesis by Th4;

    end;

    theorem :: CQC_LANG:7



     Th7: for P be QC-pred_symbol of k, A holds for l be QC-variable_list of k, A holds (P ! l) is Element of ( CQC-WFF A) iff { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( free_QC-variables A) } = {} & { (l . j) : 1 <= j & j <= ( len l) & (l . j) in ( fixed_QC-variables A) } = {}

    proof

      let P be QC-pred_symbol of k, A;

      let l be QC-variable_list of k, A;



       A1: ( Free (P ! l)) = { (l . j) : 1 <= j & j <= ( len l) & (l . j) in ( free_QC-variables A) } by QC_LANG3: 54;

      ( Fixed (P ! l)) = { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( fixed_QC-variables A) } by QC_LANG3: 64;

      hence thesis by A1, Th4;

    end;

    definition

      let k, A;

      let P be QC-pred_symbol of k, A;

      let l be CQC-variable_list of k, A;

      :: original: !

      redefine

      func P ! l -> Element of ( CQC-WFF A) ;

      coherence

      proof



         A1: { (l . j) : 1 <= j & j <= ( len l) & (l . j) in ( fixed_QC-variables A) } = {} by Th5;

        { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( free_QC-variables A) } = {} by Th5;

        hence thesis by A1, Th7;

      end;

    end

    theorem :: CQC_LANG:8



     Th8: for p be Element of ( QC-WFF A) holds ( 'not' p) is Element of ( CQC-WFF A) iff p is Element of ( CQC-WFF A)

    proof

      let p be Element of ( QC-WFF A);

      thus ( 'not' p) is Element of ( CQC-WFF A) implies p is Element of ( CQC-WFF A)

      proof

        assume

         A1: ( 'not' p) is Element of ( CQC-WFF A);

        then ( Free ( 'not' p)) = {} by Th4;

        then

         A2: ( Free p) = {} by QC_LANG3: 55;

        ( Fixed ( 'not' p)) = {} by A1, Th4;

        then ( Fixed p) = {} by QC_LANG3: 65;

        hence thesis by A2, Th4;

      end;

      assume p is Element of ( CQC-WFF A);

      then

      reconsider r = p as Element of ( CQC-WFF A);

      ( Fixed r) = {} by Th4;

      then

       A3: ( Fixed ( 'not' r)) = {} by QC_LANG3: 65;

      ( Free r) = {} by Th4;

      then ( Free ( 'not' r)) = {} by QC_LANG3: 55;

      hence thesis by A3, Th4;

    end;

    theorem :: CQC_LANG:9



     Th9: for p,q be Element of ( QC-WFF A) holds (p '&' q) is Element of ( CQC-WFF A) iff p is Element of ( CQC-WFF A) & q is Element of ( CQC-WFF A)

    proof

      let p,q be Element of ( QC-WFF A);

      thus (p '&' q) is Element of ( CQC-WFF A) implies p is Element of ( CQC-WFF A) & q is Element of ( CQC-WFF A)

      proof

        assume

         A1: (p '&' q) is Element of ( CQC-WFF A);

        then ( Fixed (p '&' q)) = {} by Th4;

        then

         A2: (( Fixed p) \/ ( Fixed q)) = {} by QC_LANG3: 67;

        then

         A3: ( Fixed p) = {} ;

        ( Free (p '&' q)) = {} by A1, Th4;

        then

         A4: (( Free p) \/ ( Free q)) = {} by QC_LANG3: 57;

        then ( Free p) = {} ;

        hence thesis by A4, A2, A3, Th4;

      end;

      assume p is Element of ( CQC-WFF A) & q is Element of ( CQC-WFF A);

      then

      reconsider r = p, s = q as Element of ( CQC-WFF A);

      ( Fixed r) = {} by Th4;

      then (( Fixed r) \/ ( Fixed s)) = {} by Th4;

      then

       A5: ( Fixed (r '&' s)) = {} by QC_LANG3: 67;

      ( Free r) = {} by Th4;

      then (( Free r) \/ ( Free s)) = {} by Th4;

      then ( Free (r '&' s)) = {} by QC_LANG3: 57;

      hence thesis by A5, Th4;

    end;

    definition

      let A;

      :: original: VERUM

      redefine

      func VERUM (A) -> Element of ( CQC-WFF A) ;

      coherence by Th6;

      let r be Element of ( CQC-WFF A);

      :: original: 'not'

      redefine

      func 'not' r -> Element of ( CQC-WFF A) ;

      coherence by Th8;

      let s be Element of ( CQC-WFF A);

      :: original: '&'

      redefine

      func r '&' s -> Element of ( CQC-WFF A) ;

      coherence by Th9;

    end

    theorem :: CQC_LANG:10



     Th10: for r,s be Element of ( CQC-WFF A) holds (r => s) is Element of ( CQC-WFF A)

    proof

      let r,s be Element of ( CQC-WFF A);

      (r => s) = ( 'not' (r '&' ( 'not' s))) by QC_LANG2:def 2;

      hence thesis;

    end;

    theorem :: CQC_LANG:11



     Th11: for r,s be Element of ( CQC-WFF A) holds (r 'or' s) is Element of ( CQC-WFF A)

    proof

      let r,s be Element of ( CQC-WFF A);

      (r 'or' s) = ( 'not' (( 'not' r) '&' ( 'not' s))) by QC_LANG2:def 3;

      hence thesis;

    end;

    theorem :: CQC_LANG:12



     Th12: for r,s be Element of ( CQC-WFF A) holds (r <=> s) is Element of ( CQC-WFF A)

    proof

      let r,s be Element of ( CQC-WFF A);

      (r <=> s) = ((r => s) '&' (s => r)) by QC_LANG2:def 4

      .= (( 'not' (r '&' ( 'not' s))) '&' (s => r)) by QC_LANG2:def 2

      .= (( 'not' (r '&' ( 'not' s))) '&' ( 'not' (s '&' ( 'not' r)))) by QC_LANG2:def 2;

      hence thesis;

    end;

    definition

      let A;

      let r,s be Element of ( CQC-WFF A);

      :: original: =>

      redefine

      func r => s -> Element of ( CQC-WFF A) ;

      coherence by Th10;

      :: original: 'or'

      redefine

      func r 'or' s -> Element of ( CQC-WFF A) ;

      coherence by Th11;

      :: original: <=>

      redefine

      func r <=> s -> Element of ( CQC-WFF A) ;

      coherence by Th12;

    end

    theorem :: CQC_LANG:13



     Th13: for x be bound_QC-variable of A, p be Element of ( QC-WFF A) holds ( All (x,p)) is Element of ( CQC-WFF A) iff p is Element of ( CQC-WFF A)

    proof

      let x be bound_QC-variable of A, p be Element of ( QC-WFF A);

      thus ( All (x,p)) is Element of ( CQC-WFF A) implies p is Element of ( CQC-WFF A)

      proof

        assume

         A1: ( All (x,p)) is Element of ( CQC-WFF A);

        then ( Fixed ( All (x,p))) = {} by Th4;

        then

         A2: ( Fixed p) = {} by QC_LANG3: 68;

        ( Free ( All (x,p))) = {} by A1, Th4;

        then ( Free p) = {} by QC_LANG3: 58;

        hence thesis by A2, Th4;

      end;

      assume

       A3: p is Element of ( CQC-WFF A);

      then ( Fixed p) = {} by Th4;

      then

       A4: ( Fixed ( All (x,p))) = {} by QC_LANG3: 68;

      ( Free p) = {} by A3, Th4;

      then ( Free ( All (x,p))) = {} by QC_LANG3: 58;

      hence thesis by A4, Th4;

    end;

    definition

      let A;

      let x be bound_QC-variable of A, r be Element of ( CQC-WFF A);

      :: original: All

      redefine

      func All (x,r) -> Element of ( CQC-WFF A) ;

      coherence by Th13;

    end

    theorem :: CQC_LANG:14



     Th14: for x be bound_QC-variable of A, r be Element of ( CQC-WFF A) holds ( Ex (x,r)) is Element of ( CQC-WFF A)

    proof

      let x be bound_QC-variable of A, r be Element of ( CQC-WFF A);

      ( Ex (x,r)) = ( 'not' ( All (x,( 'not' r)))) by QC_LANG2:def 5;

      hence thesis;

    end;

    definition

      let A;

      let x be bound_QC-variable of A, r be Element of ( CQC-WFF A);

      :: original: Ex

      redefine

      func Ex (x,r) -> Element of ( CQC-WFF A) ;

      coherence by Th14;

    end

    scheme :: CQC_LANG:sch1

    CQCInd { A() -> QC-alphabet , P[ set] } :

for r be Element of ( CQC-WFF A()) holds P[r]

      provided

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

      defpred Prop[ Element of ( QC-WFF A())] means $1 is Element of ( CQC-WFF A()) implies P[$1];



       A2: for p be Element of ( QC-WFF A()) st Prop[p] holds Prop[( 'not' p)]

      proof

        let p be Element of ( QC-WFF A());

        assume

         A3: Prop[p];

        assume ( 'not' p) is Element of ( CQC-WFF A());

        then p is Element of ( CQC-WFF A()) by Th8;

        hence thesis by A1, A3;

      end;



       A4: for p,q be Element of ( QC-WFF A()) st Prop[p] & Prop[q] holds Prop[(p '&' q)]

      proof

        let p,q be Element of ( QC-WFF A());

        assume

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

        assume (p '&' q) is Element of ( CQC-WFF A());

        then p is Element of ( CQC-WFF A()) & q is Element of ( CQC-WFF A()) by Th9;

        hence thesis by A1, A5;

      end;



       A6: for k be Nat, P be QC-pred_symbol of k, A(), l be QC-variable_list of k, A() holds Prop[(P ! l)]

      proof

        let k be Nat, P be QC-pred_symbol of k, A(), l be QC-variable_list of k, A();

        assume

         A7: (P ! l) is Element of ( CQC-WFF A());

        reconsider k as Nat;

        reconsider l as QC-variable_list of k, A();



         A8: { (l . j) : 1 <= j & j <= ( len l) & (l . j) in ( fixed_QC-variables A()) } = {} by Th7, A7;

        { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( free_QC-variables A()) } = {} by A7, Th7;

        then l is CQC-variable_list of k, A() by A8, Th5;

        hence thesis by A1;

      end;



       A9: for x be bound_QC-variable of A(), p be Element of ( QC-WFF A()) st Prop[p] holds Prop[( All (x,p))]

      proof

        let x be bound_QC-variable of A(), p be Element of ( QC-WFF A());

        assume

         A10: Prop[p];

        assume ( All (x,p)) is Element of ( CQC-WFF A());

        then p is Element of ( CQC-WFF A()) by Th13;

        hence thesis by A1, A10;

      end;



       A11: Prop[( VERUM A())] by A1;

      for p be Element of ( QC-WFF A()) holds Prop[p] from QC_LANG1:sch 1( A6, A11, A2, A4, A9);

      hence thesis;

    end;

    scheme :: CQC_LANG:sch2

    CQCFuncEx { Al() -> QC-alphabet , D() -> non empty set , V() -> Element of D() , A( set, set, set) -> Element of D() , N( set) -> Element of D() , C( set, set) -> Element of D() , Q( set, set) -> Element of D() } :

ex F be Function of ( CQC-WFF Al()), D() st (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.);

      deffunc q( Element of ( QC-WFF Al()), Element of D()) = Q(bound_in,$2);

      deffunc a( Element of ( QC-WFF Al())) = A(the_arity_of,the_pred_symbol_of,the_arguments_of);

      consider F be Function of ( QC-WFF Al()), D() such that

       A1: (F . ( VERUM Al())) = V() & for p be Element of ( QC-WFF Al()) holds (p is atomic implies (F . p) = a(p)) & (p is negative implies (F . p) = N(.)) & (p is conjunctive implies (F . p) = C(.,.)) & (p is universal implies (F . p) = q(p,.)) from QC_LANG1:sch 3;

      reconsider G = (F | ( CQC-WFF Al())) as Function of ( CQC-WFF Al()), D() by FUNCT_2: 32;

      take G;

      thus (G . ( VERUM Al())) = V() by A1, FUNCT_1: 49;

      let r,s be Element of ( CQC-WFF Al());

      let x be bound_QC-variable of Al();

      let k;

      let l be CQC-variable_list of k, Al();

      let P be QC-pred_symbol of k, Al();



       A2: ( the_arity_of P) = k by QC_LANG1: 11;



       A3: (P ! l) is atomic by QC_LANG1:def 18;

      then

       A4: ( the_arguments_of (P ! l)) = l & ( the_pred_symbol_of (P ! l)) = P by QC_LANG1:def 22, QC_LANG1:def 23;



      thus (G . (P ! l)) = (F . (P ! l)) by FUNCT_1: 49

      .= A(k,P,l) by A1, A3, A4, A2;

      set r9 = (G . r), s9 = (G . s);



       A5: r9 = (F . r) by FUNCT_1: 49;



       A6: (r '&' s) is conjunctive by QC_LANG1:def 20;

      then

       A7: ( the_left_argument_of (r '&' s)) = r & ( the_right_argument_of (r '&' s)) = s by QC_LANG1:def 25, QC_LANG1:def 26;



       A8: ( 'not' r) is negative by QC_LANG1:def 19;

      then

       A9: ( the_argument_of ( 'not' r)) = r by QC_LANG1:def 24;



      thus (G . ( 'not' r)) = (F . ( 'not' r)) by FUNCT_1: 49

      .= N(r9) by A1, A5, A8, A9;



       A10: s9 = (F . s) by FUNCT_1: 49;



      thus (G . (r '&' s)) = (F . (r '&' s)) by FUNCT_1: 49

      .= C(r9,s9) by A1, A5, A10, A6, A7;



       A11: ( All (x,r)) is universal by QC_LANG1:def 21;

      then

       A12: ( bound_in ( All (x,r))) = x & ( the_scope_of ( All (x,r))) = r by QC_LANG1:def 27, QC_LANG1:def 28;



      thus (G . ( All (x,r))) = (F . ( All (x,r))) by FUNCT_1: 49

      .= Q(x,r9) by A1, A5, A11, A12;

    end;

    scheme :: CQC_LANG:sch3

    CQCFuncUniq { Al() -> QC-alphabet , D() -> non empty set , F1() -> Function of ( CQC-WFF Al()), D() , F2() -> Function of ( CQC-WFF Al()), D() , V() -> Element of D() , A( set, set, set) -> Element of D() , N( set) -> Element of D() , C( set, set) -> Element of D() , Q( set, set) -> Element of D() } :

F1() = F2()

      provided

       A1: (F1() . ( VERUM Al())) = V() & 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 (F1() . (P ! l)) = A(k,P,l) & (F1() . ( 'not' r)) = N(.) & (F1() . (r '&' s)) = C(.,.) & (F1() . ( All (x,r))) = Q(x,.)

       and

       A2: (F2() . ( VERUM Al())) = V() & 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 (F2() . (P ! l)) = A(k,P,l) & (F2() . ( 'not' r)) = N(.) & (F2() . (r '&' s)) = C(.,.) & (F2() . ( All (x,r))) = Q(x,.);

      defpred P[ set] means (F1() . $1) = (F2() . $1);



       A3: 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))])

      proof

        let r,s be Element of ( CQC-WFF Al());

        let x be bound_QC-variable of Al();

        let k;

        let l be CQC-variable_list of k, Al();

        let P be QC-pred_symbol of k, Al();

        thus (F1() . ( VERUM Al())) = (F2() . ( VERUM Al())) by A1, A2;

        (F1() . (P ! l)) = A(k,P,l) by A1;

        hence (F1() . (P ! l)) = (F2() . (P ! l)) by A2;

        (F1() . ( 'not' r)) = N(.) by A1;

        hence (F1() . r) = (F2() . r) implies (F1() . ( 'not' r)) = (F2() . ( 'not' r)) by A2;

        (F1() . (r '&' s)) = C(.,.) by A1;

        hence (F1() . r) = (F2() . r) & (F1() . s) = (F2() . s) implies (F1() . (r '&' s)) = (F2() . (r '&' s)) by A2;

        (F1() . ( All (x,r))) = Q(x,.) by A1;

        hence thesis by A2;

      end;

      for r be Element of ( CQC-WFF Al()) holds P[r] from CQCInd( A3);

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: CQC_LANG:sch4

    CQCDefcorrectness { Al() -> QC-alphabet , D() -> non empty set , p() -> Element of ( CQC-WFF Al()) , V() -> Element of D() , A( set, set, set) -> Element of D() , N( set) -> Element of D() , C( set, set) -> Element of D() , Q( set, set) -> Element of D() } :

(ex d be Element of D() st ex F be Function of ( CQC-WFF Al()), D() st d = (F . p()) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.)) & for d1,d2 be Element of D() st (ex F be Function of ( CQC-WFF Al()), D() st d1 = (F . p()) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.)) & (ex F be Function of ( CQC-WFF Al()), D() st d2 = (F . p()) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.)) holds d1 = d2;

      thus ex d be Element of D() st ex F be Function of ( CQC-WFF Al()), D() st d = (F . p()) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.)

      proof

        consider F be Function of ( CQC-WFF Al()), D() such that

         A1: (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.) from CQCFuncEx;

        take (F . p()), F;

        thus thesis by A1;

      end;

      let d1,d2 be Element of D();

      given F1 be Function of ( CQC-WFF Al()), D() such that

       A2: d1 = (F1 . p()) and

       A3: (F1 . ( VERUM Al())) = V() & 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 (F1 . (P ! l)) = A(k,P,l) & (F1 . ( 'not' r)) = N(.) & (F1 . (r '&' s)) = C(.,.) & (F1 . ( All (x,r))) = Q(x,.);

      given F2 be Function of ( CQC-WFF Al()), D() such that

       A4: d2 = (F2 . p()) and

       A5: (F2 . ( VERUM Al())) = V() & 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 (F2 . (P ! l)) = A(k,P,l) & (F2 . ( 'not' r)) = N(.) & (F2 . (r '&' s)) = C(.,.) & (F2 . ( All (x,r))) = Q(x,.);

      F1 = F2 from CQCFuncUniq( A3, A5);

      hence thesis by A2, A4;

    end;

    scheme :: CQC_LANG:sch5

    CQCDefVERUM { Al() -> QC-alphabet , D() -> non empty set , F( set) -> Element of D() , V() -> Element of D() , A( set, set, set) -> Element of D() , N( set) -> Element of D() , C( set, set) -> Element of D() , Q( set, set) -> Element of D() } :

F(VERUM) = V()

      provided

       A1: for p be Element of ( CQC-WFF Al()), d be Element of D() holds d = F(p) iff ex F be Function of ( CQC-WFF Al()), D() st d = (F . p) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.);

      ex F be Function of ( CQC-WFF Al()), D() st (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.) from CQCFuncEx;

      hence thesis by A1;

    end;

    scheme :: CQC_LANG:sch6

    CQCDefatomic { Al() -> QC-alphabet , D() -> non empty set , V() -> Element of D() , F( set) -> Element of D() , A( set, set, set) -> Element of D() , k() -> Nat , P() -> QC-pred_symbol of k(), Al() , l() -> CQC-variable_list of k(), Al() , N( set) -> Element of D() , C( set, set) -> Element of D() , Q( set, set) -> Element of D() } :

F(!) = A(k,P,l)

      provided

       A1: for p be Element of ( CQC-WFF Al()), d be Element of D() holds d = F(p) iff ex F be Function of ( CQC-WFF Al()), D() st d = (F . p) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.);

      consider F be Function of ( CQC-WFF Al()), D() such that

       A2: (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.) from CQCFuncEx;

      A(k,P,l) = (F . (P() ! l())) by A2;

      hence thesis by A1, A2;

    end;

    scheme :: CQC_LANG:sch7

    CQCDefnegative { Al() -> QC-alphabet , D() -> non empty set , F( set) -> Element of D() , V() -> Element of D() , A( set, set, set) -> Element of D() , N( set) -> Element of D() , r() -> Element of ( CQC-WFF Al()) , C( set, set) -> Element of D() , Q( set, set) -> Element of D() } :

F('not') = N(F)

      provided

       A1: for p be Element of ( CQC-WFF Al()), d be Element of D() holds d = F(p) iff ex F be Function of ( CQC-WFF Al()), D() st d = (F . p) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.);

      consider G be Function of ( CQC-WFF Al()), D() such that

       A2: F(r) = (G . r()) and

       A3: (G . ( VERUM Al())) = V() & 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 (G . (P ! l)) = A(k,P,l) & (G . ( 'not' r)) = N(.) & (G . (r '&' s)) = C(.,.) & (G . ( All (x,r))) = Q(x,.) by A1;

      consider F be Function of ( CQC-WFF Al()), D() such that

       A4: (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.) from CQCFuncEx;



       A5: (F . ( 'not' r())) = N(.) by A4;

      F = G from CQCFuncUniq( A4, A3);

      hence thesis by A1, A4, A5, A2;

    end;

    scheme :: CQC_LANG:sch8

    QCDefconjunctive { Al() -> QC-alphabet , D() -> non empty set , F( set) -> Element of D() , V() -> Element of D() , A( set, set, set) -> Element of D() , N( set) -> Element of D() , C( set, set) -> Element of D() , r() -> Element of ( CQC-WFF Al()) , s() -> Element of ( CQC-WFF Al()) , Q( set, set) -> Element of D() } :

F('&') = C(F,F)

      provided

       A1: for p be Element of ( CQC-WFF Al()), d be Element of D() holds d = F(p) iff ex F be Function of ( CQC-WFF Al()), D() st d = (F . p) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.);

      consider F2 be Function of ( CQC-WFF Al()), D() such that

       A2: F(s) = (F2 . s()) and

       A3: (F2 . ( VERUM Al())) = V() & 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 (F2 . (P ! l)) = A(k,P,l) & (F2 . ( 'not' r)) = N(.) & (F2 . (r '&' s)) = C(.,.) & (F2 . ( All (x,r))) = Q(x,.) by A1;

      consider F1 be Function of ( CQC-WFF Al()), D() such that

       A4: F(r) = (F1 . r()) and

       A5: (F1 . ( VERUM Al())) = V() & 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 (F1 . (P ! l)) = A(k,P,l) & (F1 . ( 'not' r)) = N(.) & (F1 . (r '&' s)) = C(.,.) & (F1 . ( All (x,r))) = Q(x,.) by A1;

      consider F be Function of ( CQC-WFF Al()), D() such that

       A6: (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.) from CQCFuncEx;



       A7: (F . (r() '&' s())) = C(.,.) by A6;



       A8: F = F2 from CQCFuncUniq( A6, A3);

      F = F1 from CQCFuncUniq( A6, A5);

      hence thesis by A1, A6, A7, A4, A2, A8;

    end;

    scheme :: CQC_LANG:sch9

    QCDefuniversal { Al() -> QC-alphabet , D() -> non empty set , F( set) -> Element of D() , V() -> Element of D() , A( set, set, set) -> Element of D() , N( set) -> Element of D() , C( set, set) -> Element of D() , Q( set, set) -> Element of D() , x() -> bound_QC-variable of Al() , r() -> Element of ( CQC-WFF Al()) } :

F(All) = Q(x,F)

      provided

       A1: for p be Element of ( CQC-WFF Al()), d be Element of D() holds d = F(p) iff ex F be Function of ( CQC-WFF Al()), D() st d = (F . p) & (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.);

      consider G be Function of ( CQC-WFF Al()), D() such that

       A2: F(r) = (G . r()) and

       A3: (G . ( VERUM Al())) = V() & 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 (G . (P ! l)) = A(k,P,l) & (G . ( 'not' r)) = N(.) & (G . (r '&' s)) = C(.,.) & (G . ( All (x,r))) = Q(x,.) by A1;

      consider F be Function of ( CQC-WFF Al()), D() such that

       A4: (F . ( VERUM Al())) = V() & 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 (F . (P ! l)) = A(k,P,l) & (F . ( 'not' r)) = N(.) & (F . (r '&' s)) = C(.,.) & (F . ( All (x,r))) = Q(x,.) from CQCFuncEx;



       A5: (F . ( All (x(),r()))) = Q(x,.) by A4;

      F = G from CQCFuncUniq( A4, A3);

      hence thesis by A1, A4, A5, A2;

    end;

    reserve x,y for bound_QC-variable of A;

    reserve a for free_QC-variable of A;

    reserve p,q for Element of ( QC-WFF A);

    reserve l,l1,l2,ll for FinSequence of ( QC-variables A);

    reserve r,s for Element of ( CQC-WFF A);



     Lm2: for F1,F2 be Function of ( QC-WFF A), ( QC-WFF A) st (for q holds (F1 . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F1 . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F1 . q) = ( 'not' (F1 . ( the_argument_of q)))) & (q is conjunctive implies (F1 . q) = ((F1 . ( the_left_argument_of q)) '&' (F1 . ( the_right_argument_of q)))) & (q is universal implies (F1 . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F1 . ( the_scope_of q)))))))) & (for q holds (F2 . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F2 . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F2 . q) = ( 'not' (F2 . ( the_argument_of q)))) & (q is conjunctive implies (F2 . q) = ((F2 . ( the_left_argument_of q)) '&' (F2 . ( the_right_argument_of q)))) & (q is universal implies (F2 . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F2 . ( the_scope_of q)))))))) holds F1 = F2

    proof

      deffunc c( Element of ( QC-WFF A), Element of ( QC-WFF A)) = ($1 '&' $2);

      deffunc n( Element of ( QC-WFF A)) = ( 'not' $1);

      let F1,F2 be Function of ( QC-WFF A), ( QC-WFF A);

      deffunc a( Element of ( QC-WFF A)) = (( the_pred_symbol_of $1) ! ( Subst (( the_arguments_of $1),((A a. 0 ) .--> x))));

      deffunc q( Element of ( QC-WFF A), Element of ( QC-WFF A)) = ( IFEQ (( bound_in $1),x,$1,( All (( bound_in $1),$2))));

      assume for q holds (F1 . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F1 . q) = a(q)) & (q is negative implies (F1 . q) = ( 'not' (F1 . ( the_argument_of q)))) & (q is conjunctive implies (F1 . q) = ((F1 . ( the_left_argument_of q)) '&' (F1 . ( the_right_argument_of q)))) & (q is universal implies (F1 . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F1 . ( the_scope_of q)))))));

      then

       A1: for p be Element of ( QC-WFF A) holds for d1,d2 be Element of ( QC-WFF A) holds (p = ( VERUM A) implies (F1 . p) = ( VERUM A)) & (p is atomic implies (F1 . p) = a(p)) & (p is negative & d1 = (F1 . ( the_argument_of p)) implies (F1 . p) = n(d1)) & (p is conjunctive & d1 = (F1 . ( the_left_argument_of p)) & d2 = (F1 . ( the_right_argument_of p)) implies (F1 . p) = c(d1,d2)) & (p is universal & d1 = (F1 . ( the_scope_of p)) implies (F1 . p) = q(p,d1));

      assume for q holds (F2 . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F2 . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F2 . q) = ( 'not' (F2 . ( the_argument_of q)))) & (q is conjunctive implies (F2 . q) = ((F2 . ( the_left_argument_of q)) '&' (F2 . ( the_right_argument_of q)))) & (q is universal implies (F2 . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F2 . ( the_scope_of q)))))));

      then

       A2: for p be Element of ( QC-WFF A) holds for d1,d2 be Element of ( QC-WFF A) holds (p = ( VERUM A) implies (F2 . p) = ( VERUM A)) & (p is atomic implies (F2 . p) = a(p)) & (p is negative & d1 = (F2 . ( the_argument_of p)) implies (F2 . p) = n(d1)) & (p is conjunctive & d1 = (F2 . ( the_left_argument_of p)) & d2 = (F2 . ( the_right_argument_of p)) implies (F2 . p) = c(d1,d2)) & (p is universal & d1 = (F2 . ( the_scope_of p)) implies (F2 . p) = q(p,d1));

      thus F1 = F2 from QC_LANG3:sch 1( A1, A2);

    end;

    definition

      let A, p, x;

      :: CQC_LANG:def3

      func p . x -> Element of ( QC-WFF A) means

      : Def3: ex F be Function of ( QC-WFF A), ( QC-WFF A) st it = (F . p) & for q holds (F . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F . q) = ( 'not' (F . ( the_argument_of q)))) & (q is conjunctive implies (F . q) = ((F . ( the_left_argument_of q)) '&' (F . ( the_right_argument_of q)))) & (q is universal implies (F . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F . ( the_scope_of q)))))));

      existence

      proof

        deffunc q( Element of ( QC-WFF A), Element of ( QC-WFF A)) = ( IFEQ (( bound_in $1),x,$1,( All (( bound_in $1),$2))));

        deffunc c( Element of ( QC-WFF A), Element of ( QC-WFF A)) = ($1 '&' $2);

        deffunc n( Element of ( QC-WFF A)) = ( 'not' $1);

        deffunc a( Element of ( QC-WFF A)) = (( the_pred_symbol_of $1) ! ( Subst (( the_arguments_of $1),((A a. 0 ) .--> x))));

        consider F be Function of ( QC-WFF A), ( QC-WFF A) such that

         A1: (F . ( VERUM A)) = ( VERUM A) & for p be Element of ( QC-WFF A) holds (p is atomic implies (F . p) = a(p)) & (p is negative implies (F . p) = n(.)) & (p is conjunctive implies (F . p) = c(.,.)) & (p is universal implies (F . p) = q(p,.)) from QC_LANG1:sch 3;

        take (F . p), F;

        thus (F . p) = (F . p);

        thus thesis by A1;

      end;

      uniqueness by Lm2;

    end

    theorem :: CQC_LANG:15



     Th15: (( VERUM A) . x) = ( VERUM A)

    proof

      ex F be Function of ( QC-WFF A), ( QC-WFF A) st (( VERUM A) . x) = (F . ( VERUM A)) & for q holds (F . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F . q) = ( 'not' (F . ( the_argument_of q)))) & (q is conjunctive implies (F . q) = ((F . ( the_left_argument_of q)) '&' (F . ( the_right_argument_of q)))) & (q is universal implies (F . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F . ( the_scope_of q))))))) by Def3;

      hence thesis;

    end;

    theorem :: CQC_LANG:16



     Th16: p is atomic implies (p . x) = (( the_pred_symbol_of p) ! ( Subst (( the_arguments_of p),((A a. 0 ) .--> x))))

    proof

      ex F be Function of ( QC-WFF A), ( QC-WFF A) st (p . x) = (F . p) & for q holds (F . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F . q) = ( 'not' (F . ( the_argument_of q)))) & (q is conjunctive implies (F . q) = ((F . ( the_left_argument_of q)) '&' (F . ( the_right_argument_of q)))) & (q is universal implies (F . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F . ( the_scope_of q))))))) by Def3;

      hence thesis;

    end;

    theorem :: CQC_LANG:17



     Th17: for k be Nat holds for P be QC-pred_symbol of k, A holds for l be QC-variable_list of k, A holds ((P ! l) . x) = (P ! ( Subst (l,((A a. 0 ) .--> x))))

    proof

      let k be Nat;

      let P be QC-pred_symbol of k, A;

      let l be QC-variable_list of k, A;

      reconsider P9 = P as QC-pred_symbol of A;



       A1: (P ! l) is atomic by QC_LANG1:def 18;

      then ( the_arguments_of (P ! l)) = l & ( the_pred_symbol_of (P ! l)) = P9 by QC_LANG1:def 22, QC_LANG1:def 23;

      hence thesis by A1, Th16;

    end;

    theorem :: CQC_LANG:18



     Th18: p is negative implies (p . x) = ( 'not' (( the_argument_of p) . x))

    proof

      consider F be Function of ( QC-WFF A), ( QC-WFF A) such that

       A1: (p . x) = (F . p) and

       A2: for q holds (F . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F . q) = ( 'not' (F . ( the_argument_of q)))) & (q is conjunctive implies (F . q) = ((F . ( the_left_argument_of q)) '&' (F . ( the_right_argument_of q)))) & (q is universal implies (F . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F . ( the_scope_of q))))))) by Def3;

      consider G be Function of ( QC-WFF A), ( QC-WFF A) such that

       A3: (( the_argument_of p) . x) = (G . ( the_argument_of p)) and

       A4: for q holds (G . ( VERUM A)) = ( VERUM A) & (q is atomic implies (G . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (G . q) = ( 'not' (G . ( the_argument_of q)))) & (q is conjunctive implies (G . q) = ((G . ( the_left_argument_of q)) '&' (G . ( the_right_argument_of q)))) & (q is universal implies (G . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(G . ( the_scope_of q))))))) by Def3;

      F = G by A2, A4, Lm2;

      hence thesis by A1, A2, A3;

    end;

    theorem :: CQC_LANG:19



     Th19: (( 'not' p) . x) = ( 'not' (p . x))

    proof

      set 9p = ( 'not' p);



       A1: 9p is negative by QC_LANG1:def 19;

      then ( the_argument_of 9p) = p by QC_LANG1:def 24;

      hence thesis by A1, Th18;

    end;

    theorem :: CQC_LANG:20



     Th20: p is conjunctive implies (p . x) = ((( the_left_argument_of p) . x) '&' (( the_right_argument_of p) . x))

    proof

      consider F be Function of ( QC-WFF A), ( QC-WFF A) such that

       A1: (p . x) = (F . p) and

       A2: for q holds (F . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F . q) = ( 'not' (F . ( the_argument_of q)))) & (q is conjunctive implies (F . q) = ((F . ( the_left_argument_of q)) '&' (F . ( the_right_argument_of q)))) & (q is universal implies (F . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F . ( the_scope_of q))))))) by Def3;

      consider F2 be Function of ( QC-WFF A), ( QC-WFF A) such that

       A3: (( the_right_argument_of p) . x) = (F2 . ( the_right_argument_of p)) and

       A4: for q holds (F2 . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F2 . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F2 . q) = ( 'not' (F2 . ( the_argument_of q)))) & (q is conjunctive implies (F2 . q) = ((F2 . ( the_left_argument_of q)) '&' (F2 . ( the_right_argument_of q)))) & (q is universal implies (F2 . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F2 . ( the_scope_of q))))))) by Def3;



       A5: F2 = F by A2, A4, Lm2;

      consider F1 be Function of ( QC-WFF A), ( QC-WFF A) such that

       A6: (( the_left_argument_of p) . x) = (F1 . ( the_left_argument_of p)) and

       A7: for q holds (F1 . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F1 . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F1 . q) = ( 'not' (F1 . ( the_argument_of q)))) & (q is conjunctive implies (F1 . q) = ((F1 . ( the_left_argument_of q)) '&' (F1 . ( the_right_argument_of q)))) & (q is universal implies (F1 . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F1 . ( the_scope_of q))))))) by Def3;

      F1 = F by A2, A7, Lm2;

      hence thesis by A1, A2, A6, A3, A5;

    end;

    theorem :: CQC_LANG:21



     Th21: ((p '&' q) . x) = ((p . x) '&' (q . x))

    proof

      set pq = (p '&' q);



       A1: (p '&' q) is conjunctive by QC_LANG1:def 20;

      then ( the_left_argument_of pq) = p & ( the_right_argument_of pq) = q by QC_LANG1:def 25, QC_LANG1:def 26;

      hence thesis by A1, Th20;

    end;



     Lm3: p is universal implies (p . x) = ( IFEQ (( bound_in p),x,p,( All (( bound_in p),(( the_scope_of p) . x)))))

    proof

      consider F be Function of ( QC-WFF A), ( QC-WFF A) such that

       A1: (p . x) = (F . p) and

       A2: for q holds (F . ( VERUM A)) = ( VERUM A) & (q is atomic implies (F . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (F . q) = ( 'not' (F . ( the_argument_of q)))) & (q is conjunctive implies (F . q) = ((F . ( the_left_argument_of q)) '&' (F . ( the_right_argument_of q)))) & (q is universal implies (F . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(F . ( the_scope_of q))))))) by Def3;

      consider G be Function of ( QC-WFF A), ( QC-WFF A) such that

       A3: (( the_scope_of p) . x) = (G . ( the_scope_of p)) and

       A4: for q holds (G . ( VERUM A)) = ( VERUM A) & (q is atomic implies (G . q) = (( the_pred_symbol_of q) ! ( Subst (( the_arguments_of q),((A a. 0 ) .--> x))))) & (q is negative implies (G . q) = ( 'not' (G . ( the_argument_of q)))) & (q is conjunctive implies (G . q) = ((G . ( the_left_argument_of q)) '&' (G . ( the_right_argument_of q)))) & (q is universal implies (G . q) = ( IFEQ (( bound_in q),x,q,( All (( bound_in q),(G . ( the_scope_of q))))))) by Def3;

      F = G by A2, A4, Lm2;

      hence thesis by A1, A2, A3;

    end;

    theorem :: CQC_LANG:22



     Th22: p is universal & ( bound_in p) = x implies (p . x) = p

    proof

      assume p is universal;

      then (p . x) = ( IFEQ (( bound_in p),x,p,( All (( bound_in p),(( the_scope_of p) . x))))) by Lm3;

      hence thesis by FUNCOP_1:def 8;

    end;

    theorem :: CQC_LANG:23



     Th23: p is universal & ( bound_in p) <> x implies (p . x) = ( All (( bound_in p),(( the_scope_of p) . x)))

    proof

      assume p is universal;

      then (p . x) = ( IFEQ (( bound_in p),x,p,( All (( bound_in p),(( the_scope_of p) . x))))) by Lm3;

      hence thesis by FUNCOP_1:def 8;

    end;

    theorem :: CQC_LANG:24



     Th24: (( All (x,p)) . x) = ( All (x,p))

    proof

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



       A1: q is universal by QC_LANG1:def 21;

      then ( bound_in q) = x by QC_LANG1:def 27;

      hence thesis by A1, Th22;

    end;

    theorem :: CQC_LANG:25



     Th25: x <> y implies (( All (x,p)) . y) = ( All (x,(p . y)))

    proof

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



       A1: q is universal by QC_LANG1:def 21;

      then ( the_scope_of q) = p & ( bound_in q) = x by QC_LANG1:def 27, QC_LANG1:def 28;

      hence thesis by A1, Th23;

    end;

    theorem :: CQC_LANG:26



     Th26: ( Free p) = {} implies (p . x) = p

    proof

      defpred P[ Element of ( QC-WFF A)] means ( Free $1) = {} implies ($1 . x) = $1;



       A1: for p st P[p] holds P[( 'not' p)] by Th19, QC_LANG3: 55;



       A2: for p, q st P[p] & P[q] holds P[(p '&' q)]

      proof

        let p, q;

        assume

         A3: (( Free p) = {} implies (p . x) = p) & (( Free q) = {} implies (q . x) = q);

        assume ( Free (p '&' q)) = {} ;

        then (( Free p) \/ ( Free q)) = {} by QC_LANG3: 57;

        hence thesis by A3, Th21;

      end;



       A4: for k be Nat holds for P be QC-pred_symbol of k, A, l be QC-variable_list of k, A holds P[(P ! l)]

      proof

        let k be Nat;

        let P be QC-pred_symbol of k, A, l be QC-variable_list of k, A;

        assume

         A5: ( Free (P ! l)) = {} ;

         A6:

        now

          let j be Nat;

          assume

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

          now

            assume (l . j) = (A a. 0 );

            then (A a. 0 ) in { (l . i) where i be Nat : 1 <= i & i <= ( len l) & (l . i) in ( free_QC-variables A) } by A7;

            hence contradiction by A5, QC_LANG3: 54;

          end;

          hence (( Subst (l,((A a. 0 ) .--> x))) . j) = (l . j) by A7, Th3;

        end;

        ( len ( Subst (l,((A a. 0 ) .--> x)))) = ( len l) by Def1;

        then ( Subst (l,((A a. 0 ) .--> x))) = l by A6, FINSEQ_1: 14;

        hence thesis by Th17;

      end;



       A8: for y, p st P[p] holds P[( All (y,p))]

      proof

        let y, p;

        assume

         A9: ( Free p) = {} implies (p . x) = p;



         A10: x = y implies (( All (y,p)) . x) = ( All (y,p)) by Th24;

        assume ( Free ( All (y,p))) = {} ;

        hence thesis by A9, A10, Th25, QC_LANG3: 58;

      end;



       A11: P[( VERUM A)] by Th15;

      for p holds P[p] from QC_LANG1:sch 1( A4, A11, A1, A2, A8);

      hence thesis;

    end;

    theorem :: CQC_LANG:27

    (r . x) = r

    proof

      ( Free r) = {} by Th4;

      hence thesis by Th26;

    end;

    theorem :: CQC_LANG:28

    ( Fixed (p . x)) = ( Fixed p)

    proof

      defpred P[ Element of ( QC-WFF A)] means ( Fixed ($1 . x)) = ( Fixed $1);



       A1: for p st P[p] holds P[( 'not' p)]

      proof

        let p such that

         A2: ( Fixed (p . x)) = ( Fixed p);



        thus ( Fixed (( 'not' p) . x)) = ( Fixed ( 'not' (p . x))) by Th19

        .= ( Fixed p) by A2, QC_LANG3: 65

        .= ( Fixed ( 'not' p)) by QC_LANG3: 65;

      end;



       A3: for p, q st P[p] & P[q] holds P[(p '&' q)]

      proof

        let p, q such that

         A4: ( Fixed (p . x)) = ( Fixed p) & ( Fixed (q . x)) = ( Fixed q);



        thus ( Fixed ((p '&' q) . x)) = ( Fixed ((p . x) '&' (q . x))) by Th21

        .= (( Fixed p) \/ ( Fixed q)) by A4, QC_LANG3: 67

        .= ( Fixed (p '&' q)) by QC_LANG3: 67;

      end;



       A5: for k holds for P be QC-pred_symbol of k, A, l be QC-variable_list of k, A holds P[(P ! l)]

      proof

        let k;

        let P be QC-pred_symbol of k, A, l be QC-variable_list of k, A;

        set F1 = { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( fixed_QC-variables A) };

        set ll = ( Subst (l,((A a. 0 ) .--> x)));

        set F2 = { (ll . i) : 1 <= i & i <= ( len ll) & (ll . i) in ( fixed_QC-variables A) };



         A6: ( len l) = ( len ll) by Def1;

        now

          let y be object;

          thus y in F1 implies y in F2

          proof

            assume y in F1;

            then

            consider i such that

             A7: y = (l . i) and

             A8: 1 <= i & i <= ( len l) and

             A9: (l . i) in ( fixed_QC-variables A);

            (l . i) <> (A a. 0 ) by A9, QC_LANG3: 32;

            then (ll . i) = (l . i) by A8, Th3;

            hence thesis by A6, A7, A8, A9;

          end;

          assume y in F2;

          then

          consider i such that

           A10: y = (ll . i) and

           A11: 1 <= i & i <= ( len ll) and

           A12: (ll . i) in ( fixed_QC-variables A);

          now

            assume (l . i) = (A a. 0 );

            then (ll . i) = x by A6, A11, Th3;

            hence contradiction by A12, Lm1;

          end;

          then (ll . i) = (l . i) by A6, A11, Th3;

          hence y in F1 by A6, A10, A11, A12;

        end;

        then

         A13: F1 = F2 by TARSKI: 2;

        ( Fixed (P ! l)) = F1 & ( Fixed (P ! ll)) = F2 by QC_LANG3: 64;

        hence thesis by A13, Th17;

      end;



       A14: for y, p st P[p] holds P[( All (y,p))]

      proof

        let y, p such that

         A15: ( Fixed (p . x)) = ( Fixed p);

        now

          assume x <> y;



          hence ( Fixed (( All (y,p)) . x)) = ( Fixed ( All (y,(p . x)))) by Th25

          .= ( Fixed p) by A15, QC_LANG3: 68

          .= ( Fixed ( All (y,p))) by QC_LANG3: 68;

        end;

        hence thesis by Th24;

      end;



       A16: P[( VERUM A)] by Th15;

      for p holds P[p] from QC_LANG1:sch 1( A5, A16, A1, A3, A14);

      hence thesis;

    end;