qc_lang3.miz



    begin

    reserve i,k for Nat;

    scheme :: QC_LANG3:sch1

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

F1() = F2()

      provided

       A1: for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F1() . p) = V()) & (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))

       and

       A2: for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F2() . p) = V()) & (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));

      defpred Prop[ Element of ( QC-WFF Al())] means (F1() . $1) = (F2() . $1);

      

       A3: for k holds for P be QC-pred_symbol of k, Al(), l be QC-variable_list of k, Al() holds Prop[(P ! l)]

      proof

        let k;

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

        

         A4: (P ! l) is atomic;

        

        hence (F1() . (P ! l)) = A(!) by A1

        .= (F2() . (P ! l)) by A2, A4;

      end;

      

       A5: for x be bound_QC-variable of Al(), p be Element of ( QC-WFF Al()) holds Prop[p] implies Prop[( All (x,p))]

      proof

        let x be bound_QC-variable of Al(), p be Element of ( QC-WFF Al()) such that

         A6: (F1() . p) = (F2() . p);

        

         A7: ( All (x,p)) is universal;

        then ( the_scope_of ( All (x,p))) = p by QC_LANG1:def 28;

        

        hence (F1() . ( All (x,p))) = Q(All,.) by A1, A6, A7

        .= (F2() . ( All (x,p))) by A2, A7;

      end;

      

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

      proof

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

         A9: (F1() . p) = (F2() . p) & (F1() . q) = (F2() . q);

        

         A10: (p '&' q) is conjunctive;

        then

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

        

        hence (F1() . (p '&' q)) = C(.,.) by A1, A9, A10

        .= (F2() . (p '&' q)) by A2, A10, A11;

      end;

      

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

      proof

        let p be Element of ( QC-WFF Al()) such that

         A13: (F1() . p) = (F2() . p);

        

         A14: ( 'not' p) is negative;

        then

         A15: ( the_argument_of ( 'not' p)) = p by QC_LANG1:def 24;

        

        hence (F1() . ( 'not' p)) = N(.) by A1, A13, A14

        .= (F2() . ( 'not' p)) by A2, A14, A15;

      end;

      (F1() . ( VERUM Al())) = V() by A1;

      then

       A16: Prop[( VERUM Al())] by A2;

      for p be Element of ( QC-WFF Al()) holds Prop[p] from QC_LANG1:sch 1( A3, A16, A12, A8, A5);

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: QC_LANG3:sch2

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

(ex d be Element of D(), F be Function of ( QC-WFF Al()), D() st d = (F . p()) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) & for x1,x2 be Element of D() st (ex F be Function of ( QC-WFF Al()), D() st x1 = (F . p()) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) & (ex F be Function of ( QC-WFF Al()), D() st x2 = (F . p()) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) holds x1 = x2;

      thus ex d be Element of D(), F be Function of ( QC-WFF Al()), D() st d = (F . p()) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))

      proof

        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;

        take (F . p()), F;

        thus thesis by A1;

      end;

      let x1,x2 be Element of D();

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

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

       A3: for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F1 . p) = V()) & (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));

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

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

       A5: for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F2 . p) = V()) & (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));

      F1 = F2 from QCFuncUniq( A3, A5);

      hence thesis by A2, A4;

    end;

    scheme :: QC_LANG3:sch3

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

F(VERUM) = V()

      provided

       A1: for p be QC-formula of Al(), d be Element of D() holds d = F(p) iff ex F be Function of ( QC-WFF Al()), D() st d = (F . p) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1));

      ex F be Function of ( QC-WFF Al()), D() st F(VERUM) = (F . ( VERUM Al())) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1)) by A1;

      hence thesis;

    end;

    scheme :: QC_LANG3:sch4

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

F(p) = A(p)

      provided

       A1: for p be QC-formula of Al(), d be Element of D() holds d = F(p) iff ex F be Function of ( QC-WFF Al()), D() st d = (F . p) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))

       and

       A2: p() is atomic;

      ex F be Function of ( QC-WFF Al()), D() st F(p) = (F . p()) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1)) by A1;

      hence thesis by A2;

    end;

    scheme :: QC_LANG3:sch5

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

F(p) = N(F)

      provided

       A1: for p be QC-formula of Al(), d be Element of D() holds d = F(p) iff ex F be Function of ( QC-WFF Al()), D() st d = (F . p) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))

       and

       A2: p() is negative;

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

       A3: F(p) = (F . p()) and

       A4: for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1)) by A1;

      (F . ( the_argument_of p())) = F(the_argument_of) by A1, A4;

      hence thesis by A2, A3, A4;

    end;

    scheme :: QC_LANG3:sch6

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

for d1,d2 be Element of D() st d1 = F(the_left_argument_of) & d2 = F(the_right_argument_of) holds F(p) = C(d1,d2)

      provided

       A1: for p be QC-formula of Al(), d be Element of D() holds d = F(p) iff ex F be Function of ( QC-WFF Al()), D() st d = (F . p) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))

       and

       A2: p() is conjunctive;

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

       A3: F(p) = (F . p()) and

       A4: for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1)) by A1;

      let d1,d2 be Element of D();

      assume d1 = F(the_left_argument_of) & d2 = F(the_right_argument_of);

      then (F . ( the_left_argument_of p())) = d1 & (F . ( the_right_argument_of p())) = d2 by A1, A4;

      hence thesis by A2, A3, A4;

    end;

    scheme :: QC_LANG3:sch7

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

