The Mizar article:

Interpretation and Satisfiability in the First Order Logic

by
Edmund Woronowicz

Received June 1, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: VALUAT_1
[ MML identifier index ]


environ

 vocabulary FUNCT_2, QC_LANG1, FRAENKEL, FUNCT_1, RELAT_1, MARGREL1, BOOLE,
      ZF_LANG, CQC_LANG, FINSEQ_1, ARYTM_3, FUNCOP_1, ZF_MODEL, QC_LANG3,
      CAT_1, VALUAT_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, RELAT_1, FUNCT_1,
      FUNCT_2, FINSEQ_1, FRAENKEL, QC_LANG1, QC_LANG3, CQC_LANG, MARGREL1;
 constructors QC_LANG3, CQC_LANG, MARGREL1, XREAL_0, XCMPLX_0, MEMBERED,
      XBOOLE_0;
 clusters RELSET_1, MARGREL1, CQC_LANG, QC_LANG1, ARYTM_3, FINSEQ_1, FUNCT_1,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions TARSKI, MARGREL1;
 theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, FUNCOP_1, FRAENKEL, QC_LANG1,
      QC_LANG2, QC_LANG3, CQC_LANG, MARGREL1, RELSET_1, RELAT_1, FINSEQ_3,
      XBOOLE_0, XBOOLE_1;
 schemes QC_LANG1, CQC_LANG, FUNCT_1, FUNCT_2;

begin

 reserve i,j,k for Nat,
         A,D for non empty set;

 definition let A be set;
   func Valuations_in A -> set equals
  :Def1: Funcs(bound_QC-variables, A);
  coherence;
 end;

 definition let A;
  cluster Valuations_in A -> non empty functional;
  coherence
  proof
     Valuations_in A = Funcs(bound_QC-variables, A) by Def1;
   hence thesis;
  end;
 end;

canceled;

theorem
 Th2: for x being set st x is Element of Valuations_in A holds
       x is Function of bound_QC-variables ,A
     proof let x be set;
       assume x is Element of Valuations_in A;
       then x in Valuations_in A;
       then x in Funcs(bound_QC-variables,A) by Def1;
       then ex f being Function st
 x = f & dom f = bound_QC-variables & rng f c= A by FUNCT_2:def 2;
      hence thesis by FUNCT_2:def 1,RELSET_1:11;
     end;

definition
 let A;
 redefine func Valuations_in A -> FUNCTION_DOMAIN of bound_QC-variables, A;
  coherence
   proof
       for x be Element of Valuations_in A holds
 x is Function of bound_QC-variables ,A by Th2;
     hence Valuations_in A is FUNCTION_DOMAIN of bound_QC-variables, A
                                                            by FRAENKEL:def 2;
   end;
end;

definition let f be Function;
 attr f is boolean-valued means
:Def2: rng f c= BOOLEAN;
end;

definition
 cluster boolean-valued Function;
 existence
  proof take {};
   thus rng {} c= BOOLEAN by RELAT_1:60,XBOOLE_1:2;
  end;
end;

definition let f be boolean-valued Function, x be set;
 cluster f.x -> boolean;
 coherence
  proof
   per cases;
   suppose not x in dom f;
    then f.x = 0 by FUNCT_1:def 4;
   hence f.x in BOOLEAN by MARGREL1:def 12,TARSKI:def 2;
   suppose x in dom f;
    then A1:   f.x in rng f by FUNCT_1:def 5;
      rng f c= BOOLEAN by Def2;
   hence f.x in BOOLEAN by A1;
  end;
end;

definition let A be set;
 cluster -> boolean-valued Element of Funcs(A,BOOLEAN);
 coherence
  proof let F be Element of Funcs(A,BOOLEAN);
      ex f being Function st F = f & dom f = A & rng f c= BOOLEAN
       by FUNCT_2:def 2;
   hence rng F c= BOOLEAN;
  end;
end;

definition
 let p be boolean-valued Function;
  func 'not' p -> Function means
:Def3: dom it = dom p &
   for x being set st x in dom p holds it.x = 'not'(p.x);
 existence
     proof
       deffunc F(set) = 'not'(p.$1);
       consider q being Function such that
A1:     dom q = dom p and
  A2:   for x being set st x in dom p holds q.x = F(x) from Lambda;
       take q;
       thus thesis by A1,A2;
     end;
 uniqueness
   proof let q1,q2 be Function such that
A3: dom q1 = dom p and
   A4:  for x being set st x in dom p holds q1.x = 'not'(p.x) and
A5: dom q2 = dom p and
   A6:  for x being set st x in dom p holds q2.x = 'not'(p.x);
          for x being set st x in dom p holds q1.x = q2.x
        proof let x be set;
         assume x in dom p;
          then q1.x = 'not'(p.x) & q2.x = 'not'(p.x) by A4,A6;
         hence thesis;
        end;
     hence thesis by A3,A5,FUNCT_1:9;
   end;
 let q be boolean-valued Function;
  func p '&' q -> Function means
:Def4: dom it = dom p /\ dom q &
  for x being set st x in dom it holds it.x = (p.x) '&' (q.x);
 existence
   proof
     deffunc F(set) = (p.$1) '&' (q.$1);
       consider s being Function such that
A7:     dom s = dom p /\ dom q and
  A8:   for x being set st x in dom p /\ dom q
            holds s.x = F(x) from Lambda;
       take s;
       thus thesis by A7,A8;
   end;
 uniqueness
 proof let s1,s2 be Function such that
A9: dom s1 = dom p /\ dom q and
   A10:  for x being set st x in dom s1 holds s1.x = (p.x) '&' (q.x) and
A11: dom s2 = dom p /\ dom q and
   A12:  for x being set st x in dom s2 holds s2.x = (p.x) '&' (q.x);
          for x being set st x in dom s1 holds s1.x = s2.x
        proof let x be set;
         assume x in dom s1;
           then s1.x = (p.x) '&' (q.x) & s2.x = (p.x) '&' (q.x) by A9,A10,A11,
A12;
           hence thesis;
        end;
        hence thesis by A9,A11,FUNCT_1:9;
  end;
 commutativity;
end;

definition
 let p be boolean-valued Function;
 cluster 'not' p -> boolean-valued;
  coherence
   proof let x be set;
    assume x in rng 'not' p;
     then consider y being set such that
A1:   y in dom 'not' p and
A2:   x = ('not' p).y by FUNCT_1:def 5;
A3:   y in dom p by A1,Def3;
     then A4:   x = 'not'(p.y) by A2,Def3;
A5:   rng p c= BOOLEAN by Def2;
       p.y in rng p by A3,FUNCT_1:def 5;
     then p.y = FALSE or p.y = TRUE by A5,MARGREL1:37,TARSKI:def 2;
     then x = FALSE or x = TRUE by A4,MARGREL1:def 16;
    hence x in BOOLEAN;
   end;
 let q be boolean-valued Function;
  cluster p '&' q -> boolean-valued;
  coherence
   proof let x be set;
    assume x in rng(p '&' q);
     then consider y being set such that
A6:   y in dom(p '&' q) and
A7:   x = (p '&' q).y by FUNCT_1:def 5;
A8:   x = (p.y) '&' (q.y) by A6,A7,Def4;
       p.y = TRUE & q.y = TRUE or not(p.y = TRUE & q.y = TRUE);
     then x = FALSE or x = TRUE by A8,MARGREL1:def 17;
    hence x in BOOLEAN;
   end;
end;

 reserve f1,f2 for Element of Funcs(Valuations_in A,BOOLEAN),
         x,x1,y for bound_QC-variable,
         v,v1 for Element of Valuations_in A;

definition let A;
 redefine
 let p be Element of Funcs(A,BOOLEAN);
  func 'not' p -> Element of Funcs(A,BOOLEAN) means
:Def5: for x being Element of A holds it.x = 'not'(p.x);
 coherence
     proof
       ex f being Function st p = f & dom f = A & rng f c= BOOLEAN
            by FUNCT_2:def 2;
     then A1:     dom 'not' p = A by Def3;
         rng 'not' p c= BOOLEAN by Def2;
      hence thesis by A1,FUNCT_2:def 2;
     end;
 compatibility
  proof let IT be Element of Funcs(A,BOOLEAN);
   hereby assume
A2:   IT = 'not' p;
    let x be Element of A;
       x in A;
     then x in dom p by FUNCT_2:def 1;
    hence IT.x = 'not'(p.x) by A2,Def3;
   end;
   assume
A3:  for x being Element of A holds IT.x = 'not'(p.x);
A4:  dom IT = A by FUNCT_2:def 1;
A5:  dom p = A by FUNCT_2:def 1;
    then for x being set st x in dom p holds IT.x = 'not'(p.x) by A3;
   hence IT = 'not' p by A4,A5,Def3;
  end;
 let q be Element of Funcs(A,BOOLEAN);
  func p '&' q -> Element of Funcs(A,BOOLEAN) means
:Def6: for x being Element of A holds it.x = (p.x) '&' (q.x);
 coherence
   proof
A6:  ex f being Function st p = f & dom f = A & rng f c= BOOLEAN
            by FUNCT_2:def 2;
       ex f being Function st q = f & dom f = A & rng f c= BOOLEAN
            by FUNCT_2:def 2;
     then A7:   dom(p '&' q) = A /\ A by A6,Def4 .= A;
       rng(p '&' q) c= BOOLEAN by Def2;
    hence thesis by A7,FUNCT_2:def 2;
   end;
 compatibility
  proof let IT be Element of Funcs(A,BOOLEAN);
   hereby assume
