valuat_1.miz



    begin

    reserve Al for QC-alphabet;

    reserve i,j,k for Nat,

A,D for non empty set;

    definition

      let Al;

      let A be set;

      :: VALUAT_1:def1

      func Valuations_in (Al,A) -> set equals ( Funcs (( bound_QC-variables Al),A));

      coherence ;

    end

    registration

      let Al, A;

      cluster ( Valuations_in (Al,A)) -> non empty functional;

      coherence ;

    end

    theorem :: VALUAT_1:1

    

     Th1: for x be set st x is Element of ( Valuations_in (Al,A)) holds x is Function of ( bound_QC-variables Al), A

    proof

      let x be set;

      assume x is Element of ( Valuations_in (Al,A));

      then ex f be Function st x = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

      hence thesis by FUNCT_2:def 1, RELSET_1: 4;

    end;

    definition

      let Al, A;

      :: original: Valuations_in

      redefine

      func Valuations_in (Al,A) -> FUNCTION_DOMAIN of ( bound_QC-variables Al), A ;

      coherence

      proof

        for x be Element of ( Valuations_in (Al,A)) holds x is Function of ( bound_QC-variables Al), A by Th1;

        hence thesis by FUNCT_2:def 12;

      end;

    end

    reserve f1,f2 for Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )),

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

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

    definition

      let Al, A, x;

      let p be Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

      :: VALUAT_1:def2

      func FOR_ALL (x,p) -> Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) means

      : Def2: for v holds (it . v) = ( ALL { (p . v9) where v9 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v9 . y) = (v . y) });

      existence

      proof

        deffunc F( Function) = ( ALL { (p . v9) where v9 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v9 . y) = ($1 . y) });

        consider f be Function of ( Valuations_in (Al,A)), BOOLEAN such that

         A1: for v holds (f . v) = F(v) from FUNCT_2:sch 4;

        ( dom f) = ( Valuations_in (Al,A)) & ( rng f) c= BOOLEAN by FUNCT_2:def 1, RELAT_1:def 19;

        then

        reconsider f as Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) by FUNCT_2:def 2;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1, f2;

        assume that

         A2: for v holds (f1 . v) = ( ALL { (p . v9) where v9 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v9 . y) = (v . y) }) and

         A3: for v holds (f2 . v) = ( ALL { (p . v9) where v9 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v9 . y) = (v . y) });

        for v holds (f1 . v) = (f2 . v)

        proof

          let v;

          (f1 . v) = ( ALL { (p . v9) where v9 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v9 . y) = (v . y) }) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: VALUAT_1:2

    

     Th2: for p be Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) holds (( FOR_ALL (x,p)) . v) = FALSE iff ex v1 st (p . v1) = FALSE & for y st x <> y holds (v1 . y) = (v . y)

    proof

      let p be Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

       A1:

      now

        assume ex v1 st (p . v1) = FALSE & for y st x <> y holds (v1 . y) = (v . y);

        then FALSE in { (p . v99) where v99 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v99 . y) = (v . y) };

        then ( ALL { (p . v99) where v99 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v99 . y) = (v . y) }) = FALSE by MARGREL1: 17;

        hence (( FOR_ALL (x,p)) . v) = FALSE by Def2;

      end;

      now

        assume (( FOR_ALL (x,p)) . v) = FALSE ;

        then ( ALL { (p . v99) where v99 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v99 . y) = (v . y) }) = FALSE by Def2;

        then FALSE in { (p . v99) where v99 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v99 . y) = (v . y) } by MARGREL1: 17;

        hence ex v1 st (p . v1) = FALSE & for y st x <> y holds (v1 . y) = (v . y);

      end;

      hence thesis by A1;

    end;

    theorem :: VALUAT_1:3

    

     Th3: for p be Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) holds (( FOR_ALL (x,p)) . v) = TRUE iff for v1 st for y st x <> y holds (v1 . y) = (v . y) holds (p . v1) = TRUE

    proof

      let p be Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

       A1:

      now

        assume (( FOR_ALL (x,p)) . v) = TRUE ;

        then ( ALL { (p . v99) where v99 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v99 . y) = (v . y) }) = TRUE by Def2;

        then

         A2: not FALSE in { (p . v99) where v99 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v99 . y) = (v . y) } by MARGREL1: 17;

        thus for v1 st for y st x <> y holds (v1 . y) = (v . y) holds (p . v1) = TRUE

        proof

          let v1;

          assume for y st x <> y holds (v1 . y) = (v . y);

          then not (p . v1) = FALSE by A2;

          hence thesis by XBOOLEAN:def 3;

        end;

      end;

      now

        assume for v1 st for y st x <> y holds (v1 . y) = (v . y) holds (p . v1) = TRUE ;

        then not ex v1 st (p . v1) = FALSE & for y st x <> y holds (v1 . y) = (v . y);

        then not FALSE in { (p . v99) where v99 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v99 . y) = (v . y) };

        then ( ALL { (p . v99) where v99 be Element of ( Valuations_in (Al,A)) : for y st x <> y holds (v99 . y) = (v . y) }) = TRUE by MARGREL1: 17;

        hence (( FOR_ALL (x,p)) . v) = TRUE by Def2;

      end;

      hence thesis by A1;

    end;

    reserve ll for CQC-variable_list of k, Al;

    notation

      let Al, A, k, ll, v;

      synonym v *' ll for v * ll;

    end

    definition

      let Al;

      let A, k, ll, v;

      :: original: *'

      redefine

      :: VALUAT_1:def3

      func v *' ll -> FinSequence of A means

      : Def3: ( len it ) = k & for i be Nat st 1 <= i & i <= k holds (it . i) = (v . (ll . i));

      coherence

      proof

        ( rng v) c= A & ( rng (v * ll)) c= ( rng v) by RELAT_1: 26, RELAT_1:def 19;

        then

         A1: ( rng (v * ll)) c= A by XBOOLE_1: 1;

        

         A2: ( len ll) = k by CARD_1:def 7;

        ( dom v) = ( bound_QC-variables Al) by FUNCT_2:def 1;

        then ( rng ll) c= ( dom v) by RELAT_1:def 19;

        

        then ( dom (v * ll)) = ( dom ll) by RELAT_1: 27

        .= ( Seg k) by A2, FINSEQ_1:def 3;

        then (v * ll) is FinSequence-like by FINSEQ_1:def 2;

        hence thesis by A1, FINSEQ_1:def 4;

      end;

      compatibility

      proof

        let IT be FinSequence of A;

        

         A3: ( len ll) = k by CARD_1:def 7;

        ( dom v) = ( bound_QC-variables Al) by FUNCT_2:def 1;

        then

         A4: ( rng ll) c= ( dom v) by RELAT_1:def 19;

        thus IT = (v * ll) implies ( len IT) = k & for i be Nat st 1 <= i & i <= k holds (IT . i) = (v . (ll . i))

        proof

          assume

           A5: IT = (v * ll);

          then

           A6: ( dom ll) = ( dom IT) by A4, RELAT_1: 27;

          hence ( len IT) = k by A3, FINSEQ_3: 29;

          let i be Nat;

          assume 1 <= i & i <= k;

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

          hence thesis by A5, FUNCT_1: 12;

        end;

        assume that

         A7: ( len IT) = k and

         A8: for i be Nat st 1 <= i & i <= k holds (IT . i) = (v . (ll . i));

        

         A9: for x be object holds x in ( dom IT) iff x in ( dom ll) & (ll . x) in ( dom v)

        proof

          let x be object;

          thus x in ( dom IT) implies x in ( dom ll) & (ll . x) in ( dom v)

          proof

            assume x in ( dom IT);

            hence x in ( dom ll) by A3, A7, FINSEQ_3: 29;

            then (ll . x) in ( rng ll) by FUNCT_1:def 3;

            hence thesis by A4;

          end;

          assume that

           A10: x in ( dom ll) and (ll . x) in ( dom v);

          thus thesis by A3, A7, A10, FINSEQ_3: 29;

        end;

        for x be object st x in ( dom IT) holds (IT . x) = (v . (ll . x))

        proof

          let x be object;

          assume

           A11: x in ( dom IT);

          then

          reconsider i = x as Element of NAT ;

          1 <= i & i <= k by A7, A11, FINSEQ_3: 25;

          hence thesis by A8;

        end;

        hence thesis by A9, FUNCT_1: 10;

      end;

    end

    definition

      let Al;

      let A, k, ll;

      let r be Element of ( relations_on A);

      :: VALUAT_1:def4

      func ll 'in' r -> Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) means

      : Def4: for v be Element of ( Valuations_in (Al,A)) holds ((v *' ll) in r iff (it . v) = TRUE ) & ( not (v *' ll) in r iff (it . v) = FALSE );

      existence

      proof

        defpred C[ object] means ex v be Element of ( Valuations_in (Al,A)) st $1 = v & (v *' ll) in r;

        deffunc T( object) = TRUE ;

        deffunc F( object) = FALSE ;

        

         A1: for x be object st x in ( Valuations_in (Al,A)) holds ( C[x] implies T(x) in BOOLEAN ) & ( not C[x] implies F(x) in BOOLEAN );

        consider f be Function of ( Valuations_in (Al,A)), BOOLEAN such that

         A2: for x be object st x in ( Valuations_in (Al,A)) holds ( C[x] implies (f . x) = T(x)) & ( not C[x] implies (f . x) = F(x)) from FUNCT_2:sch 5( A1);

        ( dom f) = ( Valuations_in (Al,A)) & ( rng f) c= BOOLEAN by FUNCT_2:def 1, RELAT_1:def 19;

        then

        reconsider f as Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) by FUNCT_2:def 2;

        take f;

        let v be Element of ( Valuations_in (Al,A));

         not (ex v9 be Element of ( Valuations_in (Al,A)) st v = v9 & (v9 *' ll) in r) implies (f . v) = FALSE by A2;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

        assume that

         A3: for v be Element of ( Valuations_in (Al,A)) holds ((v *' ll) in r iff (f1 . v) = TRUE ) & ( not (v *' ll) in r iff (f1 . v) = FALSE ) and

         A4: for v be Element of ( Valuations_in (Al,A)) holds ((v *' ll) in r iff (f2 . v) = TRUE ) & ( not (v *' ll) in r iff (f2 . v) = FALSE );

        for v be Element of ( Valuations_in (Al,A)) holds (f1 . v) = (f2 . v)

        proof

          let v be Element of ( Valuations_in (Al,A));

          per cases ;

            suppose

             A5: (v *' ll) in r;

            then (f1 . v) = TRUE by A3;

            hence thesis by A4, A5;

          end;

            suppose

             A6: not (v *' ll) in r;

            then (f1 . v) = FALSE by A3;

            hence thesis by A4, A6;

          end;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let Al, A;

      let F be Function of ( CQC-WFF Al), ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

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

      :: original: .

      redefine

      func F . p -> Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) ;

      coherence

      proof

        thus (F . p) is Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

      end;

    end

    definition

      let Al, D;

      :: VALUAT_1:def5

      mode interpretation of Al,D -> Function of ( QC-pred_symbols Al), ( relations_on D) means for P be Element of ( QC-pred_symbols Al), r be Element of ( relations_on D) st (it . P) = r holds r = ( empty_rel D) or ( the_arity_of P) = ( the_arity_of r);

      existence

      proof

        reconsider F1 = (( QC-pred_symbols Al) --> ( empty_rel D)) as Function of ( QC-pred_symbols Al), ( relations_on D);

        take F1;

        let P be Element of ( QC-pred_symbols Al);

        thus thesis by FUNCOP_1: 7;

      end;

    end

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

J for interpretation of Al, A,

P for QC-pred_symbol of k, Al,

r for Element of ( relations_on A);

    definition

      let Al, A, k, J, P;

      :: original: .

      redefine

      func J . P -> Element of ( relations_on A) ;

      coherence by FUNCT_2: 5;

    end

    definition

      let Al, A, J, p;

      :: VALUAT_1:def6

      func Valid (p,J) -> Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) means

      : Def6: ex F be Function of ( CQC-WFF Al), ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) st it = (F . p) & (F . ( VERUM Al)) = (( Valuations_in (Al,A)) --> TRUE ) & for p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al holds (F . (P ! ll)) = (ll 'in' (J . P)) & (F . ( 'not' p)) = ( 'not' (F . p)) & (F . (p '&' q)) = ((F . p) '&' (F . q)) & (F . ( All (x,p))) = ( FOR_ALL (x,(F . p)));

      existence

      proof

        deffunc A( Nat, QC-pred_symbol of $1, Al, CQC-variable_list of $1, Al) = ($3 'in' (J . $2));

        set D = ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

        set V = ( In ((( Valuations_in (Al,A)) --> TRUE ),D));

        deffunc N( Element of D) = ( In (( 'not' $1),D));

        deffunc C( Element of D, Element of D) = ( In (($1 '&' $2),D));

        deffunc Q( bound_QC-variable of Al, Element of D) = ( In (( FOR_ALL ($1,$2)),D));

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

         A1: (F . ( VERUM Al)) = V and

         A2: for r,s be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat 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 CQC_LANG:sch 2;

        take (F . p), F;

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

        (( Valuations_in (Al,A)) --> TRUE ) in D by FUNCT_2: 8;

        hence (F . ( VERUM Al)) = (( Valuations_in (Al,A)) --> TRUE ) by A1, SUBSET_1:def 8;

        let p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al;

        thus (F . (P ! ll)) = (ll 'in' (J . P)) by A2;

        

         A3: ( 'not' (F . p)) in D by FUNCT_2: 8;

        

        thus (F . ( 'not' p)) = N(.) by A2

        .= ( 'not' (F . p)) by A3, SUBSET_1:def 8;

        

         A4: ((F . p) '&' (F . q)) in D by FUNCT_2: 8;

        

        thus (F . (p '&' q)) = C(.,.) by A2

        .= ((F . p) '&' (F . q)) by A4, SUBSET_1:def 8;

        

        thus (F . ( All (x,p))) = Q(x,.) by A2

        .= ( FOR_ALL (x,(F . p))) by SUBSET_1:def 8;

      end;

      uniqueness

      proof

        deffunc A( Nat, QC-pred_symbol of $1, Al, CQC-variable_list of $1, Al) = ($3 'in' (J . $2));

        set D = ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

        set V = ( In ((( Valuations_in (Al,A)) --> TRUE ),D));

        deffunc N( Element of D) = ( In (( 'not' $1),D));

        deffunc C( Element of D, Element of D) = ( In (($1 '&' $2),D));

        deffunc Q( bound_QC-variable of Al, Element of D) = ( In (( FOR_ALL ($1,$2)),D));

        let d1,d2 be Element of D;

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

         A5: d1 = (F1 . p) and

         A6: (F1 . ( VERUM Al)) = (( Valuations_in (Al,A)) --> TRUE ) and

         A7: for r,s be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat 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)) = ( 'not' (F1 . r)) & (F1 . (r '&' s)) = ((F1 . r) '&' (F1 . s)) & (F1 . ( All (x,r))) = ( FOR_ALL (x,(F1 . r)));

         A8:

        now

          thus (F1 . ( VERUM Al)) = V by A6, SUBSET_1:def 8;

          let r,s be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, l be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al;

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

          

           A9: ( 'not' (F1 . r)) in D by FUNCT_2: 8;

          

          thus (F1 . ( 'not' r)) = ( 'not' (F1 . r)) by A7

          .= N(.) by A9, SUBSET_1:def 8;

          

           A10: ((F1 . r) '&' (F1 . s)) in D by FUNCT_2: 8;

          

          thus (F1 . (r '&' s)) = ((F1 . r) '&' (F1 . s)) by A7

          .= C(.,.) by A10, SUBSET_1:def 8;

          

          thus (F1 . ( All (x,r))) = ( FOR_ALL (x,(F1 . r))) by A7

          .= Q(x,.) by SUBSET_1:def 8;

        end;

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

         A11: d2 = (F2 . p) and

         A12: (F2 . ( VERUM Al)) = (( Valuations_in (Al,A)) --> TRUE ) and

         A13: for r,s be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat 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)) = ( 'not' (F2 . r)) & (F2 . (r '&' s)) = ((F2 . r) '&' (F2 . s)) & (F2 . ( All (x,r))) = ( FOR_ALL (x,(F2 . r)));

         A14:

        now

          thus (F2 . ( VERUM Al)) = V by A12, SUBSET_1:def 8;

          let r,s be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, l be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al;

          thus (F2 . (P ! l)) = A(k,P,l) by A13;

          

           A15: ( 'not' (F2 . r)) in D by FUNCT_2: 8;

          

          thus (F2 . ( 'not' r)) = ( 'not' (F2 . r)) by A13

          .= N(.) by A15, SUBSET_1:def 8;

          

           A16: ((F2 . r) '&' (F2 . s)) in D by FUNCT_2: 8;

          

          thus (F2 . (r '&' s)) = ((F2 . r) '&' (F2 . s)) by A13

          .= C(.,.) by A16, SUBSET_1:def 8;

          

          thus (F2 . ( All (x,r))) = ( FOR_ALL (x,(F2 . r))) by A13

          .= Q(x,.) by SUBSET_1:def 8;

        end;

        F1 = F2 from CQC_LANG:sch 3( A8, A14);

        hence thesis by A5, A11;

      end;

    end

    

     Lm1: for A, J holds ( Valid (( VERUM Al),J)) = (( Valuations_in (Al,A)) --> TRUE ) & (for k, ll, P holds ( Valid ((P ! ll),J)) = (ll 'in' (J . P))) & (for p holds ( Valid (( 'not' p),J)) = ( 'not' ( Valid (p,J)))) & (for q holds ( Valid ((p '&' q),J)) = (( Valid (p,J)) '&' ( Valid (q,J)))) & for x holds ( Valid (( All (x,p)),J)) = ( FOR_ALL (x,( Valid (p,J))))

    proof

      let A, J;

      set D = ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

      set V = ( In ((( Valuations_in (Al,A)) --> TRUE ),D));

      deffunc A( Nat, QC-pred_symbol of $1, Al, CQC-variable_list of $1, Al) = ($3 'in' (J . $2));

      deffunc N( Element of D) = ( In (( 'not' $1),D));

      deffunc C( Element of D, Element of D) = ( In (($1 '&' $2),D));

      deffunc Q( bound_QC-variable of Al, Element of D) = ( In (( FOR_ALL ($1,$2)),D));

      deffunc X( Element of ( CQC-WFF Al)) = ( Valid ($1,J));

      

       A1: for p holds for d be Element of D holds d = X(p) iff ex F be Function of ( CQC-WFF Al), D st d = (F . p) & (F . ( VERUM Al)) = V & for p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al holds (F . (P ! ll)) = A(k,P,ll) & (F . ( 'not' p)) = N(.) & (F . (p '&' q)) = C(.,.) & (F . ( All (x,p))) = Q(x,.)

      proof

        let p;

        let d be Element of D;

        thus d = X(p) implies ex F be Function of ( CQC-WFF Al), D st d = (F . p) & (F . ( VERUM Al)) = V & for p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al holds (F . (P ! ll)) = A(k,P,ll) & (F . ( 'not' p)) = N(.) & (F . (p '&' q)) = C(.,.) & (F . ( All (x,p))) = Q(x,.)

        proof

          assume d = X(p);

          then

          consider F be Function of ( CQC-WFF Al), ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) such that

           A2: d = (F . p) and

           A3: (F . ( VERUM Al)) = (( Valuations_in (Al,A)) --> TRUE ) and

           A4: for p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al holds (F . (P ! ll)) = (ll 'in' (J . P)) & (F . ( 'not' p)) = ( 'not' (F . p)) & (F . (p '&' q)) = ((F . p) '&' (F . q)) & (F . ( All (x,p))) = ( FOR_ALL (x,(F . p))) by Def6;

          take F;

          thus d = (F . p) by A2;

          thus (F . ( VERUM Al)) = V by A3, SUBSET_1:def 8;

          let p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al;

          thus (F . (P ! ll)) = A(k,P,ll) by A4;

          

           A5: ( 'not' (F . p)) in D by FUNCT_2: 8;

          

          thus (F . ( 'not' p)) = ( 'not' (F . p)) by A4

          .= N(.) by A5, SUBSET_1:def 8;

          

           A6: ((F . p) '&' (F . q)) in D by FUNCT_2: 8;

          

          thus (F . (p '&' q)) = ((F . p) '&' (F . q)) by A4

          .= C(.,.) by A6, SUBSET_1:def 8;

          

          thus (F . ( All (x,p))) = ( FOR_ALL (x,(F . p))) by A4

          .= Q(x,.) by SUBSET_1:def 8;

        end;

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

         A7: d = (F . p) and

         A8: (F . ( VERUM Al)) = V and

         A9: for p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al holds (F . (P ! ll)) = A(k,P,ll) & (F . ( 'not' p)) = N(.) & (F . (p '&' q)) = C(.,.) & (F . ( All (x,p))) = Q(x,.);

        (( Valuations_in (Al,A)) --> TRUE ) in D by FUNCT_2: 8;

        then

         A10: (F . ( VERUM Al)) = (( Valuations_in (Al,A)) --> TRUE ) by A8, SUBSET_1:def 8;

        for p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al holds (F . (P ! ll)) = A(k,P,ll) & (F . ( 'not' p)) = ( 'not' (F . p)) & (F . (p '&' q)) = ((F . p) '&' (F . q)) & (F . ( All (x,p))) = ( FOR_ALL (x,(F . p)))

        proof

          let p,q be Element of ( CQC-WFF Al), x be bound_QC-variable of Al, k be Nat, ll be CQC-variable_list of k, Al, P be QC-pred_symbol of k, Al;

          thus (F . (P ! ll)) = A(k,P,ll) by A9;

          

           A11: ( 'not' (F . p)) in D by FUNCT_2: 8;

          

          thus (F . ( 'not' p)) = N(.) by A9

          .= ( 'not' (F . p)) by A11, SUBSET_1:def 8;

          

           A12: ((F . p) '&' (F . q)) in D by FUNCT_2: 8;

          

          thus (F . (p '&' q)) = C(.,.) by A9

          .= ((F . p) '&' (F . q)) by A12, SUBSET_1:def 8;

          

          thus (F . ( All (x,p))) = Q(x,.) by A9

          .= ( FOR_ALL (x,(F . p))) by SUBSET_1:def 8;

        end;

        hence d = X(p) by A7, A10, Def6;

      end;

      

       A13: (( Valuations_in (Al,A)) --> TRUE ) in D by FUNCT_2: 8;

       X(VERUM) = V from CQC_LANG:sch 5( A1);

      hence X(VERUM) = (( Valuations_in (Al,A)) --> TRUE ) by A13, SUBSET_1:def 8;

      hereby

        let k, ll, P;

        thus X(!) = A(k,P,ll) from CQC_LANG:sch 6( A1);

      end;

      hereby

        let p;

        

         A14: ( 'not' X(p)) in D by FUNCT_2: 8;

         X('not') = N(X) from CQC_LANG:sch 7( A1);

        hence X('not') = ( 'not' X(p)) by A14, SUBSET_1:def 8;

      end;

      hereby

        let q;

        

         A15: ( X(p) '&' X(q)) in D by FUNCT_2: 8;

         X('&') = C(X,X) from CQC_LANG:sch 8( A1);

        hence X('&') = ( X(p) '&' X(q)) by A15, SUBSET_1:def 8;

      end;

      let x;

       X(All) = Q(x,X) from CQC_LANG:sch 9( A1);

      hence X(All) = ( FOR_ALL (x, X(p))) by SUBSET_1:def 8;

    end;

    theorem :: VALUAT_1:4

    ( Valid (( VERUM Al),J)) = (( Valuations_in (Al,A)) --> TRUE ) by Lm1;

    theorem :: VALUAT_1:5

    

     Th5: (( Valid (( VERUM Al),J)) . v) = TRUE

    proof

      ((( Valuations_in (Al,A)) --> TRUE ) . v) = TRUE by FUNCOP_1: 7;

      hence thesis by Lm1;

    end;

    theorem :: VALUAT_1:6

    ( Valid ((P ! ll),J)) = (ll 'in' (J . P)) by Lm1;

    theorem :: VALUAT_1:7

    

     Th7: p = (P ! ll) & r = (J . P) implies ((v *' ll) in r iff (( Valid (p,J)) . v) = TRUE )

    proof

      assume that

       A1: p = (P ! ll) and

       A2: r = (J . P);

       A3:

      now

        assume (( Valid (p,J)) . v) = TRUE ;

        then ((ll 'in' (J . P)) . v) <> FALSE by A1, Lm1;

        hence (v *' ll) in r by A2, Def4;

      end;

      now

        assume (v *' ll) in r;

        then ((ll 'in' (J . P)) . v) = TRUE by A2, Def4;

        hence (( Valid (p,J)) . v) = TRUE by A1, Lm1;

      end;

      hence thesis by A3;

    end;

    theorem :: VALUAT_1:8

    

     Th8: p = (P ! ll) & r = (J . P) implies ( not (v *' ll) in r iff (( Valid (p,J)) . v) = FALSE )

    proof

      assume that

       A1: p = (P ! ll) and

       A2: r = (J . P);

       A3:

      now

        assume (( Valid (p,J)) . v) = FALSE ;

        then ((ll 'in' (J . P)) . v) <> TRUE by A1, Lm1;

        hence not (v *' ll) in r by A2, Def4;

      end;

      now

        assume not (v *' ll) in r;

        then ((ll 'in' (J . P)) . v) = FALSE by A2, Def4;

        hence (( Valid (p,J)) . v) = FALSE by A1, Lm1;

      end;

      hence thesis by A3;

    end;

    theorem :: VALUAT_1:9

    ( Valid (( 'not' p),J)) = ( 'not' ( Valid (p,J))) by Lm1;

    theorem :: VALUAT_1:10

    

     Th10: (( Valid (( 'not' p),J)) . v) = ( 'not' (( Valid (p,J)) . v))

    proof

      (( Valid (( 'not' p),J)) . v) = (( 'not' ( Valid (p,J))) . v) by Lm1;

      hence thesis by MARGREL1:def 19;

    end;

    theorem :: VALUAT_1:11

    ( Valid ((p '&' q),J)) = (( Valid (p,J)) '&' ( Valid (q,J))) by Lm1;

    theorem :: VALUAT_1:12

    

     Th12: (( Valid ((p '&' q),J)) . v) = ((( Valid (p,J)) . v) '&' (( Valid (q,J)) . v))

    proof

      (( Valid ((p '&' q),J)) . v) = ((( Valid (p,J)) '&' ( Valid (q,J))) . v) by Lm1;

      hence thesis by MARGREL1:def 20;

    end;

    theorem :: VALUAT_1:13

    ( Valid (( All (x,p)),J)) = ( FOR_ALL (x,( Valid (p,J)))) by Lm1;

    theorem :: VALUAT_1:14

    

     Th14: (( Valid ((p '&' ( 'not' p)),J)) . v) = FALSE

    proof

       A1:

      now

        assume (( Valid (p,J)) . v) = TRUE ;

        then ( 'not' (( Valid (p,J)) . v)) = FALSE by MARGREL1: 11;

        hence ((( Valid (p,J)) . v) '&' ( 'not' (( Valid (p,J)) . v))) = FALSE by MARGREL1: 12;

      end;

      

       A2: (( Valid (p,J)) . v) = FALSE implies ((( Valid (p,J)) . v) '&' ( 'not' (( Valid (p,J)) . v))) = FALSE by MARGREL1: 12;

      (( Valid ((p '&' ( 'not' p)),J)) . v) = ((( Valid (p,J)) . v) '&' (( Valid (( 'not' p),J)) . v)) by Th12

      .= ((( Valid (p,J)) . v) '&' ( 'not' (( Valid (p,J)) . v))) by Th10;

      hence thesis by A1, A2, XBOOLEAN:def 3;

    end;

    theorem :: VALUAT_1:15

    (( Valid (( 'not' (p '&' ( 'not' p))),J)) . v) = TRUE

    proof

      (( Valid (( 'not' (p '&' ( 'not' p))),J)) . v) = ( 'not' (( Valid ((p '&' ( 'not' p)),J)) . v)) by Th10

      .= ( 'not' FALSE ) by Th14;

      hence thesis by MARGREL1: 11;

    end;

    definition

      let Al, A, p, J, v;

      :: VALUAT_1:def7

      pred J,v |= p means

      : Def7: (( Valid (p,J)) . v) = TRUE ;

    end

    theorem :: VALUAT_1:16

    (J,v) |= (P ! ll) iff ((ll 'in' (J . P)) . v) = TRUE by Lm1;

    theorem :: VALUAT_1:17

    (J,v) |= ( 'not' p) iff not (J,v) |= p

    proof

       A1:

      now

        assume not (J,v) |= p;

        then not (( Valid (p,J)) . v) = TRUE ;

        then (( Valid (p,J)) . v) = FALSE by XBOOLEAN:def 3;

        then ( 'not' (( Valid (p,J)) . v)) = TRUE by MARGREL1: 11;

        then (( 'not' ( Valid (p,J))) . v) = TRUE by MARGREL1:def 19;

        then (( Valid (( 'not' p),J)) . v) = TRUE by Lm1;

        hence (J,v) |= ( 'not' p);

      end;

      now

        assume (J,v) |= ( 'not' p);

        then (( Valid (( 'not' p),J)) . v) = TRUE ;

        then (( 'not' ( Valid (p,J))) . v) = TRUE by Lm1;

        then ( 'not' (( Valid (p,J)) . v)) = TRUE by MARGREL1:def 19;

        then (( Valid (p,J)) . v) = FALSE by MARGREL1: 11;

        hence not (J,v) |= p;

      end;

      hence thesis by A1;

    end;

    theorem :: VALUAT_1:18

    (J,v) |= (p '&' q) iff (J,v) |= p & (J,v) |= q

    proof

       A1:

      now

        assume (J,v) |= p & (J,v) |= q;

        then (( Valid (p,J)) . v) = TRUE & (( Valid (q,J)) . v) = TRUE ;

        then ((( Valid (p,J)) . v) '&' (( Valid (q,J)) . v)) = TRUE ;

        then ((( Valid (p,J)) '&' ( Valid (q,J))) . v) = TRUE by MARGREL1:def 20;

        then (( Valid ((p '&' q),J)) . v) = TRUE by Lm1;

        hence (J,v) |= (p '&' q);

      end;

      now

        assume (J,v) |= (p '&' q);

        then (( Valid ((p '&' q),J)) . v) = TRUE ;

        then ((( Valid (p,J)) '&' ( Valid (q,J))) . v) = TRUE by Lm1;

        then ((( Valid (p,J)) . v) '&' (( Valid (q,J)) . v)) = TRUE by MARGREL1:def 20;

        then (( Valid (p,J)) . v) = TRUE & (( Valid (q,J)) . v) = TRUE by MARGREL1: 12;

        hence (J,v) |= p & (J,v) |= q;

      end;

      hence thesis by A1;

    end;

    theorem :: VALUAT_1:19

    

     Th19: (J,v) |= ( All (x,p)) iff (( FOR_ALL (x,( Valid (p,J)))) . v) = TRUE by Lm1;

    theorem :: VALUAT_1:20

    

     Th20: (J,v) |= ( All (x,p)) iff for v1 st for y st x <> y holds (v1 . y) = (v . y) holds (( Valid (p,J)) . v1) = TRUE

    proof

      hereby

        assume (J,v) |= ( All (x,p));

        then (( FOR_ALL (x,( Valid (p,J)))) . v) = TRUE by Th19;

        hence for v1 st for y st x <> y holds (v1 . y) = (v . y) holds (( Valid (p,J)) . v1) = TRUE by Th3;

      end;

      assume for v1 st for y st x <> y holds (v1 . y) = (v . y) holds (( Valid (p,J)) . v1) = TRUE ;

      then (( FOR_ALL (x,( Valid (p,J)))) . v) = TRUE by Th3;

      hence thesis by Th19;

    end;

    theorem :: VALUAT_1:21

    ( Valid (( 'not' ( 'not' p)),J)) = ( Valid (p,J))

    proof

      now

        let v;

        

        thus (( Valid (( 'not' ( 'not' p)),J)) . v) = ( 'not' (( Valid (( 'not' p),J)) . v)) by Th10

        .= ( 'not' ( 'not' (( Valid (p,J)) . v))) by Th10

        .= (( Valid (p,J)) . v);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: VALUAT_1:22

    

     Th22: ( Valid ((p '&' p),J)) = ( Valid (p,J))

    proof

      now

        let v;

        

        thus (( Valid ((p '&' p),J)) . v) = ((( Valid (p,J)) . v) '&' (( Valid (p,J)) . v)) by Th12

        .= (( Valid (p,J)) . v);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: VALUAT_1:23

    

     Th23: (J,v) |= (p => q) iff (( Valid (p,J)) . v) = FALSE or (( Valid (q,J)) . v) = TRUE

    proof

       A1:

      now

         A2:

        now

          assume

           A3: (( Valid (q,J)) . v) = TRUE ;

          assume not (J,v) |= (p => q);

          then (( Valid ((p => q),J)) . v) <> TRUE ;

          then (( Valid ((p => q),J)) . v) = FALSE by XBOOLEAN:def 3;

          then (( Valid (( 'not' (p '&' ( 'not' q))),J)) . v) = FALSE by QC_LANG2:def 2;

          then ( 'not' (( Valid ((p '&' ( 'not' q)),J)) . v)) = FALSE by Th10;

          then (( Valid ((p '&' ( 'not' q)),J)) . v) = TRUE by MARGREL1: 11;

          then ((( Valid (p,J)) . v) '&' (( Valid (( 'not' q),J)) . v)) = TRUE by Th12;

          then ((( Valid (p,J)) . v) '&' ( 'not' (( Valid (q,J)) . v))) = TRUE by Th10;

          then ( 'not' (( Valid (q,J)) . v)) = TRUE by MARGREL1: 12;

          hence contradiction by A3, MARGREL1: 11;

        end;

         A4:

        now

          assume (( Valid (p,J)) . v) = FALSE ;

          then ((( Valid (p,J)) . v) '&' (( Valid (( 'not' q),J)) . v)) = FALSE by MARGREL1: 12;

          then (( Valid ((p '&' ( 'not' q)),J)) . v) = FALSE by Th12;

          then ( 'not' (( Valid ((p '&' ( 'not' q)),J)) . v)) = TRUE by MARGREL1: 11;

          then (( Valid (( 'not' (p '&' ( 'not' q))),J)) . v) = TRUE by Th10;

          then (( Valid ((p => q),J)) . v) = TRUE by QC_LANG2:def 2;

          hence (J,v) |= (p => q);

        end;

        assume (( Valid (p,J)) . v) = FALSE or (( Valid (q,J)) . v) = TRUE ;

        hence (J,v) |= (p => q) by A4, A2;

      end;

      now

        assume (J,v) |= (p => q);

        then (( Valid ((p => q),J)) . v) = TRUE ;

        then (( Valid (( 'not' (p '&' ( 'not' q))),J)) . v) = TRUE by QC_LANG2:def 2;

        then ( 'not' (( Valid ((p '&' ( 'not' q)),J)) . v)) = TRUE by Th10;

        then (( Valid ((p '&' ( 'not' q)),J)) . v) = FALSE by MARGREL1: 11;

        then ((( Valid (p,J)) . v) '&' (( Valid (( 'not' q),J)) . v)) = FALSE by Th12;

        then ((( Valid (p,J)) . v) '&' ( 'not' (( Valid (q,J)) . v))) = FALSE by Th10;

        then (( Valid (p,J)) . v) = FALSE or ( 'not' (( Valid (q,J)) . v)) = FALSE by MARGREL1: 12;

        hence (( Valid (p,J)) . v) = FALSE or (( Valid (q,J)) . v) = TRUE by MARGREL1: 11;

      end;

      hence thesis by A1;

    end;

    theorem :: VALUAT_1:24

    

     Th24: (J,v) |= (p => q) iff ((J,v) |= p implies (J,v) |= q)

    proof

      thus (J,v) |= (p => q) & (J,v) |= p implies (J,v) |= q by Th23;

      assume (J,v) |= p implies (J,v) |= q;

      then (( Valid (p,J)) . v) = TRUE implies (( Valid (q,J)) . v) = TRUE ;

      then (( Valid (p,J)) . v) = FALSE or (( Valid (q,J)) . v) = TRUE by XBOOLEAN:def 3;

      hence thesis by Th23;

    end;

    theorem :: VALUAT_1:25

    

     Th25: for p be Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN )) holds (( FOR_ALL (x,p)) . v) = TRUE implies (p . v) = TRUE

    proof

      let p be Element of ( Funcs (( Valuations_in (Al,A)), BOOLEAN ));

      for y st x <> y holds (v . y) = (v . y);

      hence thesis by Th3;

    end;

    definition

      let Al, A, J, p;

      :: VALUAT_1:def8

      pred J |= p means for v holds (J,v) |= p;

    end

    reserve u,w,z for Element of BOOLEAN ;

    

     Lm2: ( 'not' (( 'not' (u '&' ( 'not' w))) '&' (( 'not' (w '&' z)) '&' (u '&' z)))) = TRUE

    proof

      per cases by XBOOLEAN:def 3;

        suppose z = TRUE & w = TRUE ;

        then ( 'not' (w '&' z)) = FALSE by MARGREL1: 11;

        then (( 'not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1: 12;

        then (( 'not' (u '&' ( 'not' w))) '&' (( 'not' (w '&' z)) '&' (u '&' z))) = FALSE by MARGREL1: 12;

        hence thesis by MARGREL1: 11;

      end;

        suppose that

         A1: w = FALSE and

         A2: u = TRUE ;

        ( 'not' w) = TRUE by A1, MARGREL1: 11;

        then ( 'not' (u '&' ( 'not' w))) = FALSE by A2, MARGREL1: 11;

        then (( 'not' (u '&' ( 'not' w))) '&' (( 'not' (w '&' z)) '&' (u '&' z))) = FALSE by MARGREL1: 12;

        hence thesis by MARGREL1: 11;

      end;

        suppose u = FALSE ;

        then (u '&' z) = FALSE by MARGREL1: 12;

        then (( 'not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1: 12;

        then (( 'not' (u '&' ( 'not' w))) '&' (( 'not' (w '&' z)) '&' (u '&' z))) = FALSE by MARGREL1: 12;

        hence thesis by MARGREL1: 11;

      end;

        suppose z = FALSE ;

        then (u '&' z) = FALSE by MARGREL1: 12;

        then (( 'not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1: 12;

        then (( 'not' (u '&' ( 'not' w))) '&' (( 'not' (w '&' z)) '&' (u '&' z))) = FALSE by MARGREL1: 12;

        hence thesis by MARGREL1: 11;

      end;

    end;

    reserve w,v2 for Element of ( Valuations_in (Al,A)),

z for bound_QC-variable of Al;

     Lm3:

    now

      let Al;

      let A be non empty set, Y,Z be bound_QC-variable of Al, V1,V2 be Element of ( Valuations_in (Al,A));

      thus ex v be Element of ( Valuations_in (Al,A)) st (for x be bound_QC-variable of Al st x <> Y holds (v . x) = (V1 . x)) & (v . Y) = (V2 . Z)

      proof

        deffunc G( object) = (V2 . Z);

        deffunc F( object) = (V1 . $1);

        defpred C[ object] means for x1 st x1 = $1 holds x1 <> Y;

        

         A1: for x be object st x in ( bound_QC-variables Al) holds ( C[x] implies F(x) in A) & ( not C[x] implies G(x) in A) by FUNCT_2: 5;

        consider f be Function of ( bound_QC-variables Al), A such that

         A2: for x be object st x in ( bound_QC-variables Al) holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from FUNCT_2:sch 5( A1);

        ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 1, RELAT_1:def 19;

        then

        reconsider f as Element of ( Valuations_in (Al,A)) by FUNCT_2:def 2;

        take f;

        now

          let x be bound_QC-variable of Al;

          now

            assume

             A3: x <> Y;

            (for x1 st x1 = x holds x1 <> Y) implies (f . x) = (V1 . x) by A2;

            hence (f . x) = (V1 . x) by A3;

          end;

          hence x <> Y implies (f . x) = (V1 . x);

          thus x = Y implies (f . Y) = (V2 . Z) by A2;

        end;

        hence thesis;

      end;

    end;

    theorem :: VALUAT_1:26

    for A be non empty set, Y,Z be bound_QC-variable of Al, V1,V2 be Element of ( Valuations_in (Al,A)) holds ex v be Element of ( Valuations_in (Al,A)) st (for x be bound_QC-variable of Al st x <> Y holds (v . x) = (V1 . x)) & (v . Y) = (V2 . Z) by Lm3;

    theorem :: VALUAT_1:27

    

     Th27: not x in ( still_not-bound_in p) implies for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (p,J)) . w)

    proof

      defpred PP[ Element of ( CQC-WFF Al)] means not x in ( still_not-bound_in $1) implies for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid ($1,J)) . v) = (( Valid ($1,J)) . w);

       A1:

      now

        let s, t, y, k, ll, P;

        thus PP[( VERUM Al)]

        proof

          assume not x in ( still_not-bound_in ( VERUM Al));

          thus for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid (( VERUM Al),J)) . v) = (( Valid (( VERUM Al),J)) . w)

          proof

            let v, w such that for y st x <> y holds (w . y) = (v . y);

            (( Valid (( VERUM Al),J)) . v) = TRUE by Th5;

            hence thesis by Th5;

          end;

        end;

        

         A2: ( rng ll) c= ( bound_QC-variables Al) by RELAT_1:def 19;

        thus PP[(P ! ll)]

        proof

          assume

           A3: not x in ( still_not-bound_in (P ! ll));

          thus for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid ((P ! ll),J)) . v) = (( Valid ((P ! ll),J)) . w)

          proof

            let v, w such that

             A4: for y st x <> y holds (w . y) = (v . y);

             A5:

            now

              

               A6: ( len (v *' ll)) = k by Def3;

               A7:

              now

                let i be Nat;

                assume

                 A8: 1 <= i & i <= ( len (v *' ll));

                

                 A9: ( len (v *' ll)) = ( len ll) by A6, CARD_1:def 7;

                then i in ( dom ll) by A8, FINSEQ_3: 25;

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

                then

                reconsider z = (ll . i) as bound_QC-variable of Al by A2;

                (ll . i) <> x

                proof

                  reconsider M = ( still_not-bound_in ll) as set;

                   not x in M by A3, QC_LANG3: 5;

                  then not x in ( variables_in (ll,( bound_QC-variables Al))) by QC_LANG3: 2;

                  then not x in { (ll . i2) where i2 be Nat : 1 <= i2 & i2 <= ( len ll) & (ll . i2) in ( bound_QC-variables Al) } by QC_LANG3:def 1;

                  hence thesis by A8, A9;

                end;

                then

                 A10: (w . z) = (v . z) by A4;

                ((v *' ll) . i) = (v . (ll . i)) by A6, A8, Def3;

                hence ((v *' ll) . i) = ((w *' ll) . i) by A6, A8, A10, Def3;

              end;

              assume

               A11: (( Valid ((P ! ll),J)) . v) = TRUE ;

              then ((ll 'in' (J . P)) . v) = TRUE by Lm1;

              then

               A12: (v *' ll) in (J . P) by Def4;

              ( len (w *' ll)) = k by Def3;

              then (w *' ll) in (J . P) by A12, A6, A7, FINSEQ_1: 14;

              then ((ll 'in' (J . P)) . w) = TRUE by Def4;

              hence thesis by A11, Lm1;

            end;

            now

              

               A13: ( len (v *' ll)) = k by Def3;

               A14:

              now

                let i be Nat;

                assume

                 A15: 1 <= i & i <= ( len (v *' ll));

                

                 A16: ( len (v *' ll)) = ( len ll) by A13, CARD_1:def 7;

                then i in ( dom ll) by A15, FINSEQ_3: 25;

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

                then

                reconsider z = (ll . i) as bound_QC-variable of Al by A2;

                (ll . i) <> x

                proof

                  reconsider M = ( still_not-bound_in ll) as set;

                   not x in M by A3, QC_LANG3: 5;

                  then not x in ( variables_in (ll,( bound_QC-variables Al))) by QC_LANG3: 2;

                  then i in NAT & not x in { (ll . i2) where i2 be Nat : 1 <= i2 & i2 <= ( len ll) & (ll . i2) in ( bound_QC-variables Al) } by ORDINAL1:def 12, QC_LANG3:def 1;

                  hence thesis by A15, A16;

                end;

                then

                 A17: (w . z) = (v . z) by A4;

                ((v *' ll) . i) = (v . (ll . i)) by A13, A15, Def3;

                hence ((v *' ll) . i) = ((w *' ll) . i) by A13, A15, A17, Def3;

              end;

              assume

               A18: (( Valid ((P ! ll),J)) . v) = FALSE ;

              then ((ll 'in' (J . P)) . v) = FALSE by Lm1;

              then

               A19: not (v *' ll) in (J . P) by Def4;

              ( len (w *' ll)) = k by Def3;

              then not (w *' ll) in (J . P) by A19, A13, A14, FINSEQ_1: 14;

              then ((ll 'in' (J . P)) . w) = FALSE by Def4;

              hence thesis by A18, Lm1;

            end;

            hence thesis by A5, XBOOLEAN:def 3;

          end;

        end;

        thus PP[s] implies PP[( 'not' s)]

        proof

          assume

           A20: ( not x in ( still_not-bound_in s) implies for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid (s,J)) . v) = (( Valid (s,J)) . w)) & not x in ( still_not-bound_in ( 'not' s));

          thus for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid (( 'not' s),J)) . v) = (( Valid (( 'not' s),J)) . w)

          proof

            let v, w such that

             A21: for y st x <> y holds (w . y) = (v . y);

             A22:

            now

              assume

               A23: (( Valid (( 'not' s),J)) . v) = FALSE ;

              then ( 'not' (( Valid (s,J)) . v)) = FALSE by Th10;

              then (( Valid (s,J)) . v) = TRUE by MARGREL1: 11;

              then (( Valid (s,J)) . w) = TRUE by A20, A21, QC_LANG3: 7;

              then ( 'not' (( Valid (s,J)) . w)) = FALSE by MARGREL1: 11;

              hence thesis by A23, Th10;

            end;

            now

              assume

               A24: (( Valid (( 'not' s),J)) . v) = TRUE ;

              then ( 'not' (( Valid (s,J)) . v)) = TRUE by Th10;

              then (( Valid (s,J)) . v) = FALSE by MARGREL1: 11;

              then (( Valid (s,J)) . w) = FALSE by A20, A21, QC_LANG3: 7;

              then ( 'not' (( Valid (s,J)) . w)) = TRUE by MARGREL1: 11;

              hence thesis by A24, Th10;

            end;

            hence thesis by A22, XBOOLEAN:def 3;

          end;

        end;

        thus PP[s] & PP[t] implies PP[(s '&' t)]

        proof

          assume that

           A25: not x in ( still_not-bound_in s) implies for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid (s,J)) . v) = (( Valid (s,J)) . w) and

           A26: not x in ( still_not-bound_in t) implies for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid (t,J)) . v) = (( Valid (t,J)) . w) and

           A27: not x in ( still_not-bound_in (s '&' t));

          

           A28: not x in (( still_not-bound_in s) \/ ( still_not-bound_in t)) by A27, QC_LANG3: 10;

          thus for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid ((s '&' t),J)) . v) = (( Valid ((s '&' t),J)) . w)

          proof

            let v, w such that

             A29: for y st x <> y holds (w . y) = (v . y);

             A30:

            now

              assume

               A31: (( Valid ((s '&' t),J)) . v) = FALSE ;

               A32:

              now

                assume (( Valid (s,J)) . v) = FALSE ;

                then (( Valid (s,J)) . w) = FALSE by A25, A28, A29, XBOOLE_0:def 3;

                then ((( Valid (s,J)) . w) '&' (( Valid (t,J)) . w)) = FALSE by MARGREL1: 12;

                hence thesis by A31, Th12;

              end;

               A33:

              now

                assume (( Valid (t,J)) . v) = FALSE ;

                then (( Valid (t,J)) . w) = FALSE by A26, A28, A29, XBOOLE_0:def 3;

                then ((( Valid (s,J)) . w) '&' (( Valid (t,J)) . w)) = FALSE by MARGREL1: 12;

                hence thesis by A31, Th12;

              end;

              ((( Valid (s,J)) . v) '&' (( Valid (t,J)) . v)) = FALSE by A31, Th12;

              hence thesis by A32, A33, MARGREL1: 12;

            end;

            now

              assume

               A34: (( Valid ((s '&' t),J)) . v) = TRUE ;

              then

               A35: ((( Valid (s,J)) . v) '&' (( Valid (t,J)) . v)) = TRUE by Th12;

              then (( Valid (t,J)) . v) = TRUE by MARGREL1: 12;

              then

               A36: (( Valid (t,J)) . w) = TRUE by A26, A28, A29, XBOOLE_0:def 3;

              (( Valid (s,J)) . v) = TRUE by A35, MARGREL1: 12;

              then (( Valid (s,J)) . w) = TRUE by A25, A28, A29, XBOOLE_0:def 3;

              then ((( Valid (s,J)) . w) '&' (( Valid (t,J)) . w)) = TRUE by A36;

              hence thesis by A34, Th12;

            end;

            hence thesis by A30, XBOOLEAN:def 3;

          end;

        end;

        thus PP[s] implies PP[( All (y,s))]

        proof

          assume that

           A37: not x in ( still_not-bound_in s) implies for v, w st for y st x <> y holds (w . y) = (v . y) holds (( Valid (s,J)) . v) = (( Valid (s,J)) . w) and

           A38: not x in ( still_not-bound_in ( All (y,s)));

          

           A39: not x in (( still_not-bound_in s) \ {y}) by A38, QC_LANG3: 12;

          thus for v, w st for z st x <> z holds (w . z) = (v . z) holds (( Valid (( All (y,s)),J)) . v) = (( Valid (( All (y,s)),J)) . w)

          proof

            let v, w such that

             A40: for z st x <> z holds (w . z) = (v . z);

             A41:

            now

              assume

               A42: (( Valid (( All (y,s)),J)) . v) = FALSE ;

              then (( FOR_ALL (y,( Valid (s,J)))) . v) = FALSE by Lm1;

              then

              consider v1 such that

               A43: (( Valid (s,J)) . v1) = FALSE and

               A44: for z st y <> z holds (v1 . z) = (v . z) by Th2;

               A45:

              now

                assume

                 A46: not x in ( still_not-bound_in s);

                consider v2 such that

                 A47: (for z st z <> y holds (v2 . z) = (w . z)) & (v2 . y) = (v1 . y) by Lm3;

                take v2;

                for z st x <> z holds (v2 . z) = (v1 . z)

                proof

                  let z such that

                   A48: x <> z;

                  now

                    assume

                     A49: z <> y;

                    

                    hence (v2 . z) = (w . z) by A47

                    .= (v . z) by A40, A48

                    .= (v1 . z) by A44, A49;

                  end;

                  hence thesis by A47;

                end;

                hence (( Valid (s,J)) . v2) = FALSE by A37, A43, A46;

                thus for z st y <> z holds (v2 . z) = (w . z) by A47;

              end;

              now

                assume

                 A50: x in {y};

                take v2 = v1;

                thus (( Valid (s,J)) . v2) = FALSE by A43;

                for z st y <> z holds (v1 . z) = (w . z)

                proof

                  let z;

                  assume

                   A51: y <> z;

                  then

                   A52: x <> z by A50, TARSKI:def 1;

                  

                  thus (v1 . z) = (v . z) by A44, A51

                  .= (w . z) by A40, A52;

                end;

                hence for z st y <> z holds (v2 . z) = (w . z);

              end;

              then (( FOR_ALL (y,( Valid (s,J)))) . w) = FALSE by A39, A45, Th2, XBOOLE_0:def 5;

              hence thesis by A42, Lm1;

            end;

            now

              assume

               A53: (( Valid (( All (y,s)),J)) . v) = TRUE ;

              then

               A54: (( FOR_ALL (y,( Valid (s,J)))) . v) = TRUE by Lm1;

              for v1 st for z st y <> z holds (v1 . z) = (w . z) holds (( Valid (s,J)) . v1) = TRUE

              proof

                let v1 such that

                 A55: for z st y <> z holds (v1 . z) = (w . z);

                 A56:

                now

                  assume

                   A57: not x in ( still_not-bound_in s);

                  consider v2 such that

                   A58: (for z st z <> y holds (v2 . z) = (v . z)) & (v2 . y) = (v1 . y) by Lm3;

                  

                   A59: for z st x <> z holds (v2 . z) = (v1 . z)

                  proof

                    let z such that

                     A60: x <> z;

                    now

                      assume

                       A61: z <> y;

                      

                      hence (v2 . z) = (v . z) by A58

                      .= (w . z) by A40, A60

                      .= (v1 . z) by A55, A61;

                    end;

                    hence thesis by A58;

                  end;

                  (( Valid (s,J)) . v2) = TRUE by A54, A58, Th3;

                  hence thesis by A37, A57, A59;

                end;

                now

                  assume x in {y};

                  then

                   A62: x = y by TARSKI:def 1;

                  for z st y <> z holds (v1 . z) = (v . z)

                  proof

                    let z;

                    assume

                     A63: y <> z;

                    

                    hence (v . z) = (w . z) by A40, A62

                    .= (v1 . z) by A55, A63;

                  end;

                  hence thesis by A54, Th3;

                end;

                hence thesis by A39, A56, XBOOLE_0:def 5;

              end;

              then (( FOR_ALL (y,( Valid (s,J)))) . w) = TRUE by Th3;

              hence thesis by A53, Lm1;

            end;

            hence thesis by A41, XBOOLEAN:def 3;

          end;

        end;

      end;

      for s holds PP[s] from CQC_LANG:sch 1( A1);

      hence thesis;

    end;

    theorem :: VALUAT_1:28

    

     Th28: (J,v) |= p & not x in ( still_not-bound_in p) implies for w st for y st x <> y holds (w . y) = (v . y) holds (J,w) |= p by Th27;

    theorem :: VALUAT_1:29

    

     Th29: (J,v) |= ( All (x,p)) iff for w st for y st x <> y holds (w . y) = (v . y) holds (J,w) |= p

    proof

       A1:

      now

        assume

         A2: for w st for y st x <> y holds (w . y) = (v . y) holds (J,w) |= p;

        for w st for y st x <> y holds (w . y) = (v . y) holds (( Valid (p,J)) . w) = TRUE by A2, Def7;

        hence (J,v) |= ( All (x,p)) by Th20;

      end;

      (J,v) |= ( All (x,p)) implies for w st for y st x <> y holds (w . y) = (v . y) holds (J,w) |= p by Th20;

      hence thesis by A1;

    end;

    reserve u,w for Element of ( Valuations_in (Al,A));

    reserve s9 for QC-formula of Al;

    theorem :: VALUAT_1:30

    

     Th30: x <> y & p = (s9 . x) & q = (s9 . y) implies for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v)

    proof

      defpred PP[ Element of ( QC-WFF Al)] means for x, y, p, q st x <> y & p = ($1 . x) & q = ($1 . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v);

       A1:

      now

        let s be Element of ( QC-WFF Al);

        thus s is atomic implies PP[s]

        proof

          assume

           A2: s is atomic;

          thus for x, y, p, q st x <> y & p = (s . x) & q = (s . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v)

          proof

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

             A3: s = (P ! l) by A2, QC_LANG1:def 18;

            let x, y, p, q such that x <> y and

             A4: p = (s . x) and

             A5: q = (s . y);

            set lx = ( Subst (l,((Al a. 0 ) .--> x))), ly = ( Subst (l,((Al a. 0 ) .--> y)));

            let v such that

             A6: (v . x) = (v . y);

            

             A7: p = (P ! ( Subst (l,((Al a. 0 ) .--> x)))) by A4, A3, CQC_LANG: 17;

            then

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

            

             A9: q = (P ! ( Subst (l,((Al a. 0 ) .--> y)))) by A5, A3, CQC_LANG: 17;

            then

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

            

             A11: { (ly . j) : 1 <= j & j <= ( len ly) & (ly . j) in ( fixed_QC-variables Al) } = {} by A9, CQC_LANG: 7;

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

            then

            reconsider lx, ly as CQC-variable_list of k, Al by A8, A10, A11, CQC_LANG: 5;

            

             A12: ( len (v *' lx)) = k by Def3;

             A13:

            now

              let i be Nat;

              assume that

               A14: 1 <= i and

               A15: i <= ( len (v *' lx));

              

               A16: i <= ( len l) by A12, A15, CARD_1:def 7;

               A17:

              now

                assume (l . i) <> (Al a. 0 );

                then

                 A18: (lx . i) = (l . i) & (ly . i) = (l . i) by A14, A16, CQC_LANG: 3;

                (v . (lx . i)) = ((v *' lx) . i) by A12, A14, A15, Def3;

                hence ((v *' lx) . i) = ((v *' ly) . i) by A12, A14, A15, A18, Def3;

              end;

              now

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

                then

                 A19: (lx . i) = x & (ly . i) = y by A14, A16, CQC_LANG: 3;

                (v . (lx . i)) = ((v *' lx) . i) by A12, A14, A15, Def3;

                hence ((v *' lx) . i) = ((v *' ly) . i) by A6, A12, A14, A15, A19, Def3;

              end;

              hence ((v *' lx) . i) = ((v *' ly) . i) by A17;

            end;

            ( len (v *' ly)) = k by Def3;

            then

             A20: (v *' lx) = (v *' ly) by A12, A13, FINSEQ_1: 14;

             A21:

            now

              assume (( Valid (p,J)) . v) = FALSE ;

              then not (v *' lx) in (J . P) by A7, Th8;

              hence (( Valid (q,J)) . v) = FALSE by A9, A20, Th8;

            end;

            now

              assume (( Valid (p,J)) . v) = TRUE ;

              then (v *' lx) in (J . P) by A7, Th7;

              hence (( Valid (q,J)) . v) = TRUE by A9, A20, Th7;

            end;

            hence thesis by A21, XBOOLEAN:def 3;

          end;

        end;

        thus PP[( VERUM Al)]

        proof

          let x, y, p, q such that x <> y and

           A22: p = (( VERUM Al) . x) and

           A23: q = (( VERUM Al) . y);

          let v such that (v . x) = (v . y);

          p = ( VERUM Al) by A22, CQC_LANG: 15;

          hence thesis by A23, CQC_LANG: 15;

        end;

        thus s is negative & PP[( the_argument_of s)] implies PP[s]

        proof

          assume that

           A24: s is negative and

           A25: for x, y, p, q st x <> y & p = (( the_argument_of s) . x) & q = (( the_argument_of s) . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v);

          thus for x, y, p, q st x <> y & p = (s . x) & q = (s . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v)

          proof

            let x, y, p, q such that x <> y and

             A26: p = (s . x) and

             A27: q = (s . y);

            

             A28: (s . y) = ( 'not' (( the_argument_of s) . y)) by A24, CQC_LANG: 18;

            then

            reconsider qa = (( the_argument_of s) . y) as Element of ( CQC-WFF Al) by A27, CQC_LANG: 8;

            

             A29: (s . x) = ( 'not' (( the_argument_of s) . x)) by A24, CQC_LANG: 18;

            then

            reconsider pa = (( the_argument_of s) . x) as Element of ( CQC-WFF Al) by A26, CQC_LANG: 8;

            let v such that

             A30: (v . x) = (v . y);

             A31:

            now

              assume (( Valid (p,J)) . v) = FALSE ;

              then ( 'not' (( Valid (pa,J)) . v)) = FALSE by A26, A29, Th10;

              then (( Valid (pa,J)) . v) = TRUE by MARGREL1: 11;

              then (( Valid (qa,J)) . v) = TRUE by A25, A30;

              then ( 'not' (( Valid (qa,J)) . v)) = FALSE by MARGREL1: 11;

              hence (( Valid (q,J)) . v) = FALSE by A27, A28, Th10;

            end;

            now

              assume (( Valid (p,J)) . v) = TRUE ;

              then ( 'not' (( Valid (pa,J)) . v)) = TRUE by A26, A29, Th10;

              then (( Valid (pa,J)) . v) = FALSE by MARGREL1: 11;

              then (( Valid (qa,J)) . v) = FALSE by A25, A30;

              then ( 'not' (( Valid (qa,J)) . v)) = TRUE by MARGREL1: 11;

              hence (( Valid (q,J)) . v) = TRUE by A27, A28, Th10;

            end;

            hence thesis by A31, XBOOLEAN:def 3;

          end;

        end;

        thus s is conjunctive & PP[( the_left_argument_of s)] & PP[( the_right_argument_of s)] implies PP[s]

        proof

          assume that

           A32: s is conjunctive and

           A33: for x, y, p, q st x <> y & p = (( the_left_argument_of s) . x) & q = (( the_left_argument_of s) . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v) and

           A34: for x, y, p, q st x <> y & p = (( the_right_argument_of s) . x) & q = (( the_right_argument_of s) . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v);

          thus for x, y, p, q st x <> y & p = (s . x) & q = (s . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v)

          proof

            let x, y, p, q such that x <> y and

             A35: p = (s . x) and

             A36: q = (s . y);

            

             A37: (s . x) = ((( the_left_argument_of s) . x) '&' (( the_right_argument_of s) . x)) by A32, CQC_LANG: 20;

            then

            reconsider pla = (( the_left_argument_of s) . x), pra = (( the_right_argument_of s) . x) as Element of ( CQC-WFF Al) by A35, CQC_LANG: 9;

            

             A38: (s . y) = ((( the_left_argument_of s) . y) '&' (( the_right_argument_of s) . y)) by A32, CQC_LANG: 20;

            then

            reconsider qla = (( the_left_argument_of s) . y), qra = (( the_right_argument_of s) . y) as Element of ( CQC-WFF Al) by A36, CQC_LANG: 9;

            let v such that

             A39: (v . x) = (v . y);

             A40:

            now

              assume

               A41: (( Valid (p,J)) . v) = FALSE ;

               A42:

              now

                assume (( Valid (pla,J)) . v) = FALSE ;

                then (( Valid (qla,J)) . v) = FALSE by A33, A39;

                then ((( Valid (qla,J)) . v) '&' (( Valid (qra,J)) . v)) = FALSE by MARGREL1: 12;

                hence thesis by A36, A38, A41, Th12;

              end;

               A43:

              now

                assume (( Valid (pra,J)) . v) = FALSE ;

                then (( Valid (qra,J)) . v) = FALSE by A34, A39;

                then ((( Valid (qla,J)) . v) '&' (( Valid (qra,J)) . v)) = FALSE by MARGREL1: 12;

                hence thesis by A36, A38, A41, Th12;

              end;

              ((( Valid (pla,J)) . v) '&' (( Valid (pra,J)) . v)) = FALSE by A35, A37, A41, Th12;

              hence thesis by A42, A43, MARGREL1: 12;

            end;

            now

              assume (( Valid (p,J)) . v) = TRUE ;

              then

               A44: ((( Valid (pla,J)) . v) '&' (( Valid (pra,J)) . v)) = TRUE by A35, A37, Th12;

              then (( Valid (pra,J)) . v) = TRUE by MARGREL1: 12;

              then

               A45: (( Valid (qra,J)) . v) = TRUE by A34, A39;

              (( Valid (pla,J)) . v) = TRUE by A44, MARGREL1: 12;

              then (( Valid (qla,J)) . v) = TRUE by A33, A39;

              then ((( Valid (qla,J)) . v) '&' (( Valid (qra,J)) . v)) = TRUE by A45;

              hence (( Valid (q,J)) . v) = TRUE by A36, A38, Th12;

            end;

            hence thesis by A40, XBOOLEAN:def 3;

          end;

        end;

        thus s is universal & PP[( the_scope_of s)] implies PP[s]

        proof

          assume that

           A46: s is universal and

           A47: for x, y, p, q st x <> y & p = (( the_scope_of s) . x) & q = (( the_scope_of s) . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v);

          consider xx be bound_QC-variable of Al, pp be Element of ( QC-WFF Al) such that

           A48: s = ( All (xx,pp)) by A46, QC_LANG1:def 21;

          

           A49: xx = ( bound_in s) by A46, A48, QC_LANG1:def 27;

          thus for x, y, p, q st x <> y & p = (s . x) & q = (s . y) holds for v st (v . x) = (v . y) holds (( Valid (p,J)) . v) = (( Valid (q,J)) . v)

          proof

            let x, y, p, q such that x <> y and

             A50: p = (s . x) and

             A51: q = (s . y);

            let v such that

             A52: (v . x) = (v . y);

             A53:

            now

              assume

               A54: x <> ( bound_in s);

              then (s . x) = ( All (( bound_in s),(( the_scope_of s) . x))) by A46, CQC_LANG: 23;

              then

              reconsider ps = (( the_scope_of s) . x) as Element of ( CQC-WFF Al) by A50, CQC_LANG: 13;

              

               A55: ( All (( bound_in s),ps)) = p by A46, A50, A54, CQC_LANG: 23;

               A56:

              now

                assume

                 A57: y <> ( bound_in s);

                then (s . y) = ( All (( bound_in s),(( the_scope_of s) . y))) by A46, CQC_LANG: 23;

                then

                reconsider qs = (( the_scope_of s) . y) as Element of ( CQC-WFF Al) by A51, CQC_LANG: 13;

                

                 A58: ( Valid (( All (( bound_in s),qs)),J)) = ( FOR_ALL (( bound_in s),( Valid (qs,J)))) by Lm1;

                

                 A59: ( Valid (( All (( bound_in s),ps)),J)) = ( FOR_ALL (( bound_in s),( Valid (ps,J)))) by Lm1;

                

                 A60: ( All (( bound_in s),qs)) = q by A46, A51, A57, CQC_LANG: 23;

                 A61:

                now

                  assume

                   A62: (( Valid (p,J)) . v) = TRUE ;

                  for v1 st for y st ( bound_in s) <> y holds (v1 . y) = (v . y) holds (( Valid (qs,J)) . v1) = TRUE

                  proof

                    let v1;

                    assume

                     A63: for y st ( bound_in s) <> y holds (v1 . y) = (v . y);

                    then

                     A64: (v1 . x) = (v . x) & (v1 . y) = (v . y) by A54, A57;

                    (( Valid (ps,J)) . v1) = TRUE by A55, A59, A62, A63, Th3;

                    hence thesis by A47, A52, A64;

                  end;

                  hence (( Valid (q,J)) . v) = TRUE by A60, A58, Th3;

                end;

                now

                  assume

                   A65: (( Valid (p,J)) . v) = FALSE ;

                  ex v1 st (( Valid (qs,J)) . v1) = FALSE & for y st ( bound_in s) <> y holds (v1 . y) = (v . y)

                  proof

                    consider v1 such that

                     A66: (( Valid (ps,J)) . v1) = FALSE and

                     A67: for y st ( bound_in s) <> y holds (v1 . y) = (v . y) by A55, A59, A65, Th2;

                    (v1 . x) = (v . x) & (v1 . y) = (v . y) by A54, A57, A67;

                    then (( Valid (qs,J)) . v1) = FALSE by A47, A52, A66;

                    hence thesis by A67;

                  end;

                  hence (( Valid (q,J)) . v) = FALSE by A60, A58, Th2;

                end;

                hence thesis by A61, XBOOLEAN:def 3;

              end;

              now

                assume

                 A68: y = ( bound_in s);

                then q = ( All (y,pp)) by A48, A49, A51, CQC_LANG: 24;

                hence thesis by A48, A49, A50, A68, CQC_LANG: 27;

              end;

              hence thesis by A56;

            end;

            now

              assume

               A69: x = ( bound_in s);

              then p = ( All (x,pp)) by A48, A49, A50, CQC_LANG: 24;

              hence thesis by A48, A49, A51, A69, CQC_LANG: 27;

            end;

            hence thesis by A53;

          end;

        end;

      end;

      for s be Element of ( QC-WFF Al) holds PP[s] from QC_LANG1:sch 2( A1);

      hence thesis;

    end;

    theorem :: VALUAT_1:31

    

     Th31: x <> y & not x in ( still_not-bound_in s9) implies not x in ( still_not-bound_in (s9 . y))

    proof

      defpred PP[ Element of ( QC-WFF Al)] means x <> y & not x in ( still_not-bound_in $1) implies not x in ( still_not-bound_in ($1 . y));

       A1:

      now

        let s be Element of ( QC-WFF Al);

        thus s is atomic implies PP[s]

        proof

          assume that

           A2: s is atomic and

           A3: x <> y and

           A4: not x in ( still_not-bound_in s);

          thus not x in ( still_not-bound_in (s . y))

          proof

            set l = ( the_arguments_of s);

            set ll = ( Subst (l,((Al a. 0 ) .--> y)));

            

             A5: ( still_not-bound_in s) = ( still_not-bound_in l) by A2, QC_LANG3: 4

            .= ( variables_in (l,( bound_QC-variables Al))) by QC_LANG3: 2

            .= { (l . k) : 1 <= k & k <= ( len l) & (l . k) in ( bound_QC-variables Al) } by QC_LANG3:def 1;

            

             A6: x in { (ll . k) : 1 <= k & k <= ( len ll) & (ll . k) in ( bound_QC-variables Al) } implies x in { (l . i) : 1 <= i & i <= ( len l) & (l . i) in ( bound_QC-variables Al) }

            proof

              assume x in { (ll . k) : 1 <= k & k <= ( len ll) & (ll . k) in ( bound_QC-variables Al) };

              then

              consider k such that

               A7: x = (ll . k) and

               A8: 1 <= k and

               A9: k <= ( len ll) and (ll . k) in ( bound_QC-variables Al);

              

               A10: k <= ( len l) by A9, CQC_LANG:def 1;

              then x = (l . k) by A3, A7, A8, CQC_LANG: 3;

              hence thesis by A8, A10;

            end;

            

             A11: (s . y) = (( the_pred_symbol_of s) ! ( Subst (l,((Al a. 0 ) .--> y)))) by A2, CQC_LANG: 16;

            

             A12: (s . y) is atomic & ( the_arguments_of (s . y)) = ll

            proof

              consider k be Nat, p be QC-pred_symbol of k, Al, l2 be QC-variable_list of k, Al such that

               A13: s = (p ! l2) by A2, QC_LANG1:def 18;

              l2 = l by A2, A13, QC_LANG1:def 23;

              then

              reconsider l3 = ( Subst (l,((Al a. 0 ) .--> y))) as QC-variable_list of k, Al;

              

               A14: (s . y) = (p ! l3) by A2, A11, A13, QC_LANG1:def 22;

              hence (s . y) is atomic by QC_LANG1:def 18;

              hence thesis by A14, QC_LANG1:def 23;

            end;

            

            then ( still_not-bound_in ( the_arguments_of (s . y))) = ( variables_in (ll,( bound_QC-variables Al))) by QC_LANG3: 2

            .= { (ll . k) : 1 <= k & k <= ( len ll) & (ll . k) in ( bound_QC-variables Al) } by QC_LANG3:def 1;

            hence thesis by A4, A5, A12, A6, QC_LANG3: 4;

          end;

        end;

        thus PP[( VERUM Al)] by CQC_LANG: 15;

        thus s is negative & PP[( the_argument_of s)] implies PP[s]

        proof

          assume that

           A15: s is negative and

           A16: (x <> y & not x in ( still_not-bound_in ( the_argument_of s)) implies not x in ( still_not-bound_in (( the_argument_of s) . y))) & x <> y & not x in ( still_not-bound_in s);

           not x in ( still_not-bound_in ( 'not' (( the_argument_of s) . y))) by A15, A16, QC_LANG3: 6, QC_LANG3: 7;

          hence thesis by A15, CQC_LANG: 18;

        end;

        thus s is conjunctive & PP[( the_left_argument_of s)] & PP[( the_right_argument_of s)] implies PP[s]

        proof

          assume that

           A17: s is conjunctive and

           A18: (x <> y & not x in ( still_not-bound_in ( the_left_argument_of s)) implies not x in ( still_not-bound_in (( the_left_argument_of s) . y))) & (x <> y & not x in ( still_not-bound_in ( the_right_argument_of s)) implies not x in ( still_not-bound_in (( the_right_argument_of s) . y))) & x <> y & not x in ( still_not-bound_in s);

          ( still_not-bound_in s) = (( still_not-bound_in ( the_left_argument_of s)) \/ ( still_not-bound_in ( the_right_argument_of s))) by A17, QC_LANG3: 9;

          then not x in (( still_not-bound_in (( the_left_argument_of s) . y)) \/ ( still_not-bound_in (( the_right_argument_of s) . y))) by A18, XBOOLE_0:def 3;

          then not x in ( still_not-bound_in ((( the_left_argument_of s) . y) '&' (( the_right_argument_of s) . y))) by QC_LANG3: 10;

          hence thesis by A17, CQC_LANG: 20;

        end;

        thus s is universal & PP[( the_scope_of s)] implies PP[s]

        proof

          assume that

           A19: s is universal and

           A20: x <> y & not x in ( still_not-bound_in ( the_scope_of s)) implies not x in ( still_not-bound_in (( the_scope_of s) . y)) and

           A21: x <> y and

           A22: not x in ( still_not-bound_in s);

          

           A23: ( still_not-bound_in s) = (( still_not-bound_in ( the_scope_of s)) \ {( bound_in s)}) by A19, QC_LANG3: 11;

          thus not x in ( still_not-bound_in (s . y))

          proof

             A24:

            now

              ( still_not-bound_in ( All (x,(( the_scope_of s) . y)))) = (( still_not-bound_in (( the_scope_of s) . y)) \ {x}) by QC_LANG3: 12;

              then

               A25: not x in ( still_not-bound_in ( All (x,(( the_scope_of s) . y)))) iff not x in ( still_not-bound_in (( the_scope_of s) . y)) or x in {x} by XBOOLE_0:def 5;

              assume x in {( bound_in s)};

              then x = ( bound_in s) by TARSKI:def 1;

              hence thesis by A19, A21, A25, CQC_LANG: 23, TARSKI:def 1;

            end;

            now

              assume not x in ( still_not-bound_in ( the_scope_of s));

              then not x in (( still_not-bound_in (( the_scope_of s) . y)) \ {( bound_in s)}) by A20, A21, XBOOLE_0:def 5;

              then not x in ( still_not-bound_in ( All (( bound_in s),(( the_scope_of s) . y)))) by QC_LANG3: 12;

              hence thesis by A19, A22, CQC_LANG: 22, CQC_LANG: 23;

            end;

            hence thesis by A22, A23, A24, XBOOLE_0:def 5;

          end;

        end;

      end;

      for s be Element of ( QC-WFF Al) holds PP[s] from QC_LANG1:sch 2( A1);

      hence thesis;

    end;

    theorem :: VALUAT_1:32

    

     Th32: (J,v) |= ( VERUM Al)

    proof

      ((( Valuations_in (Al,A)) --> TRUE ) . v) = TRUE by FUNCOP_1: 7;

      then (( Valid (( VERUM Al),J)) . v) = TRUE by Lm1;

      hence thesis;

    end;

    theorem :: VALUAT_1:33

    

     Th33: (J,v) |= ((p '&' q) => (q '&' p))

    proof

      thus (( Valid (((p '&' q) => (q '&' p)),J)) . v) = TRUE

      proof

        assume not (( Valid (((p '&' q) => (q '&' p)),J)) . v) = TRUE ;

        then

         A1: (( Valid (((p '&' q) => (q '&' p)),J)) . v) = FALSE by XBOOLEAN:def 3;

        (( Valid (((p '&' q) => (q '&' p)),J)) . v) = (( Valid (( 'not' ((p '&' q) '&' ( 'not' (q '&' p)))),J)) . v) by QC_LANG2:def 2

        .= ( 'not' (( Valid (((p '&' q) '&' ( 'not' (q '&' p))),J)) . v)) by Th10

        .= ( 'not' ((( Valid ((p '&' q),J)) . v) '&' (( Valid (( 'not' (q '&' p)),J)) . v))) by Th12

        .= ( 'not' ((( Valid ((p '&' q),J)) . v) '&' ( 'not' (( Valid ((q '&' p),J)) . v)))) by Th10;

        then

         A2: ((( Valid ((p '&' q),J)) . v) '&' ( 'not' (( Valid ((q '&' p),J)) . v))) = TRUE by A1, MARGREL1: 11;

        then ( 'not' (( Valid ((q '&' p),J)) . v)) = TRUE by MARGREL1: 12;

        then

         A3: (( Valid ((q '&' p),J)) . v) = FALSE by MARGREL1: 11;

        (( Valid ((p '&' q),J)) . v) = TRUE by A2, MARGREL1: 12;

        then ((( Valid (p,J)) . v) '&' (( Valid (q,J)) . v)) = TRUE by Th12;

        hence thesis by A3, Th12;

      end;

    end;

    theorem :: VALUAT_1:34

    

     Th34: (J,v) |= ((( 'not' p) => p) => p)

    proof

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

      

      then

       A1: (( Valid (((( 'not' p) => p) => p),J)) . v) = (( Valid (( 'not' (( 'not' (( 'not' p) '&' ( 'not' p))) '&' ( 'not' p))),J)) . v) by QC_LANG2:def 2

      .= ( 'not' (( Valid ((( 'not' (( 'not' p) '&' ( 'not' p))) '&' ( 'not' p)),J)) . v)) by Th10

      .= ( 'not' ((( Valid (( 'not' (( 'not' p) '&' ( 'not' p))),J)) . v) '&' (( Valid (( 'not' p),J)) . v))) by Th12;

      (( Valid (( 'not' (( 'not' p) '&' ( 'not' p))),J)) . v) = ( 'not' (( Valid ((( 'not' p) '&' ( 'not' p)),J)) . v)) by Th10

      .= ( 'not' (( Valid (( 'not' p),J)) . v)) by Th22

      .= ( 'not' ( 'not' (( Valid (p,J)) . v))) by Th10

      .= (( Valid (p,J)) . v);

      

      then (( Valid (((( 'not' p) => p) => p),J)) . v) = ( 'not' ((( Valid (p,J)) . v) '&' ( 'not' (( Valid (p,J)) . v)))) by A1, Th10

      .= TRUE by XBOOLEAN: 102;

      hence (( Valid (((( 'not' p) => p) => p),J)) . v) = TRUE ;

    end;

    theorem :: VALUAT_1:35

    

     Th35: (J,v) |= (p => (( 'not' p) => q))

    proof

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

      

      then

       A1: (( Valid ((p => (( 'not' p) => q)),J)) . v) = (( Valid (( 'not' (p '&' ( 'not' ( 'not' (( 'not' p) '&' ( 'not' q)))))),J)) . v) by QC_LANG2:def 2

      .= ( 'not' (( Valid ((p '&' ( 'not' ( 'not' (( 'not' p) '&' ( 'not' q))))),J)) . v)) by Th10

      .= ( 'not' ((( Valid (p,J)) . v) '&' (( Valid (( 'not' ( 'not' (( 'not' p) '&' ( 'not' q)))),J)) . v))) by Th12;

      (( Valid (( 'not' ( 'not' (( 'not' p) '&' ( 'not' q)))),J)) . v) = ( 'not' (( Valid (( 'not' (( 'not' p) '&' ( 'not' q))),J)) . v)) by Th10

      .= ( 'not' ( 'not' (( Valid ((( 'not' p) '&' ( 'not' q)),J)) . v))) by Th10

      .= ((( Valid (( 'not' p),J)) . v) '&' (( Valid (( 'not' q),J)) . v)) by Th12

      .= (( 'not' (( Valid (p,J)) . v)) '&' (( Valid (( 'not' q),J)) . v)) by Th10

      .= (( 'not' (( Valid (p,J)) . v)) '&' ( 'not' (( Valid (q,J)) . v))) by Th10;

      

      then

       A2: (( Valid ((p => (( 'not' p) => q)),J)) . v) = ( 'not' (((( Valid (p,J)) . v) '&' ( 'not' (( Valid (p,J)) . v))) '&' ( 'not' (( Valid (q,J)) . v)))) by A1, MARGREL1: 16

      .= ( 'not' ( FALSE '&' ( 'not' (( Valid (q,J)) . v)))) by XBOOLEAN: 138;

      ( FALSE '&' ( 'not' (( Valid (q,J)) . v))) = FALSE by MARGREL1: 13;

      hence (( Valid ((p => (( 'not' p) => q)),J)) . v) = TRUE by A2, MARGREL1: 11;

    end;

    theorem :: VALUAT_1:36

    

     Th36: (J,v) |= ((p => q) => (( 'not' (q '&' t)) => ( 'not' (p '&' t))))

    proof

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

      

      then

       A1: (( Valid (((p => q) => (( 'not' (q '&' t)) => ( 'not' (p '&' t)))),J)) . v) = (( Valid (( 'not' (( 'not' (p '&' ( 'not' q))) '&' ( 'not' ( 'not' (( 'not' (q '&' t)) '&' ( 'not' ( 'not' (p '&' t)))))))),J)) . v) by QC_LANG2:def 2

      .= ( 'not' (( Valid ((( 'not' (p '&' ( 'not' q))) '&' ( 'not' ( 'not' (( 'not' (q '&' t)) '&' ( 'not' ( 'not' (p '&' t))))))),J)) . v)) by Th10

      .= ( 'not' ((( Valid (( 'not' (p '&' ( 'not' q))),J)) . v) '&' (( Valid (( 'not' ( 'not' (( 'not' (q '&' t)) '&' ( 'not' ( 'not' (p '&' t)))))),J)) . v))) by Th12;

      

       A2: (( Valid (( 'not' (p '&' ( 'not' q))),J)) . v) = ( 'not' (( Valid ((p '&' ( 'not' q)),J)) . v)) by Th10

      .= ( 'not' ((( Valid (p,J)) . v) '&' (( Valid (( 'not' q),J)) . v))) by Th12

      .= ( 'not' ((( Valid (p,J)) . v) '&' ( 'not' (( Valid (q,J)) . v)))) by Th10;

      (( Valid (( 'not' ( 'not' (( 'not' (q '&' t)) '&' ( 'not' ( 'not' (p '&' t)))))),J)) . v) = ( 'not' (( Valid (( 'not' (( 'not' (q '&' t)) '&' ( 'not' ( 'not' (p '&' t))))),J)) . v)) by Th10

      .= ( 'not' ( 'not' (( Valid ((( 'not' (q '&' t)) '&' ( 'not' ( 'not' (p '&' t)))),J)) . v))) by Th10

      .= ((( Valid (( 'not' (q '&' t)),J)) . v) '&' (( Valid (( 'not' ( 'not' (p '&' t))),J)) . v)) by Th12

      .= (( 'not' (( Valid ((q '&' t),J)) . v)) '&' (( Valid (( 'not' ( 'not' (p '&' t))),J)) . v)) by Th10

      .= (( 'not' (( Valid ((q '&' t),J)) . v)) '&' ( 'not' (( Valid (( 'not' (p '&' t)),J)) . v))) by Th10

      .= (( 'not' (( Valid ((q '&' t),J)) . v)) '&' ( 'not' ( 'not' (( Valid ((p '&' t),J)) . v)))) by Th10

      .= (( 'not' ((( Valid (q,J)) . v) '&' (( Valid (t,J)) . v))) '&' (( Valid ((p '&' t),J)) . v)) by Th12

      .= (( 'not' ((( Valid (q,J)) . v) '&' (( Valid (t,J)) . v))) '&' ((( Valid (p,J)) . v) '&' (( Valid (t,J)) . v))) by Th12;

      hence (( Valid (((p => q) => (( 'not' (q '&' t)) => ( 'not' (p '&' t)))),J)) . v) = TRUE by A1, A2, Lm2;

    end;

    theorem :: VALUAT_1:37

    (J,v) |= p & (J,v) |= (p => q) implies (J,v) |= q by Th24;

    theorem :: VALUAT_1:38

    

     Th38: (J,v) |= (( All (x,p)) => p)

    proof

      thus (( Valid ((( All (x,p)) => p),J)) . v) = TRUE

      proof

        assume not (( Valid ((( All (x,p)) => p),J)) . v) = TRUE ;

        then

         A1: (( Valid ((( All (x,p)) => p),J)) . v) = FALSE by XBOOLEAN:def 3;

        (( Valid ((( All (x,p)) => p),J)) . v) = (( Valid (( 'not' (( All (x,p)) '&' ( 'not' p))),J)) . v) by QC_LANG2:def 2

        .= ( 'not' (( Valid ((( All (x,p)) '&' ( 'not' p)),J)) . v)) by Th10

        .= ( 'not' ((( Valid (( All (x,p)),J)) . v) '&' (( Valid (( 'not' p),J)) . v))) by Th12

        .= ( 'not' ((( Valid (( All (x,p)),J)) . v) '&' ( 'not' (( Valid (p,J)) . v)))) by Th10;

        then

         A2: ((( Valid (( All (x,p)),J)) . v) '&' ( 'not' (( Valid (p,J)) . v))) = TRUE by A1, MARGREL1: 11;

        then ( 'not' (( Valid (p,J)) . v)) = TRUE by MARGREL1: 12;

        then

         A3: (( Valid (p,J)) . v) = FALSE by MARGREL1: 11;

        (( Valid (( All (x,p)),J)) . v) = TRUE by A2, MARGREL1: 12;

        then (( FOR_ALL (x,( Valid (p,J)))) . v) = TRUE by Lm1;

        hence thesis by A3, Th25;

      end;

    end;

    theorem :: VALUAT_1:39

    J |= ( VERUM Al) by Th32;

    theorem :: VALUAT_1:40

    J |= ((p '&' q) => (q '&' p)) by Th33;

    theorem :: VALUAT_1:41

    J |= ((( 'not' p) => p) => p) by Th34;

    theorem :: VALUAT_1:42

    J |= (p => (( 'not' p) => q)) by Th35;

    theorem :: VALUAT_1:43

    J |= ((p => q) => (( 'not' (q '&' t)) => ( 'not' (p '&' t)))) by Th36;

    theorem :: VALUAT_1:44

    J |= p & J |= (p => q) implies J |= q

    proof

      assume

       A1: J |= p & J |= (p => q);

      now

        let v;

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

        hence (J,v) |= q by Th24;

      end;

      hence thesis;

    end;

    theorem :: VALUAT_1:45

    J |= (( All (x,p)) => p) by Th38;

    theorem :: VALUAT_1:46

    J |= (p => q) & not x in ( still_not-bound_in p) implies J |= (p => ( All (x,q)))

    proof

      assume that

       A1: for v holds (J,v) |= (p => q) and

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

      let u;

      now

        assume

         A3: (J,u) |= p;

        now

          let w;

          assume for y st x <> y holds (w . y) = (u . y);

          then

           A4: (J,w) |= p by A2, A3, Th28;

          (J,w) |= (p => q) by A1;

          hence (J,w) |= q by A4, Th24;

        end;

        hence (J,u) |= ( All (x,q)) by Th29;

      end;

      hence thesis by Th24;

    end;

    theorem :: VALUAT_1:47

    for s be QC-formula of Al st p = (s . x) & q = (s . y) & not x in ( still_not-bound_in s) & J |= p holds J |= q

    proof

      let s be QC-formula of Al;

      assume that

       A1: p = (s . x) and

       A2: q = (s . y) and

       A3: not x in ( still_not-bound_in s) and

       A4: J |= p;

      now

        assume

         A5: x <> y;

         A6:

        now

          let u;

          consider w be Element of ( Valuations_in (Al,A)) such that

           A7: (for z be bound_QC-variable of Al st z <> x holds (w . z) = (u . z)) & (w . x) = (u . y) by Lm3;

          (w . x) = (w . y) by A7;

          then

           A8: (( Valid (p,J)) . w) = (( Valid (q,J)) . w) by A1, A2, Th30;

          (J,w) |= p by A4;

          then

           A9: (( Valid (p,J)) . w) = TRUE ;

           not x in ( still_not-bound_in q) by A2, A3, A5, Th31;

          hence (( Valid (q,J)) . u) = TRUE by A7, A8, A9, Th27;

        end;

        for v holds (J,v) |= q by A6;

        hence thesis;

      end;

      hence thesis by A1, A2, A4;

    end;