F(p) = Q(p,F)

      provided

       A1: for p be QC-formula of Al(), d be Element of D() holds d = F(p) iff ex F be Function of ( QC-WFF Al()), D() st d = (F . p) & for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))

       and

       A2: p() is universal;

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

       A3: F(p) = (F . p()) and

       A4: for p be Element of ( QC-WFF Al()) holds for d1,d2 be Element of D() holds (p = ( VERUM Al()) implies (F . p) = V()) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1)) by A1;

      (F . ( the_scope_of p())) = F(the_scope_of) by A1, A4;

      hence thesis by A2, A3, A4;

    end;

    reserve A for QC-alphabet;

    reserve x 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 for FinSequence of ( QC-variables A);

    reserve P,Q for QC-pred_symbol of A;

    reserve V for non empty Subset of ( QC-variables A);

    reserve s,t for QC-symbol of A;

    theorem :: QC_LANG3:1

    P is QC-pred_symbol of ( the_arity_of P), A

    proof

      set k = ( the_arity_of P);

      set QCP = { Q : ( the_arity_of Q) = k };

      P in QCP;

      hence thesis;

    end;

    definition

      let A, l, V;

      :: QC_LANG3:def1

      func variables_in (l,V) -> Subset of V equals { (l . k) : 1 <= k & k <= ( len l) & (l . k) in V };

      coherence

      proof

        set A = { (l . k) : 1 <= k & k <= ( len l) & (l . k) in V };

        A c= V

        proof

          let x be object;

          assume x in A;

          then ex k st (l . k) = x & 1 <= k & k <= ( len l) & (l . k) in V;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: QC_LANG3:2

    ( still_not-bound_in l) = ( variables_in (l,( bound_QC-variables A)));

     Lm1:

    now

      let A be QC-alphabet;

      deffunc F1( Element of ( QC-WFF A)) = ( still_not-bound_in $1);

      deffunc A1( Element of ( QC-WFF A)) = ( still_not-bound_in ( the_arguments_of $1));

      deffunc Q1( Element of ( QC-WFF A), Subset of ( bound_QC-variables A)) = ($2 \ {( bound_in $1)});

      deffunc N1( Subset of ( bound_QC-variables A)) = $1;

      deffunc C1( Subset of ( bound_QC-variables A), Subset of ( bound_QC-variables A)) = ($1 \/ $2);

      thus for p be QC-formula of A, d be Subset of ( bound_QC-variables A) holds d = F1(p) iff ex F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = A1(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N1(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C1(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q1(p,d1))

      proof

        let p be QC-formula of A, d be Subset of ( bound_QC-variables A);

        thus d = ( still_not-bound_in p) implies ex F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = ( still_not-bound_in ( the_arguments_of p))) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = d1) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = (d1 \/ d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = (d1 \ {( bound_in p)}))

        proof

          assume d = ( still_not-bound_in p);

          then

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

           A1: d = (F . p) & for p be Element of ( QC-WFF A) holds (F . ( VERUM A)) = {} & (p is atomic implies (F . p) = { (( the_arguments_of p) . k) : 1 <= k & k <= ( len ( the_arguments_of p)) & (( the_arguments_of p) . k) in ( bound_QC-variables A) }) & (p is negative implies (F . p) = (F . ( the_argument_of p))) & (p is conjunctive implies (F . p) = ((F . ( the_left_argument_of p)) \/ (F . ( the_right_argument_of p)))) & (p is universal implies (F . p) = ((F . ( the_scope_of p)) \ {( bound_in p)})) by QC_LANG1:def 30;

          take F;

          thus d = (F . p) by A1;

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

          let d1,d2 be Subset of ( bound_QC-variables A);

          thus (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = ( still_not-bound_in ( the_arguments_of p))) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = d1) by A1;

          thus thesis by A1;

        end;

        given F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) such that

         A2: d = (F . p) and

         A3: for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = ( still_not-bound_in ( the_arguments_of p))) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = d1) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = (d1 \/ d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = (d1 \ {( bound_in p)}));

        now

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

          thus (F . ( VERUM A)) = {} by A3;

          thus p is atomic implies (F . p) = { (( the_arguments_of p) . k) : 1 <= k & k <= ( len ( the_arguments_of p)) & (( the_arguments_of p) . k) in ( bound_QC-variables A) }

          proof

            assume p is atomic;

            then (F . p) = ( still_not-bound_in ( the_arguments_of p)) by A3;

            hence thesis;

          end;

          thus p is negative implies (F . p) = (F . ( the_argument_of p)) by A3;

          thus p is conjunctive implies (F . p) = ((F . ( the_left_argument_of p)) \/ (F . ( the_right_argument_of p))) by A3;

          assume p is universal;

          hence (F . p) = ((F . ( the_scope_of p)) \ {( bound_in p)}) by A3;

        end;

        hence thesis by A2, QC_LANG1:def 30;

      end;

    end;

    theorem :: QC_LANG3:3

    

     Th3: ( still_not-bound_in ( VERUM A)) = {}

    proof

      deffunc F1( Element of ( QC-WFF A)) = ( still_not-bound_in $1);

      deffunc A1( Element of ( QC-WFF A)) = ( still_not-bound_in ( the_arguments_of $1));

      deffunc Q1( Element of ( QC-WFF A), Subset of ( bound_QC-variables A)) = ($2 \ {( bound_in $1)});

      deffunc N1( Subset of ( bound_QC-variables A)) = $1;

      deffunc C1( Subset of ( bound_QC-variables A), Subset of ( bound_QC-variables A)) = ($1 \/ $2);

      

       A1: for p be QC-formula of A, d be Subset of ( bound_QC-variables A) holds d = F1(p) iff ex F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = A1(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N1(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C1(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q1(p,d1)) by Lm1;

      

      thus F1(VERUM) = ( {} ( bound_QC-variables A)) from QCDResult9VERUM( A1)

      .= {} ;

    end;

    theorem :: QC_LANG3:4

    

     Th4: for p be QC-formula of A st p is atomic holds ( still_not-bound_in p) = ( still_not-bound_in ( the_arguments_of p))

    proof

      deffunc F1( Element of ( QC-WFF A)) = ( still_not-bound_in $1);

      deffunc A1( Element of ( QC-WFF A)) = ( still_not-bound_in ( the_arguments_of $1));

      deffunc Q1( Element of ( QC-WFF A), Subset of ( bound_QC-variables A)) = ($2 \ {( bound_in $1)});

      deffunc N1( Subset of ( bound_QC-variables A)) = $1;

      deffunc C1( Subset of ( bound_QC-variables A), Subset of ( bound_QC-variables A)) = ($1 \/ $2);

      

       A1: for p be QC-formula of A, d be Subset of ( bound_QC-variables A) holds d = F1(p) iff ex F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = A1(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N1(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C1(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q1(p,d1)) by Lm1;

      let p be QC-formula of A such that

       A2: p is atomic;

      thus F1(p) = A1(p) from QCDResult9atomic( A1, A2);

    end;

    theorem :: QC_LANG3:5

    for P be QC-pred_symbol of k, A holds for l be QC-variable_list of k, A holds ( still_not-bound_in (P ! l)) = ( still_not-bound_in l)

    proof

      let P be QC-pred_symbol of k, A;

      let l be QC-variable_list of k, A;

      

       A1: (P ! l) is atomic;

      then ( the_arguments_of (P ! l)) = l by QC_LANG1:def 23;

      hence thesis by A1, Th4;

    end;

    theorem :: QC_LANG3:6

    

     Th6: for p be QC-formula of A st p is negative holds ( still_not-bound_in p) = ( still_not-bound_in ( the_argument_of p))

    proof

      deffunc F1( Element of ( QC-WFF A)) = ( still_not-bound_in $1);

      deffunc A1( Element of ( QC-WFF A)) = ( still_not-bound_in ( the_arguments_of $1));

      deffunc Q1( Element of ( QC-WFF A), Subset of ( bound_QC-variables A)) = ($2 \ {( bound_in $1)});

      deffunc N1( Subset of ( bound_QC-variables A)) = $1;

      deffunc C1( Subset of ( bound_QC-variables A), Subset of ( bound_QC-variables A)) = ($1 \/ $2);

      

       A1: for p be QC-formula of A, d be Subset of ( bound_QC-variables A) holds d = F1(p) iff ex F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = A1(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N1(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C1(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q1(p,d1)) by Lm1;

      let p be QC-formula of A such that

       A2: p is negative;

      thus F1(p) = N1(F1) from QCDResult9negative( A1, A2);

    end;

    theorem :: QC_LANG3:7

    

     Th7: for p be QC-formula of A holds ( still_not-bound_in ( 'not' p)) = ( still_not-bound_in p)

    proof

      let p be QC-formula of A;

      

       A1: ( 'not' p) is negative;

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

      hence thesis by A1, Th6;

    end;

    theorem :: QC_LANG3:8

    

     Th8: ( still_not-bound_in ( FALSUM A)) = {}

    proof

      ( still_not-bound_in ( FALSUM A)) = ( still_not-bound_in ( 'not' ( VERUM A))) by QC_LANG2:def 1

      .= ( still_not-bound_in ( VERUM A)) by Th7

      .= {} by Th3;

      hence thesis;

    end;

    theorem :: QC_LANG3:9

    

     Th9: for p be QC-formula of A st p is conjunctive holds ( still_not-bound_in p) = (( still_not-bound_in ( the_left_argument_of p)) \/ ( still_not-bound_in ( the_right_argument_of p)))

    proof

      deffunc F1( Element of ( QC-WFF A)) = ( still_not-bound_in $1);

      deffunc A1( Element of ( QC-WFF A)) = ( still_not-bound_in ( the_arguments_of $1));

      deffunc Q1( Element of ( QC-WFF A), Subset of ( bound_QC-variables A)) = ($2 \ {( bound_in $1)});

      deffunc N1( Subset of ( bound_QC-variables A)) = $1;

      deffunc C1( Subset of ( bound_QC-variables A), Subset of ( bound_QC-variables A)) = ($1 \/ $2);

      

       A1: for p be QC-formula of A, d be Subset of ( bound_QC-variables A) holds d = F1(p) iff ex F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = A1(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N1(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C1(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q1(p,d1)) by Lm1;

      let p be QC-formula of A such that

       A2: p is conjunctive;

      for d1,d2 be Subset of ( bound_QC-variables A) st d1 = F1(the_left_argument_of) & d2 = F1(the_right_argument_of) holds F1(p) = C1(d1,d2) from QCDResult9conjunctive( A1, A2);

      hence thesis;

    end;

    theorem :: QC_LANG3:10

    

     Th10: for p,q be QC-formula of A holds ( still_not-bound_in (p '&' q)) = (( still_not-bound_in p) \/ ( still_not-bound_in q))

    proof

      let p,q be QC-formula of A;

      set pq = (p '&' q);

      

       A1: pq is conjunctive;

      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, Th9;

    end;

    theorem :: QC_LANG3:11

    

     Th11: for p be QC-formula of A st p is universal holds ( still_not-bound_in p) = (( still_not-bound_in ( the_scope_of p)) \ {( bound_in p)})

    proof

      deffunc F1( Element of ( QC-WFF A)) = ( still_not-bound_in $1);

      deffunc A1( Element of ( QC-WFF A)) = ( still_not-bound_in ( the_arguments_of $1));

      deffunc Q1( Element of ( QC-WFF A), Subset of ( bound_QC-variables A)) = ($2 \ {( bound_in $1)});

      deffunc N1( Subset of ( bound_QC-variables A)) = $1;

      deffunc C1( Subset of ( bound_QC-variables A), Subset of ( bound_QC-variables A)) = ($1 \/ $2);

      

       A1: for p be QC-formula of A, d be Subset of ( bound_QC-variables A) holds d = F1(p) iff ex F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = A1(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N1(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C1(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q1(p,d1)) by Lm1;

      let p be QC-formula of A such that

       A2: p is universal;

      thus F1(p) = Q1(p,F1) from QCDResult9universal( A1, A2);

    end;

    theorem :: QC_LANG3:12

    

     Th12: for p be QC-formula of A holds ( still_not-bound_in ( All (x,p))) = (( still_not-bound_in p) \ {x})

    proof

      let p be QC-formula of A;

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

      

       A1: a is universal;

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

      hence thesis by A1, Th11;

    end;

    theorem :: QC_LANG3:13

    

     Th13: for p be QC-formula of A st p is disjunctive holds ( still_not-bound_in p) = (( still_not-bound_in ( the_left_disjunct_of p)) \/ ( still_not-bound_in ( the_right_disjunct_of p)))

    proof

      let p be QC-formula of A;

      set p1 = ( the_left_disjunct_of p);

      set p2 = ( the_right_disjunct_of p);

      assume p is disjunctive;

      then p = (( the_left_disjunct_of p) 'or' ( the_right_disjunct_of p)) by QC_LANG2: 37;

      then p = ( 'not' (( 'not' p1) '&' ( 'not' p2))) by QC_LANG2:def 3;

      

      then ( still_not-bound_in p) = ( still_not-bound_in (( 'not' p1) '&' ( 'not' p2))) by Th7

      .= (( still_not-bound_in ( 'not' p1)) \/ ( still_not-bound_in ( 'not' p2))) by Th10

      .= (( still_not-bound_in p1) \/ ( still_not-bound_in ( 'not' p2))) by Th7

      .= (( still_not-bound_in p1) \/ ( still_not-bound_in p2)) by Th7;

      hence thesis;

    end;

    theorem :: QC_LANG3:14

    for p,q be QC-formula of A holds ( still_not-bound_in (p 'or' q)) = (( still_not-bound_in p) \/ ( still_not-bound_in q))

    proof

      let p,q be QC-formula of A;

      

       A1: ( the_right_disjunct_of (p 'or' q)) = q by QC_LANG2: 29;

      (p 'or' q) is disjunctive & ( the_left_disjunct_of (p 'or' q)) = p by QC_LANG2: 29, QC_LANG2:def 10;

      hence thesis by A1, Th13;

    end;

    theorem :: QC_LANG3:15

    

     Th15: for p be QC-formula of A st p is conditional holds ( still_not-bound_in p) = (( still_not-bound_in ( the_antecedent_of p)) \/ ( still_not-bound_in ( the_consequent_of p)))

    proof

      let p be QC-formula of A;

      set p1 = ( the_antecedent_of p);

      set p2 = ( the_consequent_of p);

      assume p is conditional;

      then p = (( the_antecedent_of p) => ( the_consequent_of p)) by QC_LANG2: 38;

      then p = ( 'not' (p1 '&' ( 'not' p2))) by QC_LANG2:def 2;

      

      then ( still_not-bound_in p) = ( still_not-bound_in (p1 '&' ( 'not' p2))) by Th7

      .= (( still_not-bound_in p1) \/ ( still_not-bound_in ( 'not' p2))) by Th10

      .= (( still_not-bound_in p1) \/ ( still_not-bound_in p2)) by Th7;

      hence thesis;

    end;

    theorem :: QC_LANG3:16

    

     Th16: for p,q be QC-formula of A holds ( still_not-bound_in (p => q)) = (( still_not-bound_in p) \/ ( still_not-bound_in q))

    proof

      let p,q be QC-formula of A;

      

       A1: ( the_consequent_of (p => q)) = q by QC_LANG2: 30;

      (p => q) is conditional & ( the_antecedent_of (p => q)) = p by QC_LANG2: 30, QC_LANG2:def 11;

      hence thesis by A1, Th15;

    end;

    theorem :: QC_LANG3:17

    

     Th17: for p be QC-formula of A st p is biconditional holds ( still_not-bound_in p) = (( still_not-bound_in ( the_left_side_of p)) \/ ( still_not-bound_in ( the_right_side_of p)))

    proof

      let p be QC-formula of A;

      set p1 = ( the_left_side_of p);

      set p2 = ( the_right_side_of p);

      assume p is biconditional;

      then p = (( the_left_side_of p) <=> ( the_right_side_of p)) by QC_LANG2: 39;

      then p = ((p1 => p2) '&' (p2 => p1)) by QC_LANG2:def 4;

      

      then ( still_not-bound_in p) = (( still_not-bound_in (p1 => p2)) \/ ( still_not-bound_in (p2 => p1))) by Th10

      .= ((( still_not-bound_in p1) \/ ( still_not-bound_in p2)) \/ ( still_not-bound_in (p2 => p1))) by Th16

      .= ((( still_not-bound_in p1) \/ ( still_not-bound_in p2)) \/ (( still_not-bound_in p1) \/ ( still_not-bound_in p2))) by Th16

      .= (( still_not-bound_in p1) \/ ( still_not-bound_in p2));

      hence thesis;

    end;

    theorem :: QC_LANG3:18

    for p,q be QC-formula of A holds ( still_not-bound_in (p <=> q)) = (( still_not-bound_in p) \/ ( still_not-bound_in q))

    proof

      let p,q be QC-formula of A;

      

       A1: ( the_right_side_of (p <=> q)) = q by QC_LANG2: 31;

      (p <=> q) is biconditional & ( the_left_side_of (p <=> q)) = p by QC_LANG2: 31, QC_LANG2:def 12;

      hence thesis by A1, Th17;

    end;

    theorem :: QC_LANG3:19

    

     Th19: for p be QC-formula of A holds ( still_not-bound_in ( Ex (x,p))) = (( still_not-bound_in p) \ {x})

    proof

      let p be QC-formula of A;

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

      

      hence ( still_not-bound_in ( Ex (x,p))) = ( still_not-bound_in ( All (x,( 'not' p)))) by Th7

      .= (( still_not-bound_in ( 'not' p)) \ {x}) by Th12

      .= (( still_not-bound_in p) \ {x}) by Th7;

    end;

    theorem :: QC_LANG3:20

    ( VERUM A) is closed & ( FALSUM A) is closed by Th3, Th8;

    theorem :: QC_LANG3:21

    

     Th21: for p be QC-formula of A holds p is closed iff ( 'not' p) is closed by Th7;

    theorem :: QC_LANG3:22

    

     Th22: for p,q be QC-formula of A holds p is closed & q is closed iff (p '&' q) is closed

    proof

      let p,q be QC-formula of A;

      thus p is closed & q is closed implies (p '&' q) is closed

      proof

        assume ( still_not-bound_in p) = {} & ( still_not-bound_in q) = {} ;

        then (( still_not-bound_in p) \/ ( still_not-bound_in q)) = {} ;

        hence ( still_not-bound_in (p '&' q)) = {} by Th10;

      end;

      assume

       A1: ( still_not-bound_in (p '&' q)) = {} ;

      ( still_not-bound_in (p '&' q)) = (( still_not-bound_in p) \/ ( still_not-bound_in q)) by Th10;

      hence ( still_not-bound_in p) = {} & ( still_not-bound_in q) = {} by A1, XBOOLE_1: 15;

    end;

    theorem :: QC_LANG3:23

    

     Th23: for p be QC-formula of A holds ( All (x,p)) is closed iff ( still_not-bound_in p) c= {x}

    proof

      let p be QC-formula of A;

      thus ( All (x,p)) is closed implies ( still_not-bound_in p) c= {x}

      proof

        assume ( still_not-bound_in ( All (x,p))) = {} ;

        then {} = (( still_not-bound_in p) \ {x}) by Th12;

        hence thesis by XBOOLE_1: 37;

      end;

      assume ( still_not-bound_in p) c= {x};

      then {} = (( still_not-bound_in p) \ {x}) by XBOOLE_1: 37;

      hence ( still_not-bound_in ( All (x,p))) = {} by Th12;

    end;

    theorem :: QC_LANG3:24

    for p be QC-formula of A st p is closed holds ( All (x,p)) is closed

    proof

      let p be QC-formula of A;

      assume ( still_not-bound_in p) = {} ;

      then ( still_not-bound_in p) c= {x} by XBOOLE_1: 2;

      hence thesis by Th23;

    end;

    theorem :: QC_LANG3:25

    for p,q be QC-formula of A holds p is closed & q is closed iff (p 'or' q) is closed

    proof

      let p,q be QC-formula of A;

      

       A1: (p 'or' q) = ( 'not' (( 'not' p) '&' ( 'not' q))) by QC_LANG2:def 3;

      (( 'not' p) '&' ( 'not' q)) is closed iff ( 'not' p) is closed & ( 'not' q) is closed by Th22;

      hence thesis by A1, Th21;

    end;

    theorem :: QC_LANG3:26

    

     Th26: for p,q be QC-formula of A holds p is closed & q is closed iff (p => q) is closed

    proof

      let p,q be QC-formula of A;

      

       A1: (p => q) = ( 'not' (p '&' ( 'not' q))) by QC_LANG2:def 2;

      (p '&' ( 'not' q)) is closed iff p is closed & ( 'not' q) is closed by Th22;

      hence thesis by A1, Th21;

    end;

    theorem :: QC_LANG3:27

    for p,q be QC-formula of A holds p is closed & q is closed iff (p <=> q) is closed

    proof

      let p,q be QC-formula of A;

      (p <=> q) = ((p => q) '&' (q => p)) by QC_LANG2:def 4;

      then (p <=> q) is closed iff (p => q) is closed & (q => p) is closed by Th22;

      hence thesis by Th26;

    end;

    theorem :: QC_LANG3:28

    

     Th28: for p be QC-formula of A holds ( Ex (x,p)) is closed iff ( still_not-bound_in p) c= {x}

    proof

      let p be QC-formula of A;

      thus ( Ex (x,p)) is closed implies ( still_not-bound_in p) c= {x}

      proof

        assume ( still_not-bound_in ( Ex (x,p))) = {} ;

        then {} = (( still_not-bound_in p) \ {x}) by Th19;

        hence thesis by XBOOLE_1: 37;

      end;

      assume ( still_not-bound_in p) c= {x};

      then {} = (( still_not-bound_in p) \ {x}) by XBOOLE_1: 37;

      hence ( still_not-bound_in ( Ex (x,p))) = {} by Th19;

    end;

    theorem :: QC_LANG3:29

    for p be QC-formula of A st p is closed holds ( Ex (x,p)) is closed

    proof

      let p be QC-formula of A;

      assume ( still_not-bound_in p) = {} ;

      then ( still_not-bound_in p) c= {x} by XBOOLE_1: 2;

      hence thesis by Th28;

    end;

    definition

      let A, s;

      :: QC_LANG3:def2

      func x. s -> bound_QC-variable of A equals [4, s];

      coherence

      proof

        4 in {4} by TARSKI:def 1;

        hence thesis by ZFMISC_1:def 2;

      end;

    end

    theorem :: QC_LANG3:30

    ex t st ( x. t) = x

    proof

      consider i,t be object such that

       A1: i in {4} and

       A2: t in ( QC-symbols A) and

       A3: [i, t] = x by ZFMISC_1:def 2;

      reconsider t as QC-symbol of A by A2;

      take t;

      thus thesis by A1, A3, TARSKI:def 1;

    end;

    definition

      let A, k;

      :: QC_LANG3:def3

      func (A) a. k -> free_QC-variable of A equals [6, k];

      coherence

      proof

        

         A1: k in NAT by ORDINAL1:def 12;

        6 in {6} by TARSKI:def 1;

        hence thesis by ZFMISC_1:def 2, A1;

      end;

    end

    theorem :: QC_LANG3:31

    ex i st (A a. i) = a

    proof

      consider x,y be object such that

       A1: x in {6} and

       A2: y in NAT and

       A3: [x, y] = a by ZFMISC_1:def 2;

      reconsider i = y as Nat by A2;

      take i;

      thus thesis by A1, A3, TARSKI:def 1;

    end;

    theorem :: QC_LANG3:32

    for c be Element of ( fixed_QC-variables A) holds for a be Element of ( free_QC-variables A) holds c <> a

    proof

      let c be Element of ( fixed_QC-variables A);

      let a be Element of ( free_QC-variables A);

      consider a1,a2 be object such that

       A1: a1 in {6} and a2 in NAT and

       A2: a = [a1, a2] by ZFMISC_1:def 2;

      consider c1,c2 be object such that

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

       A4: c = [c1, c2] by ZFMISC_1:def 2;

      

       A5: c1 = 5 by A3, TARSKI:def 1;

      a1 = 6 by A1, TARSKI:def 1;

      hence thesis by A2, A4, A5, XTUPLE_0: 1;

    end;

    theorem :: QC_LANG3:33

    for c be Element of ( fixed_QC-variables A) holds for x be Element of ( bound_QC-variables A) holds c <> x

    proof

      let c be Element of ( fixed_QC-variables A);

      let x be Element of ( bound_QC-variables A);

      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;

      consider c1,c2 be object such that

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

       A4: c = [c1, c2] by ZFMISC_1:def 2;

      

       A5: c1 = 5 by A3, TARSKI:def 1;

      x1 = 4 by A1, TARSKI:def 1;

      hence thesis by A2, A4, A5, XTUPLE_0: 1;

    end;

    theorem :: QC_LANG3:34

    for a be Element of ( free_QC-variables A) holds for x be Element of ( bound_QC-variables A) holds a <> x

    proof

      let a be Element of ( free_QC-variables A);

      let x be Element of ( bound_QC-variables A);

      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;

      consider a1,a2 be object such that

       A3: a1 in {6} and a2 in NAT and

       A4: a = [a1, a2] by ZFMISC_1:def 2;

      

       A5: a1 = 6 by A3, TARSKI:def 1;

      x1 = 4 by A1, TARSKI:def 1;

      hence thesis by A2, A4, A5, XTUPLE_0: 1;

    end;

    definition

      let A, V, p;

      :: QC_LANG3:def4

      func Vars (p,V) -> Subset of V means

      : Def4: ex F be Function of ( QC-WFF A), ( bool V) st it = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of V holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = ( variables_in (( the_arguments_of p),V))) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = d1) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = (d1 \/ d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = d1);

      correctness

      proof

        deffunc Q( Element of ( QC-WFF A), Subset of V) = $2;

        deffunc C( Subset of V, Subset of V) = ($1 \/ $2);

        deffunc N( Subset of V) = $1;

        deffunc A( Element of ( QC-WFF A)) = ( variables_in (( the_arguments_of $1),V));

        thus (ex d be Subset of V, F be Function of ( QC-WFF A), ( bool V) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of V holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) & for x1,x2 be Subset of V st (ex F be Function of ( QC-WFF A), ( bool V) st x1 = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of V holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) & (ex F be Function of ( QC-WFF A), ( bool V) st x2 = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of V holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) holds x1 = x2 from QCDefD;

      end;

    end

     Lm2:

    now

      let A, V;

      deffunc F1( Element of ( QC-WFF A)) = ( Vars ($1,V));

      deffunc A( Element of ( QC-WFF A)) = ( variables_in (( the_arguments_of $1),V));

      deffunc N( Subset of V) = $1;

      deffunc C( Subset of V, Subset of V) = ($1 \/ $2);

      deffunc Q( Element of ( QC-WFF A), Subset of V) = $2;

      

       A1: for X be Subset of V holds X = F1(p) iff ex F be Function of ( QC-WFF A), ( bool V) st X = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of V holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1)) by Def4;

      

      thus F1(VERUM) = ( {} V) from QCDResult9VERUM( A1)

      .= {} ;

      thus p is atomic implies ( Vars (p,V)) = ( variables_in (( the_arguments_of p),V))

      proof

        assume

         A2: p is atomic;

        thus F1(p) = A(p) from QCDResult9atomic( A1, A2);

      end;

      thus p is negative implies ( Vars (p,V)) = ( Vars (( the_argument_of p),V))

      proof

        assume

         A3: p is negative;

        thus F1(p) = N(F1) from QCDResult9negative( A1, A3);

      end;

      thus p is conjunctive implies ( Vars (p,V)) = (( Vars (( the_left_argument_of p),V)) \/ ( Vars (( the_right_argument_of p),V)))

      proof

        assume

         A4: p is conjunctive;

        for d1,d2 be Subset of V st d1 = F1(the_left_argument_of) & d2 = F1(the_right_argument_of) holds F1(p) = C(d1,d2) from QCDResult9conjunctive( A1, A4);

        hence thesis;

      end;

      thus p is universal implies ( Vars (p,V)) = ( Vars (( the_scope_of p),V))

      proof

        assume

         A5: p is universal;

        thus F1(p) = Q(p,F1) from QCDResult9universal( A1, A5);

      end;

    end;

    theorem :: QC_LANG3:35

    ( Vars (( VERUM A),V)) = {} by Lm2;

    theorem :: QC_LANG3:36

    

     Th36: p is atomic implies ( Vars (p,V)) = ( variables_in (( the_arguments_of p),V)) & ( Vars (p,V)) = { (( the_arguments_of p) . k) : 1 <= k & k <= ( len ( the_arguments_of p)) & (( the_arguments_of p) . k) in V }

    proof

      assume p is atomic;

      hence ( Vars (p,V)) = ( variables_in (( the_arguments_of p),V)) by Lm2;

      hence thesis;

    end;

    theorem :: QC_LANG3:37

    

     Th37: for P be QC-pred_symbol of k, A holds for l be QC-variable_list of k, A holds ( Vars ((P ! l),V)) = ( variables_in (l,V)) & ( Vars ((P ! l),V)) = { (l . i) : 1 <= i & i <= ( len l) & (l . i) in V }

    proof

      let P be QC-pred_symbol of k, A;

      let l be QC-variable_list of k, A;

      

       A1: (P ! l) is atomic;

      then ( the_arguments_of (P ! l)) = l by QC_LANG1:def 23;

      hence thesis by A1, Th36;

    end;

    theorem :: QC_LANG3:38

    p is negative implies ( Vars (p,V)) = ( Vars (( the_argument_of p),V)) by Lm2;

    theorem :: QC_LANG3:39

    

     Th39: ( Vars (( 'not' p),V)) = ( Vars (p,V))

    proof

      set 9p = ( 'not' p);

      

       A1: 9p is negative;

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

      hence thesis by A1, Lm2;

    end;

    theorem :: QC_LANG3:40

    

     Th40: ( Vars (( FALSUM A),V)) = {}

    proof

      ( FALSUM A) = ( 'not' ( VERUM A)) by QC_LANG2:def 1;

      

      hence ( Vars (( FALSUM A),V)) = ( Vars (( VERUM A),V)) by Th39

      .= {} by Lm2;

    end;

    theorem :: QC_LANG3:41

    p is conjunctive implies ( Vars (p,V)) = (( Vars (( the_left_argument_of p),V)) \/ ( Vars (( the_right_argument_of p),V))) by Lm2;

    theorem :: QC_LANG3:42

    

     Th42: ( Vars ((p '&' q),V)) = (( Vars (p,V)) \/ ( Vars (q,V)))

    proof

      set pq = (p '&' q);

      

       A1: (p '&' q) is conjunctive;

      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, Lm2;

    end;

    theorem :: QC_LANG3:43

    p is universal implies ( Vars (p,V)) = ( Vars (( the_scope_of p),V)) by Lm2;

    theorem :: QC_LANG3:44

    

     Th44: ( Vars (( All (x,p)),V)) = ( Vars (p,V))

    proof

      

       A1: ( All (x,p)) is universal;

      then ( the_scope_of ( All (x,p))) = p by QC_LANG1:def 28;

      hence thesis by A1, Lm2;

    end;

    theorem :: QC_LANG3:45

    

     Th45: p is disjunctive implies ( Vars (p,V)) = (( Vars (( the_left_disjunct_of p),V)) \/ ( Vars (( the_right_disjunct_of p),V)))

    proof

      set p1 = ( the_left_disjunct_of p);

      set p2 = ( the_right_disjunct_of p);

      assume p is disjunctive;

      then p = (p1 'or' p2) by QC_LANG2: 37;

      then p = ( 'not' (( 'not' p1) '&' ( 'not' p2))) by QC_LANG2:def 3;

      

      hence ( Vars (p,V)) = ( Vars ((( 'not' p1) '&' ( 'not' p2)),V)) by Th39

      .= (( Vars (( 'not' p1),V)) \/ ( Vars (( 'not' p2),V))) by Th42

      .= (( Vars (p1,V)) \/ ( Vars (( 'not' p2),V))) by Th39

      .= (( Vars (( the_left_disjunct_of p),V)) \/ ( Vars (( the_right_disjunct_of p),V))) by Th39;

    end;

    theorem :: QC_LANG3:46

    ( Vars ((p 'or' q),V)) = (( Vars (p,V)) \/ ( Vars (q,V)))

    proof

      

       A1: ( the_right_disjunct_of (p 'or' q)) = q by QC_LANG2: 29;

      (p 'or' q) is disjunctive & ( the_left_disjunct_of (p 'or' q)) = p by QC_LANG2: 29, QC_LANG2:def 10;

      hence thesis by A1, Th45;

    end;

    theorem :: QC_LANG3:47

    

     Th47: p is conditional implies ( Vars (p,V)) = (( Vars (( the_antecedent_of p),V)) \/ ( Vars (( the_consequent_of p),V)))

    proof

      set p1 = ( the_antecedent_of p);

      set p2 = ( the_consequent_of p);

      assume p is conditional;

      then p = (p1 => p2) by QC_LANG2: 38;

      then p = ( 'not' (p1 '&' ( 'not' p2))) by QC_LANG2:def 2;

      

      hence ( Vars (p,V)) = ( Vars ((p1 '&' ( 'not' p2)),V)) by Th39

      .= (( Vars (p1,V)) \/ ( Vars (( 'not' p2),V))) by Th42

      .= (( Vars (( the_antecedent_of p),V)) \/ ( Vars (( the_consequent_of p),V))) by Th39;

    end;

    theorem :: QC_LANG3:48

    

     Th48: ( Vars ((p => q),V)) = (( Vars (p,V)) \/ ( Vars (q,V)))

    proof

      

       A1: ( the_consequent_of (p => q)) = q by QC_LANG2: 30;

      (p => q) is conditional & ( the_antecedent_of (p => q)) = p by QC_LANG2: 30, QC_LANG2:def 11;

      hence thesis by A1, Th47;

    end;

    theorem :: QC_LANG3:49

    

     Th49: p is biconditional implies ( Vars (p,V)) = (( Vars (( the_left_side_of p),V)) \/ ( Vars (( the_right_side_of p),V)))

    proof

      set p1 = ( the_left_side_of p);

      set p2 = ( the_right_side_of p);

      assume p is biconditional;

      then p = (p1 <=> p2) by QC_LANG2: 39;

      then p = ((p1 => p2) '&' (p2 => p1)) by QC_LANG2:def 4;

      

      hence ( Vars (p,V)) = (( Vars ((p1 => p2),V)) \/ ( Vars ((p2 => p1),V))) by Th42

      .= ((( Vars (p1,V)) \/ ( Vars (p2,V))) \/ ( Vars ((p2 => p1),V))) by Th48

      .= ((( Vars (p1,V)) \/ ( Vars (p2,V))) \/ (( Vars (p1,V)) \/ ( Vars (p2,V)))) by Th48

      .= (( Vars (( the_left_side_of p),V)) \/ ( Vars (( the_right_side_of p),V)));

    end;

    theorem :: QC_LANG3:50

    ( Vars ((p <=> q),V)) = (( Vars (p,V)) \/ ( Vars (q,V)))

    proof

      

       A1: ( the_right_side_of (p <=> q)) = q by QC_LANG2: 31;

      (p <=> q) is biconditional & ( the_left_side_of (p <=> q)) = p by QC_LANG2: 31, QC_LANG2:def 12;

      hence thesis by A1, Th49;

    end;

    theorem :: QC_LANG3:51

    p is existential implies ( Vars (p,V)) = ( Vars (( the_argument_of ( the_scope_of ( the_argument_of p))),V))

    proof

      set p1 = ( the_argument_of ( the_scope_of ( the_argument_of p)));

      set x = ( bound_in ( the_argument_of p));

      assume p is existential;

      then p = ( Ex (x,p1)) by QC_LANG2: 40;

      then p = ( 'not' ( All (x,( 'not' p1)))) by QC_LANG2:def 5;

      

      then ( Vars (p,V)) = ( Vars (( All (x,( 'not' p1))),V)) by Th39

      .= ( Vars (( 'not' p1),V)) by Th44

      .= ( Vars (p1,V)) by Th39;

      hence thesis;

    end;

    theorem :: QC_LANG3:52

    ( Vars (( Ex (x,p)),V)) = ( Vars (p,V))

    proof

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

      

      hence ( Vars (( Ex (x,p)),V)) = ( Vars (( All (x,( 'not' p))),V)) by Th39

      .= ( Vars (( 'not' p),V)) by Th44

      .= ( Vars (p,V)) by Th39;

    end;

    definition

      let A, p;

      :: QC_LANG3:def5

      func Free p -> Subset of ( free_QC-variables A) equals ( Vars (p,( free_QC-variables A)));

      correctness ;

    end

    theorem :: QC_LANG3:53

    ( Free ( VERUM A)) = {} by Lm2;

    theorem :: QC_LANG3:54

    for P be QC-pred_symbol of k, A holds for l be QC-variable_list of k, A holds ( Free (P ! l)) = { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( free_QC-variables A) } by Th37;

    theorem :: QC_LANG3:55

    ( Free ( 'not' p)) = ( Free p) by Th39;

    theorem :: QC_LANG3:56

    ( Free ( FALSUM A)) = {} by Th40;

    theorem :: QC_LANG3:57

    ( Free (p '&' q)) = (( Free p) \/ ( Free q)) by Th42;

    theorem :: QC_LANG3:58

    ( Free ( All (x,p))) = ( Free p) by Th44;

    theorem :: QC_LANG3:59

    ( Free (p 'or' q)) = (( Free p) \/ ( Free q))

    proof

      (p 'or' q) = ( 'not' (( 'not' p) '&' ( 'not' q))) by QC_LANG2:def 3;

      

      hence ( Free (p 'or' q)) = ( Free (( 'not' p) '&' ( 'not' q))) by Th39

      .= (( Free ( 'not' p)) \/ ( Free ( 'not' q))) by Th42

      .= (( Free p) \/ ( Free ( 'not' q))) by Th39

      .= (( Free p) \/ ( Free q)) by Th39;

    end;

    theorem :: QC_LANG3:60

    

     Th60: ( Free (p => q)) = (( Free p) \/ ( Free q))

    proof

      (p => q) = ( 'not' (p '&' ( 'not' q))) by QC_LANG2:def 2;

      

      hence ( Free (p => q)) = ( Free (p '&' ( 'not' q))) by Th39

      .= (( Free p) \/ ( Free ( 'not' q))) by Th42

      .= (( Free p) \/ ( Free q)) by Th39;

    end;

    theorem :: QC_LANG3:61

    ( Free (p <=> q)) = (( Free p) \/ ( Free q))

    proof

      (p <=> q) = ((p => q) '&' (q => p)) by QC_LANG2:def 4;

      

      hence ( Free (p <=> q)) = (( Free (p => q)) \/ ( Free (q => p))) by Th42

      .= ((( Free p) \/ ( Free q)) \/ ( Free (q => p))) by Th60

      .= ((( Free p) \/ ( Free q)) \/ (( Free p) \/ ( Free q))) by Th60

      .= (( Free p) \/ ( Free q));

    end;

    theorem :: QC_LANG3:62

    ( Free ( Ex (x,p))) = ( Free p)

    proof

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

      

      hence ( Free ( Ex (x,p))) = ( Free ( All (x,( 'not' p)))) by Th39

      .= ( Free ( 'not' p)) by Th44

      .= ( Free p) by Th39;

    end;

    definition

      let A, p;

      :: QC_LANG3:def6

      func Fixed p -> Subset of ( fixed_QC-variables A) equals ( Vars (p,( fixed_QC-variables A)));

      correctness ;

    end

    theorem :: QC_LANG3:63

    ( Fixed ( VERUM A)) = {} by Lm2;

    theorem :: QC_LANG3:64

    for P be QC-pred_symbol of k, A holds for l be QC-variable_list of k, A holds ( Fixed (P ! l)) = { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( fixed_QC-variables A) } by Th37;

    theorem :: QC_LANG3:65

    ( Fixed ( 'not' p)) = ( Fixed p) by Th39;

    theorem :: QC_LANG3:66

    ( Fixed ( FALSUM A)) = {}

    proof

      

      thus ( Fixed ( FALSUM A)) = ( Fixed ( 'not' ( VERUM A))) by QC_LANG2:def 1

      .= ( Fixed ( VERUM A)) by Th39

      .= {} by Lm2;

    end;

    theorem :: QC_LANG3:67

    ( Fixed (p '&' q)) = (( Fixed p) \/ ( Fixed q)) by Th42;

    theorem :: QC_LANG3:68

    ( Fixed ( All (x,p))) = ( Fixed p) by Th44;

    theorem :: QC_LANG3:69

    ( Fixed (p 'or' q)) = (( Fixed p) \/ ( Fixed q))

    proof

      (p 'or' q) = ( 'not' (( 'not' p) '&' ( 'not' q))) by QC_LANG2:def 3;

      

      hence ( Fixed (p 'or' q)) = ( Fixed (( 'not' p) '&' ( 'not' q))) by Th39

      .= (( Fixed ( 'not' p)) \/ ( Fixed ( 'not' q))) by Th42

      .= (( Fixed p) \/ ( Fixed ( 'not' q))) by Th39

      .= (( Fixed p) \/ ( Fixed q)) by Th39;

    end;

    theorem :: QC_LANG3:70

    

     Th70: ( Fixed (p => q)) = (( Fixed p) \/ ( Fixed q))

    proof

      (p => q) = ( 'not' (p '&' ( 'not' q))) by QC_LANG2:def 2;

      

      hence ( Fixed (p => q)) = ( Fixed (p '&' ( 'not' q))) by Th39

      .= (( Fixed p) \/ ( Fixed ( 'not' q))) by Th42

      .= (( Fixed p) \/ ( Fixed q)) by Th39;

    end;

    theorem :: QC_LANG3:71

    ( Fixed (p <=> q)) = (( Fixed p) \/ ( Fixed q))

    proof

      (p <=> q) = ((p => q) '&' (q => p)) by QC_LANG2:def 4;

      

      hence ( Fixed (p <=> q)) = (( Fixed (p => q)) \/ ( Fixed (q => p))) by Th42

      .= ((( Fixed p) \/ ( Fixed q)) \/ ( Fixed (q => p))) by Th70

      .= ((( Fixed p) \/ ( Fixed q)) \/ (( Fixed q) \/ ( Fixed p))) by Th70

      .= (( Fixed p) \/ ( Fixed q));

    end;

    theorem :: QC_LANG3:72

    ( Fixed ( Ex (x,p))) = ( Fixed p)

    proof

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

      

      hence ( Fixed ( Ex (x,p))) = ( Fixed ( All (x,( 'not' p)))) by Th39

      .= ( Fixed ( 'not' p)) by Th44

      .= ( Fixed p) by Th39;

    end;