A8:   IT = p '&' q;
    let x be Element of A;
A9:  dom p = A by FUNCT_2:def 1;
      dom q = A by FUNCT_2:def 1;
    then dom(p '&' q) = A /\ A by A9,Def4 .= A;
    hence IT.x = (p.x) '&' (q.x) by A8,Def4;
   end;
   assume
A10:  for x being Element of A holds IT.x = (p.x) '&' (q.x);
A11:  dom IT = A by FUNCT_2:def 1;
A12:  dom q = A by FUNCT_2:def 1;
A13:  dom IT = A /\ A by FUNCT_2:def 1 .= dom p /\ dom q by A12,FUNCT_2:def 1;
      for x being set st x in dom IT holds IT.x = (p.x) '&' (q.x) by A10,A11;
   hence IT = p '&' q by A13,Def4;
  end;
end;

definition
 let A, x;
 let p be Element of Funcs(Valuations_in A,BOOLEAN);
  func FOR_ALL(x,p) -> Element of Funcs(Valuations_in A,BOOLEAN) means
:Def7: for v holds
        it.v = ALL{p.v' where v' is Element of Valuations_in A:
                       for y st x <> y holds v'.y = v.y};
  existence
  proof
    deffunc F(Function) = ALL{p.v' where v' is Element of Valuations_in A:
                       for y st x <> y holds v'.y = $1.y};
    consider f being Function of Valuations_in A, BOOLEAN such that
A1:   for v holds f.v = F(v) from LambdaD;
      dom f = Valuations_in A & rng f c= BOOLEAN by FUNCT_2:def 1,RELSET_1:12;
    then reconsider f as Element of Funcs(Valuations_in 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.v' where v' is Element of Valuations_in A:
                                   for y st x <> y holds v'.y = v.y} and
 A3:   for v holds f2.v = ALL{p.v' where v' is Element of Valuations_in A:
                                   for y st x <> y holds v'.y = v.y};
     for v holds f1.v = f2.v
     proof let v;
         f1.v = ALL{p.v' where v' is Element of Valuations_in A:
                      for y st x <> y holds v'.y = v.y} &
       f2.v = ALL{p.v'' where v'' is Element of Valuations_in A:
                      for y st x <> y holds v''.y = v.y} by A2,A3;
       hence thesis;
     end;
     hence thesis by FUNCT_2:113;
  end;
end;

canceled 4;

theorem
 Th7: for p being Element of Funcs(Valuations_in 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 A,BOOLEAN);
A1: now
     assume FOR_ALL(x,p).v = FALSE;
       then ALL{p.v'' where v'' is Element of Valuations_in A:
                for y st x <> y holds v''.y = v.y} = FALSE by Def7;
       then FALSE in {p.v'' where v'' is Element of Valuations_in A:
                for y st x <> y holds v''.y = v.y} by MARGREL1:53;
       hence ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
    end;
      now assume
        ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
      then FALSE in {p.v'' where v'' is Element of Valuations_in A:
                for y st x <> y holds v''.y = v.y};
      then ALL{p.v'' where v'' is Element of Valuations_in A:
                for y st x <> y holds v''.y = v.y} = FALSE by MARGREL1:53;
      hence FOR_ALL(x,p).v = FALSE by Def7;
    end;
    hence thesis by A1;
  end;

 theorem
 Th8: for p being Element of Funcs(Valuations_in 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 A,BOOLEAN);
A1: now
     assume FOR_ALL(x,p).v = TRUE;
       then ALL{p.v'' where v'' is Element of Valuations_in A:
                for y st x <> y holds v''.y = v.y} = TRUE by Def7;
then A2:       not FALSE in {p.v'' where v'' is Element of Valuations_in A:
                           for y st x <> y holds v''.y = v.y} by MARGREL1:53;

     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 (p.v1 = TRUE) by MARGREL1:43;
       end;
    end;
      now assume
 A3:   for v1 st for y st x <> y holds v1.y = v.y holds p.v1 = TRUE;
        for v1 st for y st x <> y holds v1.y = v.y holds not p.v1 = FALSE
      proof let v1;
         assume for y st x <> y holds v1.y = v.y;
           then p.v1 = TRUE by A3;
          hence not (p.v1 = FALSE) by MARGREL1:43;
      end;
      then not ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
      then not FALSE in {p.v'' where v'' is Element of Valuations_in A:
                           for y st x <> y holds v''.y = v.y};
      then ALL{p.v'' where v'' is Element of Valuations_in A:
               for y st x <> y holds v''.y = v.y} = TRUE by MARGREL1:53;
      hence FOR_ALL(x,p).v = TRUE by Def7;
    end;
    hence thesis by A1;
  end;

reserve ll for CQC-variable_list of k;

definition
 let A, k, ll, v;
  redefine
  func v*ll -> FinSequence of A means
:Def8: len it = k & for i st 1 <= i & i <= k holds it.i = v.(ll.i);
 coherence
  proof
      dom v = bound_QC-variables by FUNCT_2:def 1;
    then A1:  rng ll c= dom v by CQC_LANG:def 5;
A2:  len ll = k by QC_LANG1:def 8;
      dom(v*ll) = dom ll by A1,RELAT_1:46
              .= Seg k by A2,FINSEQ_1:def 3;
    then A3:  v*ll is FinSequence-like by FINSEQ_1:def 2;
A4:  rng v c= A by RELSET_1:12;
      rng(v*ll) c= rng v by RELAT_1:45;
    then rng( v*ll) c= A by A4,XBOOLE_1:1;
   hence v*ll is FinSequence of A by A3,FINSEQ_1:def 4;
  end;
 compatibility
  proof let IT be FinSequence of A;
     dom v = bound_QC-variables by FUNCT_2:def 1;
   then A5:  rng ll c= dom v by CQC_LANG:def 5;
A6:  len ll = k by QC_LANG1:def 8;
   thus IT = v*ll implies
    len IT = k & for i st 1 <= i & i <= k holds IT.i = v.(ll.i)
    proof assume
A7:    IT = v*ll;
      then A8:    dom ll = dom IT by A5,RELAT_1:46;
     hence len IT = k by A6,FINSEQ_3:31;
     let i;
     assume 1 <= i & i <= k;
      then i in dom IT by A6,A8,FINSEQ_3:27;
     hence IT.i = v.(ll.i) by A7,FUNCT_1:22;
    end;
   assume that
A9:  len IT = k and
A10:  for i st 1 <= i & i <= k holds IT.i = v.(ll.i);
A11:  for x being set holds x in dom IT iff x in dom ll & ll.x in dom v
     proof let x be set;
      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 A6,A9,FINSEQ_3:31;
         then ll.x in rng ll by FUNCT_1:def 5;
        hence ll.x in dom v by A5;
       end;
       assume x in dom ll & ll.x in dom v;
      hence x in dom IT by A6,A9,FINSEQ_3:31;
     end;
      for x being set st x in dom IT holds IT.x = v.(ll.x)
     proof let x be set;
      assume
A12:     x in dom IT;
       then reconsider i = x as Nat;
         1 <= i & i <= k by A9,A12,FINSEQ_3:27;
      hence IT.x = v.(ll.x) by A10;
     end;
   hence IT = v*ll by A11,FUNCT_1:20;
  end;
 synonym v*'ll;
end;

definition
 let A, k, ll;
 let r be Element of relations_on A;
  func ll 'in' r -> Element of Funcs(Valuations_in A,BOOLEAN) means
:Def9: for v being Element of Valuations_in A holds
       (v*'ll in r implies it.v = TRUE) &
       (not v*'ll in r implies it.v = FALSE);
 existence
 proof
   deffunc F(set) = FALSE;
   deffunc T(set) = TRUE;
   defpred C[set] means ex v being Element of Valuations_in A st $1 = v &
                v*'ll in r;
   A1: for x being set st x in Valuations_in A holds
           (C[x] implies T(x) in BOOLEAN) &
           (not C[x] implies F(x) in BOOLEAN);
    consider f being Function of Valuations_in A, BOOLEAN such that
  A2:   for x being set st x in Valuations_in A holds
           (C[x] implies f.x = T(x)) &
           (not C[x] implies f.x = F(x)) from Lambda1C(A1);
      dom f = Valuations_in A & rng f c= BOOLEAN by FUNCT_2:def 1,RELSET_1:12;
    then reconsider f as Element of Funcs(Valuations_in A,BOOLEAN) by FUNCT_2:
def 2;
    take f;
    let v be Element of Valuations_in A;
        ((ex v' being Element of Valuations_in A st v = v' &
              v'*'ll in r) implies f.v = TRUE) &
      (not (ex v' being Element of Valuations_in A st v = v' &
              v'*'ll in r) implies f.v = FALSE) by A2;
      hence thesis;
 end;
 uniqueness
   proof let f1,f2 be Element of Funcs(Valuations_in A,BOOLEAN);
     assume that
 A3:   for v being Element of Valuations_in A holds
         (v*'ll in r implies f1.v = TRUE) &
         (not v*'ll in r implies f1.v = FALSE) and
 A4:   for v being Element of Valuations_in A holds
         (v*'ll in r implies f2.v = TRUE) &
         (not v*'ll in r implies f2.v = FALSE);
     for v being Element of Valuations_in A holds f1.v = f2.v
     proof let v be Element of Valuations_in A;
      per cases;
      suppose v*'ll in r;
         then f1.v = TRUE & f2.v = TRUE by A3,A4;
         hence thesis;
      suppose not v*'ll in r;
         then f1.v = FALSE & f2.v = FALSE by A3,A4;
         hence thesis;
     end;
     hence thesis by FUNCT_2:113;
  end;
end;

definition
 let A;
 let F be Function of CQC-WFF,Funcs(Valuations_in A, BOOLEAN);
 let p be Element of CQC-WFF;
 redefine func F.p -> Element of Funcs(Valuations_in A, BOOLEAN);
 coherence
  proof
    thus F.p is Element of Funcs(Valuations_in A, BOOLEAN);
  end;
end;

definition
 let D;
   mode interpretation of D -> Function of QC-pred_symbols, relations_on D
     means
      for P being (Element of QC-pred_symbols),
      r being 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 --> empty_rel(D)
                 as Function of QC-pred_symbols, relations_on D;
   take F1;
   let P be Element of QC-pred_symbols;
    thus thesis by FUNCOP_1:13;
  end;
 end;

reserve
     p,q,s,t for Element of CQC-WFF,
     J for interpretation of A,
     P for QC-pred_symbol of k,
     r for Element of relations_on A;

definition let A, k, J, P;
  redefine func J.P -> Element of relations_on A;
 coherence by FUNCT_2:7;
end;

definition let A, J, p;
  func Valid(p,J) -> Element of Funcs(Valuations_in A, BOOLEAN) means
:Def11: ex F being Function of CQC-WFF,Funcs(Valuations_in A, BOOLEAN) st
    it = F.p &
    F.VERUM = (Valuations_in A --> TRUE) &
       for p,q being Element of CQC-WFF,
       x being bound_QC-variable, k being Nat,
       ll being CQC-variable_list of k,
       P being QC-pred_symbol of k 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));
  correctness
   proof
     set D = Funcs(Valuations_in A, BOOLEAN);
     set V = Valuations_in A --> TRUE;
     deffunc A(Nat, QC-pred_symbol of $1, CQC-variable_list of $1)
       = $3 'in' (J.$2);
     deffunc N(Element of D) = 'not' $1;
     deffunc C(Element of D, Element of D) = $1 '&' $2;
     deffunc Q(bound_QC-variable, Element of D) = FOR_ALL($1,$2);
     thus (ex d being Element of D st
    ex F being Function of CQC-WFF, D st d = F.p &
      F.VERUM = V &
      for r,s being (Element of CQC-WFF),
          x being bound_QC-variable, k being Nat
      for l being CQC-variable_list of k
       for P being QC-pred_symbol of k holds
         F.(P!l) = A(k,P,l) &
         F.('not' r) = N(F.r) &
         F.(r '&' s) = C(F.r,F.s) &
         F.All(x,r) = Q(x,F.r) )
  & (for d1,d2 being Element of D st
     (ex F being Function of CQC-WFF, D st d1 = F.p &
       F.VERUM = V &
       for r,s being (Element of CQC-WFF),
          x being bound_QC-variable, k being Nat
       for l being CQC-variable_list of k
         for P being QC-pred_symbol of k holds
           F.(P!l) = A(k,P,l) &
           F.('not' r) = N(F.r) &
           F.(r '&' s) = C(F.r,F.s) &
           F.All(x,r) = Q(x,F.r) ) &
     (ex F being Function of CQC-WFF, D st d2 = F.p &
       F.VERUM = V &
       for r,s being (Element of CQC-WFF),
          x being bound_QC-variable, k being Nat
       for l being CQC-variable_list of k
         for P being QC-pred_symbol of k holds
           F.(P!l) = A(k,P,l) &
           F.('not' r) = N(F.r) &
           F.(r '&' s) = C(F.r,F.s) &
           F.All(x,r) = Q(x,F.r) )
    holds d1 = d2) from CQC_Def_correctness;
   end;
end;

Lm1:
for A, J holds
 Valid(VERUM,J) = (Valuations_in 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 A, BOOLEAN);
     set V = Valuations_in A --> TRUE;
     deffunc A(Nat, QC-pred_symbol of $1, CQC-variable_list of $1)
       = $3 'in' (J.$2);
     deffunc N(Element of D) = 'not' $1;
     deffunc C(Element of D, Element of D) = $1 '&' $2;
     deffunc Q(bound_QC-variable, Element of D) = FOR_ALL($1,$2);
     deffunc X(Element of CQC-WFF) = Valid($1, J);
A1:for p holds for d be Element of D holds (
 d = (X(p)) iff
    ex F being Function of CQC-WFF, D st
      d = F.p &
      F.VERUM = V &
        for p,q being Element of CQC-WFF,
        x being bound_QC-variable, k being Nat,
        ll being CQC-variable_list of k,
        P being QC-pred_symbol of k holds
      F.(P!ll) = A(k, P, ll) &
      F.('not' p) = N(F.p) &
      (F.(p '&' q)) = C(F.p,F.q) &
      F.(All(x,p)) = Q(x,F.p)) by Def11;
 thus X(VERUM) = V from CQC_Def_VERUM(A1);
 hereby let k, ll, P;
 thus X(P!ll) = A(k,P,ll) from CQC_Def_atomic(A1);
 end;
 hereby let p;
 thus X('not' p) = N(X(p)) from CQC_Def_negative(A1);
 end;
 hereby let q;
 thus X(p '&' q) = C(X(p), X(q)) from QC_Def_conjunctive(A1);
 end;
 let x;
 thus X(All(x,p)) = Q(x,X(p)) from QC_Def_universal(A1);
end;

canceled 4;

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

theorem
  Th14: Valid(VERUM,J).v = TRUE
   proof
       (Valuations_in A --> TRUE).v = TRUE by FUNCOP_1:13;
     hence Valid(VERUM,J).v = TRUE by Lm1;
   end;

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

theorem
  Th16: p = P!ll & r = J.P implies (v*'ll in r iff Valid(p,J).v = TRUE)
  proof assume
 A1:  p = P!ll & r = J.P;
   A2: now assume v*'ll in r;
         then (ll 'in' (J.P)).v = TRUE by A1,Def9;
         hence Valid(p,J).v = TRUE by A1,Lm1;
       end;
         now assume Valid(p,J).v = TRUE;
         then (ll 'in' (J.P)).v <> FALSE by A1,Lm1,MARGREL1:38;
         hence v*'ll in r by A1,Def9;
       end;
       hence thesis by A2;
  end;

theorem Th17:
   p = P!ll & r = J.P implies (not (v*'ll in r) iff Valid(p,J).v = FALSE)
  proof assume
 A1:  p = P!ll & r = J.P;
   A2: now assume not (v*'ll in r);
         then (ll 'in' (J.P)).v = FALSE by A1,Def9;
         hence Valid(p,J).v = FALSE by A1,Lm1;
       end;
         now assume Valid(p,J).v = FALSE;
         then (ll 'in' (J.P)).v <> TRUE by A1,Lm1,MARGREL1:38;
         hence not (v*'ll in r) by A1,Def9;
       end;
       hence thesis by A2;
  end;

canceled;

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

theorem
  Th20: Valid('not' p,J).v = 'not'(Valid(p,J).v)
  proof
      Valid('not' p,J).v = ('not' Valid(p,J)).v by Lm1;
    hence Valid('not' p,J).v = 'not' (Valid(p,J).v) by Def5;
  end;

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

theorem
  Th22: 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 Valid(p '&'q ,J).v = (Valid(p,J).v) '&' (Valid(q,J).v) by Def6;
  end;

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

theorem
  Th24: Valid(p '&' 'not' p,J).v = FALSE
  proof
 A1:  Valid(p '&' 'not' p,J).v = (Valid(p,J).v) '&' (Valid('not' p,J).v)
 by Th22
                       .= (Valid(p,J).v) '&' 'not'(Valid(p,J).v) by Th20;
A2:  now assume (Valid(p,J)).v = TRUE;
       then 'not'(Valid(p,J).v) = FALSE by MARGREL1:41;
       hence (Valid(p,J).v) '&' 'not'(Valid(p,J).v) = FALSE by MARGREL1:45;
     end;
         Valid(p,J).v = FALSE implies (Valid(p,J).v) '&' 'not'
(Valid(p,J).v) = FALSE
 by MARGREL1:45;
    hence Valid(p '&' 'not' p,J).v = FALSE by A1,A2,MARGREL1:39;
  end;

theorem
     Valid('not'(p '&' 'not' p),J).v = TRUE
  proof
      Valid('not'(p '&' 'not' p),J).v = 'not'(Valid(p '&' 'not' p,J).v) by Th20
                         .= 'not' FALSE by Th24;
    hence thesis by MARGREL1:41;
  end;

definition
 let A, p, J, v;
  pred J,v |= p means
:Def12: Valid(p,J).v = TRUE;
end;

canceled;

theorem
    J,v |= P!ll iff (ll 'in' (J.P)).v = TRUE
 proof
A1:now assume J,v |= P!ll;
  then Valid(P!ll,J).v = TRUE by Def12;
     hence (ll 'in' (J.P)).v = TRUE by Lm1;
   end;
     now assume (ll 'in' (J.P)).v = TRUE;
     then Valid(P!ll,J).v = TRUE by Lm1;
     hence J,v |= P!ll by Def12;
   end;
   hence thesis by A1;
 end;

theorem
    J,v |= 'not' p iff not J,v |= p
 proof
A1: now assume J,v |= 'not' p;
       then Valid('not' p,J).v = TRUE by Def12;
       then 'not' Valid(p,J).v = TRUE by Lm1;
       then 'not'(Valid(p,J).v) = TRUE by Def5;
       then Valid(p,J).v = FALSE by MARGREL1:41;
       then not (Valid(p,J).v = TRUE) by MARGREL1:43;
      hence not J,v |= p by Def12;
    end;
      now assume not J,v |= p;
       then not (Valid(p,J).v = TRUE) by Def12;
       then Valid(p,J).v = FALSE by MARGREL1:43;
       then 'not'(Valid(p,J).v) = TRUE by MARGREL1:41;
       then 'not' Valid(p,J).v = TRUE by Def5;
       then Valid('not' p,J).v = TRUE by Lm1;
      hence J,v |= 'not' p by Def12;
    end;
    hence thesis by A1;
  end;

theorem
    J,v |= (p '&' q) iff J,v |= p & J,v |= q
  proof
A1: now assume J,v |= (p '&' q);
       then Valid(p '&' q,J).v = TRUE by Def12;
       then (Valid(p,J) '&' Valid(q,J)).v = TRUE by Lm1;
       then (Valid(p,J).v) '&' (Valid(q,J).v) = TRUE by Def6;
       then Valid(p,J).v = TRUE & Valid(q,J).v = TRUE by MARGREL1:45;
       hence J,v |= p & J,v |= q by Def12;
    end;
      now assume J,v |= p & J,v |= q;
       then Valid(p,J).v = TRUE & Valid(q,J).v = TRUE by Def12;
       then (Valid(p,J).v) '&' (Valid(q,J).v) = TRUE by MARGREL1:45;
       then (Valid(p,J) '&' Valid(q,J)).v = TRUE by Def6;
       then Valid(p '&' q,J).v = TRUE by Lm1;
       hence J,v |= (p '&' q) by Def12;
    end;
    hence thesis by A1;
  end;

theorem
  Th30: J,v |= All(x,p) iff FOR_ALL(x,Valid(p,J)).v = TRUE
 proof
A1:now assume J,v |= All(x,p);
  then Valid(All(x,p),J).v = TRUE by Def12;
     hence FOR_ALL(x,Valid(p,J)).v = TRUE by Lm1;
   end;
     now assume FOR_ALL(x,Valid(p,J)).v = TRUE;
     then Valid(All(x,p),J).v = TRUE by Lm1;
     hence J,v |= All(x,p) by Def12;
   end;
   hence thesis by A1;
 end;

theorem
  Th31: 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
A1:now assume J,v |= All(x,p);
   then FOR_ALL(x,Valid(p,J)).v = TRUE by Th30;
     hence
       for v1 st for y st x <> y holds v1.y = v.y holds Valid(p,J).v1 = TRUE
by Th8;
   end;
     now 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 Th8;
      hence J,v |= All(x,p) by Th30;
   end;
   hence thesis by A1;
 end;

 theorem
     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 Th20
                    .= 'not'('not'(Valid(p,J).v)) by Th20
                    .= Valid(p,J).v by MARGREL1:40;
    end;
    hence Valid('not' 'not' p,J) = Valid(p,J) by FUNCT_2:113;
  end;

theorem
 Th33: Valid(p '&' p,J) = Valid(p,J)
  proof
      now let v;
 A1:    Valid(p '&' p,J).v = (Valid(p,J).v) '&' (Valid(p,J).v) by Th22;
   then A2:  (Valid(p '&' p, J).v) = TRUE implies Valid(p, J).v = TRUE by
MARGREL1:45;
          (Valid(p '&' p, J).v) = FALSE implies Valid(p, J).v = FALSE by A1,
MARGREL1:51;
     hence Valid(p '&'p, J).v = Valid(p,J).v by A2,MARGREL1:39;
    end;
    hence Valid(p '&' p,J) = Valid(p,J) by FUNCT_2:113;
  end;

canceled;

theorem
 Th35: J,v |= p => q iff
          Valid(p, J).v = FALSE or Valid(q, J).v = TRUE
   proof
 A1: now assume J,v |= p => q;
       then Valid(p => q, J).v = TRUE by Def12;
       then Valid('not'(p '&' 'not' q), J).v = TRUE by QC_LANG2:def 2;
       then 'not'(Valid(p '&' 'not' q, J).v) = TRUE by Th20;
       then Valid(p '&' 'not' q, J).v = FALSE by MARGREL1:41;
       then (Valid(p, J).v) '&' (Valid('not' q, J).v) = FALSE by Th22;
       then (Valid(p, J).v) '&' 'not'(Valid(q, J).v) = FALSE by Th20;
       then Valid(p, J).v = FALSE or 'not' (Valid(q, J).v) = FALSE by MARGREL1:
45;
       hence Valid(p, J).v = FALSE or Valid(q, J).v = TRUE by MARGREL1:41;
     end;
       now assume A2: Valid(p, J).v = FALSE or Valid(q, J).v = TRUE;
  A3: now assume Valid(p, J).v = FALSE;
         then (Valid(p, J).v) '&' (Valid('not' q, J).v) = FALSE by MARGREL1:45
;
         then Valid(p '&' 'not' q, J).v = FALSE by Th22;
         then 'not'(Valid(p '&' 'not' q, J).v) = TRUE by MARGREL1:41;
         then Valid('not'(p '&' 'not' q), J).v = TRUE by Th20;
         then Valid(p => q, J).v = TRUE by QC_LANG2:def 2;
         hence J,v |= p => q by Def12;
       end;
         now assume A4: Valid(q, J).v = TRUE;
         assume not J,v |= p => q;
          then Valid(p => q, J).v <> TRUE by Def12;
          then Valid(p => q, J).v = FALSE by MARGREL1:39;
          then Valid('not'(p '&' 'not' q), J).v = FALSE by QC_LANG2:def 2;
          then 'not'(Valid(p '&' 'not' q, J).v) = FALSE by Th20;
          then Valid(p '&' 'not' q, J).v = TRUE by MARGREL1:41;
          then (Valid(p, J).v) '&' (Valid('not' q, J).v) = TRUE by Th22;
          then (Valid(p, J).v) '&' 'not'(Valid(q, J).v) = TRUE by Th20;
          then Valid(p, J).v = TRUE & 'not' (Valid(q, J).v) = TRUE by MARGREL1:
45;
          hence contradiction by A4,MARGREL1:38,41;
       end;
       hence J,v |= p => q by A2,A3;
     end;
    hence thesis by A1;
   end;

theorem
  Th36: J,v |= p => q iff (J,v |= p implies J,v |= q)
 proof
  A1: now assume J,v |= p => q;
    then A2: Valid(p, J).v = FALSE or Valid(q, J).v = TRUE by Th35;
          now assume J,v |= p;
          then Valid(p, J).v = TRUE by Def12;
          hence J,v |= q by A2,Def12,MARGREL1:43;
        end;
        hence J,v |= p implies J,v |= q;
      end;
        now assume J,v |= p implies J,v |= q;
        then Valid(p, J).v = TRUE implies Valid(q, J).v = TRUE by Def12;
        then Valid(p, J).v = FALSE or Valid(q, J).v = TRUE by MARGREL1:43;
        hence J,v |= p => q by Th35;
      end;
      hence thesis by A1;
 end;

theorem
  Th37: for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
         FOR_ALL(x,p).v = TRUE implies p.v = TRUE
  proof let p be Element of Funcs(Valuations_in A,BOOLEAN);
         for y st x <> y holds v.y = v.y;
     hence thesis by Th8;
  end;

definition
 let A, J, p;
  pred J |= p means
:Def13: 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 MARGREL1:39;
     suppose that
A1:   z = TRUE and
A2:   w = TRUE;
         w '&' z = TRUE by A1,A2,MARGREL1:45;
       then 'not'(w '&' z) = FALSE by MARGREL1:41;
       then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:45;
       then 'not'(u '&' 'not' w) '&' ('not'
(w '&' z) '&' (u '&' z)) = FALSE by MARGREL1:45;
      hence thesis by MARGREL1:41;
     suppose that
A3:   w = FALSE and
A4:   u = TRUE;
         'not' w = TRUE by A3,MARGREL1:41;
       then u '&' 'not' w = TRUE by A4,MARGREL1:45;
       then 'not'(u '&' 'not' w) = FALSE by MARGREL1:41;
       then 'not'(u '&' 'not' w) '&' ('not'
(w '&' z) '&' (u '&' z)) = FALSE by MARGREL1:45;
      hence thesis by MARGREL1:41;
     suppose u = FALSE;
        then u '&' z = FALSE by MARGREL1:45;
        then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:45;
        then 'not'(u '&' 'not' w) '&' ('not'
(w '&' z) '&' (u '&' z)) = FALSE by MARGREL1:45;
       hence thesis by MARGREL1:41;
      suppose z = FALSE;
        then u '&' z = FALSE by MARGREL1:45;
        then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:45;
        then 'not'(u '&' 'not' w) '&' ('not'
(w '&' z) '&' (u '&' z)) = FALSE by MARGREL1:45;
       hence thesis by MARGREL1:41;
    end;

reserve w,v2 for Element of Valuations_in A,
        z for bound_QC-variable;

scheme Lambda_Val {A() -> non empty set, Y, Z() -> bound_QC-variable,
                     V1, V2() -> Element of Valuations_in A()}:
 ex v being Element of Valuations_in A() st
  (for x being bound_QC-variable st x <> Y() holds v.x = V1().x) &
                                                 v.Y() = V2().Z()
 proof
   defpred C[set] means for x1 st x1 = $1 holds x1 <> Y();
   deffunc F(set) = V1().$1;
   deffunc G(set) = V2().Z();
  A1:   for x being set st x in bound_QC-variables holds
           (C[x] implies F(x) in A()) &
           (not C[x] implies G(x) in A())
 by FUNCT_2:7;
     consider f being Function of bound_QC-variables, A() such that
  A2:   for x being set st x in bound_QC-variables holds
           (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))
              from Lambda1C(A1);
      dom f = bound_QC-variables & rng f c= A() by FUNCT_2:def 1,RELSET_1:12;
    then f is Element of Funcs(bound_QC-variables,A()) by FUNCT_2:def 2;
    then reconsider f as Element of Valuations_in A() by Def1;
    take f;
     now let x be bound_QC-variable;
          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;

canceled;

theorem
 Th39:
  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] 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;
A2:   rng ll c= bound_QC-variables by CQC_LANG:def 5;

     thus PP[VERUM]
     proof assume not x in still_not-bound_in VERUM;
        thus for v,w st for y st x<>y holds w.y = v.y holds
                                    Valid(VERUM,J).v = Valid(VERUM,J).w
       proof let v,w such that
            for y st x <> y holds w.y = v.y;
             Valid(VERUM,J).v = TRUE & Valid(VERUM,J).w = TRUE by Th14;
           hence Valid(VERUM,J).v = Valid(VERUM,J).w;
       end;
     end;

     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 assume
         A6:  Valid(P!ll,J).v = TRUE;
              then (ll 'in' (J.P)).v = TRUE by Lm1;
              then not (ll 'in' (J.P)).v = FALSE by MARGREL1:43;
     then A7:      v*'ll in (J.P) by Def9;
A8:         len (v*'ll) = k & len (w*'ll) = k by Def8;
            now let i; assume
         A9:     1 <= i & i <= len (v*'ll);
         then A10:     (v*'ll).i = v.(ll.i) by A8,Def8;
         A11:     len (v*'ll) = len ll by A8,QC_LANG1:def 8;
         A12:     ll.i in bound_QC-variables
                  proof
                      i in dom ll by A9,A11,FINSEQ_3:27;
                    then ll.i in rng ll by FUNCT_1:def 5;
                   hence ll.i in bound_QC-variables by A2;
                  end;
         A13:     ll.i <> x
                   proof
                     reconsider M = still_not-bound_in ll as set;
                    not x in M by A3,QC_LANG3:9;
                     then not x in variables_in(ll,bound_QC-variables) by
QC_LANG3:6;
                       then not x in {ll.i2 where i2 is Nat : 1 <= i2 & i2 <=
len ll &
                                  ll.i2 in bound_QC-variables} by QC_LANG3:def
2;
                     hence ll.i <> x by A9,A11;
                   end;
                 reconsider z = ll.i as bound_QC-variable by A12;
                   w.z = v.z by A4,A13;
                 hence (v*'ll).i = (w*'ll).i by A8,A9,A10,Def8;
             end;
             then w*'ll in (J.P) by A7,A8,FINSEQ_1:18;
           then (ll 'in' (J.P)).w = TRUE by Def9;
             hence thesis by A6,Lm1;
            end;
             now assume
        A14:   Valid(P!ll,J).v = FALSE;
              then (ll 'in' (J.P)).v = FALSE by Lm1;
              then not (ll 'in' (J.P)).v = TRUE by MARGREL1:43;
     then A15:      not v*'ll in (J.P) by Def9;
     A16:     len (v*'ll) = k & len (w*'ll) = k by Def8;
            now let i; assume
         A17:     1 <= i & i <= len (v*'ll);
         then A18:     (v*'ll).i = v.(ll.i) by A16,Def8;
         A19:     len (v*'ll) = len ll by A16,QC_LANG1:def 8;
         A20:     ll.i in bound_QC-variables
                  proof
                      i in dom ll by A17,A19,FINSEQ_3:27;
                    then ll.i in rng ll by FUNCT_1:def 5;
                   hence ll.i in bound_QC-variables by A2;
                  end;
         A21:     ll.i <> x
                   proof
                     reconsider M = still_not-bound_in ll as set;
                    not x in M by A3,QC_LANG3:9;
                     then not x in variables_in(ll,bound_QC-variables) by
QC_LANG3:6;
                       then not x in {ll.i2 where i2 is Nat : 1 <= i2 & i2 <=
len ll &
                                  ll.i2 in bound_QC-variables} by QC_LANG3:def
2;
                     hence ll.i <> x by A17,A19;
                   end;
                 reconsider z = ll.i as bound_QC-variable by A20;
                   w.z = v.z by A4,A21;
                 hence (v*'ll).i = (w*'ll).i by A16,A17,A18,Def8;
             end;
             then not w*'ll in (J.P) by A15,A16,FINSEQ_1:18;
           then (ll 'in' (J.P)).w = FALSE by Def9;
             hence thesis by A14,Lm1;
           end;
           hence thesis by A5,MARGREL1:39;
       end;
      end;

     thus PP[s] implies PP['not' s]
       proof
        assume that
    A22:   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
    A23:   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
     A24:    for y st x<>y holds w.y = v.y;
 A25:        now assume
         A26:  Valid('not' s,J).v = TRUE;
              then 'not'(Valid(s,J).v) = TRUE by Th20;
              then Valid(s,J).v = FALSE by MARGREL1:41;
              then Valid(s,J).w = FALSE by A22,A23,A24,QC_LANG3:11;
              then 'not'(Valid(s,J).w) = TRUE by MARGREL1:41;
              hence thesis by A26,Th20;
            end;
              now assume
         A27:  Valid('not' s,J).v = FALSE;
              then 'not'(Valid(s,J).v) = FALSE by Th20;
              then Valid(s,J).v = TRUE by MARGREL1:41;
              then Valid(s,J).w = TRUE by A22,A23,A24,QC_LANG3:11;
              then 'not'(Valid(s,J).w) = FALSE by MARGREL1:41;
              hence thesis by A27,Th20;
            end;
            hence thesis by A25,MARGREL1:39;
         end;
       end;

     thus PP[s] & PP[t] implies PP[s '&' t]
       proof
        assume that
    A28:   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
    A29:   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
    A30:   not x in still_not-bound_in s '&' t;
A31:          not (x in (still_not-bound_in s) \/ (still_not-bound_in t))
                                                   by A30,QC_LANG3:14;
        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
     A32:    for y st x<>y holds w.y = v.y;
 A33:        now assume
         A34:  Valid(s '&' t ,J).v = TRUE;
              then (Valid(s,J).v) '&' (Valid(t,J).v) = TRUE by Th22;
              then Valid(s,J).v = TRUE & Valid(t,J).v = TRUE by MARGREL1:45;
              then Valid(s,J).w = TRUE & Valid(t,J).w = TRUE by A28,A29,A31,A32
,XBOOLE_0:def 2;
              then (Valid(s,J).w) '&' (Valid(t,J).w) = TRUE by MARGREL1:45;
              hence thesis by A34,Th22;
            end;
              now assume
         A35:  Valid(s '&' t ,J).v = FALSE;
then A36:              (Valid(s,J).v) '&' (Valid(t,J).v) = FALSE by Th22;
   A37:       now assume Valid(s,J).v = FALSE;
                then Valid(s,J).w = FALSE by A28,A31,A32,XBOOLE_0:def 2;
                then (Valid(s,J).w) '&' (Valid(t,J).w) = FALSE by MARGREL1:45;
                hence thesis by A35,Th22;
              end;
                now assume Valid(t,J).v = FALSE;
                then Valid(t,J).w = FALSE by A29,A31,A32,XBOOLE_0:def 2;
                then (Valid(s,J).w) '&' (Valid(t,J).w) = FALSE by MARGREL1:45;
                hence thesis by A35,Th22;
              end;
              hence thesis by A36,A37,MARGREL1:45;
            end;
            hence thesis by A33,MARGREL1:39;
          end;
        end;

     thus PP[s] implies PP[All(y,s)]
       proof
        assume that
    A38:   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
    A39:   not x in still_not-bound_in All(y,s);
A40:          not (x in (still_not-bound_in s) \ {y}) by A39,QC_LANG3:16;

        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
     A41:    for z st x<>z holds w.z = v.z;
 A42:        now assume
         A43:  Valid(All(y,s),J).v = TRUE;
then A44:              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
         A45:          for z st y<>z holds v1.z = w.z;
       A46:     now assume
        A47:        not x in (still_not-bound_in s);
                  consider v2 such that
       A48:          (for z st z <> y holds v2.z = v.z) &
                                           v2.y = v1.y from Lambda_Val;
       A49:        for z st x <> z holds v2.z = v1.z
                    proof let z such that A50: x <> z;
                     now assume A51: z <> y; hence
                          v2.z = v.z by A48
                            .= w.z by A41,A50
                            .= v1.z by A45,A51;
                      end;
                      hence thesis by A48;
                    end;
                    Valid(s,J).v2 = TRUE by A44,A48,Th8;
                  hence Valid(s,J).v1 = TRUE by A38,A47,A49;
                end;
                  now assume x in {y};
            then A52:   x = y by TARSKI:def 1;
                 for z st y <> z holds v1.z = v.z
                   proof let z; assume A53: y <> z;
                     hence v.z = w.z by A41,A52
                             .= v1.z by A45,A53;
                   end;
                  hence Valid(s,J).v1 = TRUE by A44,Th8;
                end;
                hence Valid(s,J).v1 = TRUE by A40,A46,XBOOLE_0:def 4;
              end;
              then FOR_ALL(y,Valid(s,J)).w = TRUE by Th8;
              hence thesis by A43,Lm1;
            end;
              now assume
         A54:  Valid(All(y,s),J).v = FALSE;
              then FOR_ALL(y,Valid(s,J)).v = FALSE by Lm1;
              then consider v1 such that
         A55:     Valid(s,J).v1 = FALSE and
         A56:     for z st y <> z holds v1.z = v.z by Th7;
                ex v2 st Valid(s,J).v2 = FALSE & for z st y<>z holds v2.z = w.z
              proof
     A57:       now assume
        A58:        not x in (still_not-bound_in s);
                  consider v2 such that
       A59:          (for z st z <> y holds v2.z = w.z) &
                                           v2.y = v1.y from Lambda_Val;
                  take v2;
                    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 = w.z by A59
                            .= v.z by A41,A60
                            .= v1.z by A56,A61;
                      end;
                      hence thesis by A59;
                    end;
                  hence Valid(s,J).v2 = FALSE by A38,A55,A58;
                  thus for z st y <> z holds v2.z = w.z by A59;
                end;
                  now assume A62: x in {y};
                   take v2 = v1;
                  thus Valid(s,J).v2 = FALSE by A55;
                    for z st y <> z holds v1.z = w.z
                  proof let z; assume
             A63:   y <> z;
             then A64:   x <> z by A62,TARSKI:def 1;
                    thus v1.z = v.z by A56,A63
                             .= w.z by A41,A64;
                  end;
                  hence for z st y <> z holds v2.z = w.z;
                end;
                hence ex v2 st Valid(s,J).v2 = FALSE &
                   for z st y<>z holds v2.z = w.z by A40,A57,XBOOLE_0:def 4;
              end;
              then FOR_ALL(y,Valid(s,J)).w = FALSE by Th7;
              hence thesis by A54,Lm1;
            end;
            hence thesis by A42,MARGREL1:39;
         end;
       end;
   end;
     for s holds PP[s] from CQC_Ind(A1);
   hence thesis;
 end;

theorem
 Th40:
  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
  proof
   assume that
 A1: J,v |= p and
 A2: not x in still_not-bound_in p;
      now let w;
      assume A3: for y st x<>y holds w.y = v.y;
        Valid(p,J).v = TRUE by A1,Def12;
      then Valid(p,J).w = TRUE by A2,A3,Th39;
      hence J,w |= p by Def12;
    end;
    hence thesis;
  end;

theorem
 Th41:
  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:      J,v |= All(x,p);
      let w;
      assume for y st x<>y holds w.y = v.y;
      then Valid(p,J).w = TRUE by A2,Th31;
      hence J,w |= p by Def12;
    end;
      now assume
   A3: 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
      proof let w;
        assume for y st x<>y holds w.y = v.y;
        then J,w |= p by A3;
        hence Valid(p,J).w = TRUE by Def12;
      end;
      hence J,v |= All(x,p) by Th31;
    end;
   hence thesis by A1;
 end;

reserve u,w for Element of Valuations_in A;
reserve s' for QC-formula;

theorem
 Th42:
  x <> y & p = s'.x & q = s'.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] 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;

    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 let x,y,p,q such that
   A3:    x <> y & p = s.x & q = s.y;
          let v such that
    A4:    v.x = v.y;
          consider k being Nat, P being (QC-pred_symbol of k),
            l being QC-variable_list of k such that
   A5:    s = P!l by A2,QC_LANG1:def 17;
   A6:   p = P!Subst(l, a.0 .-->x) & q = P!Subst(l, a.0 .-->y)
                                               by A3,A5,CQC_LANG:30;
          set lx = Subst(l, a.0 .-->x),
              ly = Subst(l, a.0 .-->y);
   A7:    {lx.i : 1 <= i & i <= len lx & lx.i in free_QC-variables} = {} &
          {lx.j : 1 <= j & j <= len lx & lx.j in fixed_QC-variables} = {}
                                                         by A6,CQC_LANG:17;
            {ly.i : 1 <= i & i <= len ly & ly.i in free_QC-variables} = {} &
          {ly.j : 1 <= j & j <= len ly & ly.j in fixed_QC-variables} = {}
                                                  by A6,CQC_LANG:17;
          then reconsider lx,ly as CQC-variable_list of k by A7,CQC_LANG:15;
    A8:   len (v*'lx) = k &
            for i st 1 <= i & i <= k holds (v*'lx).i = v.(lx.i) by Def8;
    A9:   len (v*'ly) = k &
            for i st 1 <= i & i <= k holds (v*'ly).i = v.(ly.i) by Def8;
    A10:   v*'lx = v*'ly
          proof
          now let i; assume
       A11:    1 <= i & i <= len (v*'lx);
       then A12:    1 <= i & i <= len l by A8,QC_LANG1:def 8;
     A13:     now assume l.i <> a.0;
then A14:                lx.i = l.i & ly.i = l.i by A12,CQC_LANG:11;
                  v.(lx.i) = (v*'lx).i & v.(ly.i) = (v*'ly).i by A8,A11,Def8;
                hence (v*'lx).i = (v*'ly).i by A14;
              end;
                now assume l.i = a.0;
then A15:                lx.i = x & ly.i = y by A12,CQC_LANG:11;
                  v.(lx.i) = (v*'lx).i & v.(ly.i) = (v*'ly).i by A8,A11,Def8;
                hence (v*'lx).i = (v*'ly).i by A4,A15;
              end;
              hence (v*'lx).i = (v*'ly).i by A13;
            end;
                hence thesis by A8,A9,FINSEQ_1:18;
              end;
  A16:     now assume
           Valid(p,J).v = TRUE;
           then v*'lx in J.P by A6,Th16;
            hence Valid(q,J).v = TRUE by A6,A10,Th16;
          end;
            now assume
           Valid(p,J).v = FALSE;
         then not (v*'lx in J.P) by A6,Th17;
            hence Valid(q,J).v = FALSE by A6,A10,Th17;
          end;
          hence thesis by A16,MARGREL1:39;
        end;
      end;
    thus PP[VERUM]
    proof let x,y,p,q such that
 A17:  x <> y & p = VERUM.x & q = VERUM.y;
      let v such that v.x = v.y;
        p = VERUM & q = VERUM by A17,CQC_LANG:28;
      hence thesis;
    end;
    thus s is negative & PP[the_argument_of s] implies PP[s]
    proof assume that
  A18: s is negative and
  A19: 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
  A20:   x <> y & p = s.x & q = s.y;
        let v such that
   A21:     v.x = v.y;
   A22:   s.x = 'not'((the_argument_of s).x) & s.y = 'not'
((the_argument_of s).y)
                                                        by A18,CQC_LANG:31;
         then reconsider pa = (the_argument_of s).x as Element of CQC-WFF by
A20,CQC_LANG:18;
         reconsider qa = (the_argument_of s).y as Element of CQC-WFF by A20,A22
,CQC_LANG:18;
 A23:        now assume
                Valid(p,J).v = TRUE;
              then 'not'(Valid(pa,J).v) = TRUE by A20,A22,Th20;
              then Valid(pa,J).v = FALSE by MARGREL1:41;
              then Valid(qa,J).v = FALSE by A19,A21;
              then 'not'(Valid(qa,J).v) = TRUE by MARGREL1:41;
              hence Valid(q,J).v = TRUE by A20,A22,Th20;
            end;
              now assume
                Valid(p,J).v = FALSE;
              then 'not'(Valid(pa,J).v) = FALSE by A20,A22,Th20;
              then Valid(pa,J).v = TRUE by MARGREL1:41;
              then Valid(qa,J).v = TRUE by A19,A21;
              then 'not'(Valid(qa,J).v) = FALSE by MARGREL1:41;
              hence Valid(q,J).v = FALSE by A20,A22,Th20;
            end;
            hence thesis by A23,MARGREL1:39;
         end;
      end;
    thus (s is conjunctive & PP[the_left_argument_of s] &
          PP[the_right_argument_of s]) implies PP[s]
    proof assume that
 A24:  s is conjunctive and
 A25:  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
 A26:  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
 A27:    x <> y & p = s.x & q = s.y;
        let v such that
    A28:    v.x = v.y;
  A29:    s.x=((the_left_argument_of s).x) '&' ((the_right_argument_of s).x) &
          s.y=((the_left_argument_of s).y) '&' ((the_right_argument_of s).y)
                                                         by A24,CQC_LANG:33;
          then reconsider pla = (the_left_argument_of s).x ,
                     pra = (the_right_argument_of s).x as Element of CQC-WFF
 by A27,CQC_LANG:19;
          reconsider qla = (the_left_argument_of s).y ,
                     qra = (the_right_argument_of s).y as Element of CQC-WFF
 by A27,A29,CQC_LANG:19;
A30:        now assume
               Valid(p,J).v = TRUE;
             then (Valid(pla,J).v) '&' (Valid(pra,J).v) = TRUE by A27,A29,Th22
;
             then Valid(pla,J).v = TRUE & Valid(pra,J).v = TRUE by MARGREL1:45
;
             then Valid(qla,J).v = TRUE & Valid(qra,J).v = TRUE by A25,A26,A28
;
             then (Valid(qla,J).v) '&' (Valid(qra,J).v) = TRUE by MARGREL1:45;
             hence Valid(q,J).v = TRUE by A27,A29,Th22;
           end;
             now assume
      A31:   Valid(p,J).v = FALSE;
then A32:             (Valid(pla,J).v) '&' (Valid(pra,J).v) = FALSE by A27,A29,
Th22
;
 A33:         now assume Valid(pla,J).v = FALSE;
                then Valid(qla,J).v = FALSE by A25,A28;
                then (Valid(qla,J).v) '&' (Valid(qra,J).v) = FALSE by MARGREL1:
45;
                hence thesis by A27,A29,A31,Th22;
              end;
                now assume Valid(pra,J).v = FALSE;
                then Valid(qra,J).v = FALSE by A26,A28;
                then (Valid(qla,J).v) '&' (Valid(qra,J).v) = FALSE by MARGREL1:
45;
                hence thesis by A27,A29,A31,Th22;
              end;
             hence thesis by A32,A33,MARGREL1:45;
           end;
           hence thesis by A30,MARGREL1:39;
        end;
      end;
    thus s is universal & PP[the_scope_of s] implies PP[s]
    proof assume that
  A34: s is universal and
  A35: 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 being bound_QC-variable, pp being Element of QC-WFF such that
  A36: s = All(xx,pp) by A34,QC_LANG1:def 20;
  A37: xx = bound_in s by A34,A36,QC_LANG1:def 26;
     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
  A38:   x <> y & p = s.x & q = s.y;
        let v such that
     A39:   v.x = v.y;
 A40:   now assume
  A41:   x <> bound_in s;
     then s.x = All(bound_in s, (the_scope_of s).x) by A34,CQC_LANG:36;
then reconsider ps = (the_scope_of s).x as Element of CQC-WFF by A38,CQC_LANG:
23;
  A42:   All(bound_in s, ps) = p by A34,A38,A41,CQC_LANG:36;
  A43:   now assume
     A44:    y <> bound_in s;
      then s.y = All(bound_in s, (the_scope_of s).y) by A34,CQC_LANG:36;
           then reconsider qs = (the_scope_of s).y as Element of CQC-WFF by A38
,CQC_LANG:23;
  A45:    All(bound_in s, qs) = q by A34,A38,A44,CQC_LANG:36;
      A46:  Valid(All(bound_in s, ps),J) = FOR_ALL(bound_in s, Valid(ps,J)) &
           Valid(All(bound_in s, qs),J) = FOR_ALL(bound_in s, Valid(qs,J))
                                                                by Lm1;
    A47:   now assume
A48:              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
          A49:      for y st (bound_in s) <> y holds v1.y = v.y;
                then A50: v1.x = v.x & v1.y = v.y by A41,A44;
                  Valid(ps,J).v1 = TRUE by A42,A46,A48,A49,Th8;
                hence Valid(qs,J).v1 = TRUE by A35,A39,A50;
              end;
              hence Valid(q,J).v = TRUE by A45,A46,Th8;
            end;
              now assume
A51:              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
            A52:  Valid(ps,J).v1 = FALSE and
            A53:  for y st (bound_in s) <> y holds v1.y = v.y by A42,A46,A51,
Th7;
                   v1.x = v.x & v1.y = v.y by A41,A44,A53;
                 then Valid(qs,J).v1 = FALSE by A35,A39,A52;
                hence thesis by A53;
              end;
              hence Valid(q,J).v = FALSE by A45,A46,Th7;
            end;
            hence thesis by A47,MARGREL1:39;
         end;
           now assume
A54:           y = bound_in s;
       then q = All(y,pp) by A36,A37,A38,CQC_LANG:37;
           hence thesis by A36,A37,A38,A54,CQC_LANG:40;
         end;
         hence thesis by A43;
       end;
         now assume
A55:      x = bound_in s;
     then p = All(x,pp) by A36,A37,A38,CQC_LANG:37;
         hence thesis by A36,A37,A38,A55,CQC_LANG:40;
       end;
       hence thesis by A40;
     end;
    end;
  end;
     for s being Element of QC-WFF holds PP[s] from QC_Ind2 (A1);
   hence thesis;
 end;

theorem
 Th43:
  x <> y & not x in still_not-bound_in s' implies
    not x in still_not-bound_in (s'.y)
 proof
   defpred PP[Element of QC-WFF] 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;
    thus s is atomic implies PP[s]
      proof assume that
        A2: s is atomic and
        A3: x <> y & 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;
A4:         still_not-bound_in s = still_not-bound_in l by A2,QC_LANG3:8
           .= variables_in(l, bound_QC-variables) by QC_LANG3:6
           .={l.k : 1<=k & k<=len l & l.k in bound_QC-variables} by QC_LANG3:
def 2;

  A5:    s.y = (the_pred_symbol_of s)!Subst(l,a.0 .-->y) by A2,CQC_LANG:29;
         set ll = Subst(l,a.0 .-->y);
  A6:   s.y is atomic & the_arguments_of s.y = ll
           proof
             consider k being Nat, p being (QC-pred_symbol of k),
               l2 being QC-variable_list of k such that
        A7:    s = p!l2 by A2,QC_LANG1:def 17;
                 l2 = l by A2,A7,QC_LANG1:def 22;
            then len l = k by QC_LANG1:def 8;
               then len (Subst(l,a.0 .-->y)) = k by CQC_LANG:def 3;
               then reconsider l3 = Subst(l,a.0 .-->y)
 as QC-variable_list of k by QC_LANG1:def 8;
        A8:    s.y = p!l3 by A2,A5,A7,QC_LANG1:def 21;
               hence
                 s.y is atomic by QC_LANG1:def 17;
               hence ll = the_arguments_of s.y by A8,QC_LANG1:def 22;
           end;

         then A9: still_not-bound_in the_arguments_of s.y =
                 variables_in(ll, bound_QC-variables) by QC_LANG3:6
          .={ll.k : 1<=k & k<=
len ll & ll.k in bound_QC-variables} by QC_LANG3:def 2;

          x in {ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables}
implies
          x in {l.i : 1 <= i & i <= len l & l.i in bound_QC-variables}
        proof assume
            x in {ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables};
          then consider k such that
      A10:   x = ll.k & 1 <= k & k <= len ll & ll.k in bound_QC-variables;
      A11:   1 <= k & k <= len l by A10,CQC_LANG:def 3;
            then l.k <> a.0 by A3,A10,CQC_LANG:11;
            then x = l.k & l.k in bound_QC-variables by A10,A11,CQC_LANG:11;
          hence x in {l.i : 1 <= i & i <=
 len l & l.i in bound_QC-variables} by A11
;
        end;
      hence thesis by A3,A4,A6,A9,QC_LANG3:8;
      end;
    end;
    thus PP[VERUM] by CQC_LANG:28;
    thus s is negative & PP[the_argument_of s] implies PP[s]
    proof assume that
  A12: s is negative and
  A13: 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)
     and
  A14: x <> y & not x in still_not-bound_in s;
      not x in
 still_not-bound_in 'not'((the_argument_of s).y) by A12,A13,A14,QC_LANG3:10,11;
      hence not x in still_not-bound_in (s.y) by A12,CQC_LANG:31;
    end;
    thus (s is conjunctive & PP[the_left_argument_of s] &
                PP[the_right_argument_of s]) implies PP[s]
    proof assume that
  A15: s is conjunctive and
  A16: 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)
     and
  A17: 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)
     and
  A18: 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 A15,QC_LANG3:13;
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 A16,A17,A18,
XBOOLE_0:def 2;
         then not x in (still_not-bound_in ((the_left_argument_of s).y) '&'
                              ((the_right_argument_of s).y)) by QC_LANG3:14;
      hence not x in still_not-bound_in (s.y) by A15,CQC_LANG:33;
    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 & not x in still_not-bound_in s;
A22:      still_not-bound_in s =
        still_not-bound_in (the_scope_of s) \ {bound_in s} by A19,QC_LANG3:15;

    thus not x in still_not-bound_in (s.y)
    proof
 A23:   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 4
;
       then not x in still_not-bound_in All(bound_in s,(the_scope_of s).y)
                                                            by QC_LANG3:16;
   then y <> bound_in s implies not x in still_not-bound_in (s.y) by A19,
CQC_LANG:36;
         hence thesis by A19,A21,CQC_LANG:35;
       end;
         now assume x in {bound_in s};
then A24:      x = bound_in s by TARSKI:def 1;
           still_not-bound_in All(x,(the_scope_of s).y) =
           still_not-bound_in ((the_scope_of s).y) \ {x} by QC_LANG3:16;
         then 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 4;
         hence not x in still_not-bound_in (s.y)
           by A19,A21,A24,CQC_LANG:36,TARSKI:def 1;
       end;
       hence thesis by A21,A22,A23,XBOOLE_0:def 4;
     end;
    end;
  end;
      for s being Element of QC-WFF holds PP[s] from QC_Ind2 (A1);
   hence thesis;
 end;

theorem
  Th44: J,v |= VERUM
 proof
       (Valuations_in A --> TRUE).v = TRUE by FUNCOP_1:13;
     then (Valid(VERUM,J)).v = TRUE by Lm1;
     hence J,v |= VERUM by Def12;
 end;

theorem
  Th45: 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 MARGREL1:43;
      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 Th20
            .= 'not'((Valid(p '&' q, J).v) '&' (Valid('not'
(q '&' p), J).v)) by Th22
            .= 'not'((Valid(p '&' q, J).v) '&' 'not'
(Valid(q '&' p, J).v)) by Th20
;
      then (Valid(p '&' q, J).v) '&' 'not'(Valid(q '&' p, J).v) = TRUE by A1,
MARGREL1:41;
      then Valid(p '&' q, J).v=TRUE & 'not'
(Valid(q '&' p, J).v) = TRUE by MARGREL1:45;
      then Valid(p '&' q, J).v = TRUE & Valid(q '&' p, J).v = FALSE by MARGREL1
:41;
      then (Valid(p, J).v) '&' (Valid(q, J).v) = TRUE &
        (Valid(q, J).v) '&' (Valid(p, J).v) = FALSE by Th22;
      hence thesis by MARGREL1:38;
     end;
 end;

theorem
  Th46: J,v |= ('not' p => p) => p
 proof
    thus Valid(('not' p => p) => p, J).v = TRUE
     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 Th20
     .= 'not'((Valid('not'('not' p '&' 'not' p), J).v) '&' (Valid('not'
p, J).v)) by Th22;
      Valid('not'('not' p '&' 'not' p), J).v = 'not'(Valid('not' p '&' 'not'
p, J).v) by Th20
                 .= 'not'(Valid('not' p, J).v) by Th33
                 .= 'not' 'not'(Valid(p, J).v) by Th20
                 .= Valid(p, J).v by MARGREL1:40;
      hence
        Valid(('not' p => p) => p, J).v='not'((Valid(p, J).v) '&' 'not'
(Valid(p, J).v)) by A1,Th20
           .= TRUE by MARGREL1:47;
     end;
 end;

theorem
  Th47: J,v |= p => ('not' p => q)
 proof
   thus Valid(p => ('not' p => q), J).v = TRUE
     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 Th20
      .= 'not'((Valid(p,J).v) '&' (Valid('not'('not'('not' p '&' 'not'
q)), J).v)) by Th22;
           Valid('not'('not'('not' p '&' 'not' q)), J).v =
         'not'(Valid('not'('not'
p '&' 'not' q), J).v) by Th20
              .= 'not' 'not'(Valid('not' p '&' 'not' q, J).v) by Th20
              .= (Valid('not' p '&' 'not' q, J).v) by MARGREL1:40
              .= (Valid('not' p, J).v) '&' (Valid('not' q, J).v) by Th22
              .= 'not'(Valid(p, J).v) '&' (Valid('not' q, J).v) by Th20
              .= 'not'(Valid(p, J).v) '&' 'not'(Valid(q, J).v) by Th20;
      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:52
        .= 'not'(FALSE '&' 'not'(Valid(q, J).v)) by MARGREL1:46;
          FALSE '&' 'not'(Valid(q, J).v) = FALSE by MARGREL1:49;
        hence Valid(p => ('not' p => q), J).v = TRUE by A2,MARGREL1:41;
     end;
 end;

theorem
  Th48: J,v |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t))
 proof
    thus Valid((p => q) => ('not'(q '&' t) => 'not'(p '&' t)), J).v = TRUE
     proof
  A1:  p => q = 'not'(p '&' 'not' q) by QC_LANG2:def 2;
        'not'(q '&' t) => 'not'(p '&' t) = 'not'('not'(q '&' t) '&'
      'not' 'not' (p '&' t)) by QC_LANG2:def 2;
  then A2: 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 A1,QC_LANG2:def 2
       .= 'not'(Valid('not'(p '&' 'not' q) '&' 'not'('not'('not'(q '&' t) '&'
'not' 'not'(p '&' t))), J).v)
                                                                    by Th20
       .= 'not'((Valid('not'(p '&' 'not' q), J).v) '&'
              (Valid('not'('not'('not'(q '&' t) '&' 'not' 'not'
(p '&' t))), J).v)) by Th22;
  A3:  Valid('not'(p '&' 'not' q), J).v = 'not'(Valid(p '&' 'not' q, J).v)
   by Th20
           .= 'not'((Valid(p, J).v) '&' (Valid('not' q, J).v)) by Th22
           .= 'not'((Valid(p, J).v) '&'('not'(Valid(q, J).v))) by Th20;
         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 Th20
           .= 'not' 'not'(Valid('not'(q '&' t) '&' 'not' 'not'
(p '&' t), J).v) by Th20
           .= Valid('not'(q '&' t) '&' 'not' 'not'(p '&' t), J).v
           by MARGREL1:40
           .= (Valid('not'(q '&' t),J).v) '&' (Valid('not' 'not'
(p '&' t), J).v) by Th22
           .= 'not'(Valid(q '&' t,J).v) '&' (Valid('not' 'not'
(p '&' t), J).v) by Th20
           .= 'not'(Valid(q '&' t,J).v) '&'('not'(Valid('not'
(p '&' t), J).v)) by Th20
           .= 'not'(Valid(q '&' t,J).v) '&'('not' 'not'
(Valid(p '&' t, J).v)) by Th20
           .= 'not'(Valid(q '&' t,J).v) '&'(Valid(p '&' t, J).v) by MARGREL1:40
           .= 'not'((Valid(q,J).v) '&' (Valid(t,J).v)) '&'
                                     (Valid(p '&' t, J).v) by Th22
           .= 'not'((Valid(q,J).v) '&' (Valid(t,J).v)) '&'
                                ((Valid(p,J).v) '&' (Valid(t,J).v)) by Th22;
      hence Valid((p => q) => ('not'(q '&' t) => 'not'
(p '&' t)), J).v =TRUE by A2,A3,Lm2;
     end;
 end;

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

theorem
  Th50: 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 MARGREL1:43;
      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 Th20
            .= 'not'((Valid(All(x,p), J).v) '&' (Valid('not' p, J).v)) by Th22
            .= 'not'((Valid(All(x,p), J).v) '&' 'not'
(Valid(p, J).v)) by Th20;
      then (Valid(All(x,p), J).v) '&' 'not'(Valid(p, J).v) = TRUE by A1,
MARGREL1:41;
then A2:  Valid(All(x,p), J).v=TRUE & 'not'
(Valid(p, J).v) = TRUE by MARGREL1:45;
 then A3:  Valid(All(x,p), J).v = TRUE & Valid(p, J).v = FALSE by MARGREL1:41;
          FOR_ALL(x, Valid(p,J)).v = TRUE by A2,Lm1;
        hence thesis by A3,Th37,MARGREL1:38;
     end;
 end;


theorem
    J |= VERUM
 proof let v;
   thus thesis by Th44;
 end;

theorem
    J |= p '&' q => q '&' p
 proof let v;
   thus thesis by Th45;
 end;

theorem
    J |= ('not' p => p) => p
 proof let v;
   thus thesis by Th46;
 end;

theorem
    J |= p => ('not' p => q)
 proof let v;
   thus thesis by Th47;
 end;

theorem
    J |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t))
 proof let v;
   thus thesis by Th48;
 end;

theorem
    J |= p & J |= (p => q) implies J |= q
 proof
   assume that
 A1: J |= p and A2: J |= p => q;
       now let v;
         J,v |= p & J,v |= p => q by A1,A2,Def13;
       hence J,v |= q by Th36;
     end;
     hence J |= q by Def13;
 end;

theorem
    J |= All(x,p) => p
 proof let v;
   thus thesis by Th50;
 end;

theorem
    (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,Th40;
                 J,w |= p => q by A1;
               hence J,w |= q by A4,Th36;
         end;
        hence J,u |= All(x,q) by Th41;
      end;
    hence J,u |= p => All(x,q) by Th36;
 end;

theorem
    for s being QC-formula 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;
   assume that
 A1: p = s.x & q = s.y and
 A2: not x in still_not-bound_in s and
 A3: J |= p;
     now assume
 A4: x <> y;
 A5: now let u;
       consider w being Element of Valuations_in A such that
   A6:  (for z being bound_QC-variable st z <> x holds w.z = u.z) &
                                                  w.x = u.y from Lambda_Val;
         w.x = w.y by A6;
   then A7: Valid(p,J).w = Valid(q,J).w by A1,Th42;
         J,w |= p by A3,Def13;
   then A8: Valid(p,J).w = TRUE by Def12;
         not x in still_not-bound_in q by A1,A2,A4,Th43;
       hence Valid(q,J).u = TRUE by A6,A7,A8,Th39;
     end;
       now let v;
         Valid(q,J).v = TRUE by A5;
       hence J,v |= q by Def12;
     end;
     hence J |= q by Def13;
   end;
   hence thesis by A1,A3;
 end;

Back to top