CQC_LANG

:: A Classical First Order Language
::  by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SUBSET_1, NUMBERS, QC_LANG1, FINSEQ_1, PARTFUN1, XXREAL_0,
      FUNCT_1, RELAT_1, TARSKI, FUNCOP_1, QC_LANG3, XBOOLE_0, ZF_MODEL,
      FINSEQ_2, ZF_LANG, CARD_1, REALSET1, XBOOLEAN, BVFUNC_2, MARGREL1,
      CLASSES2, CQC_LANG, ZFMISC_1, NAT_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCOP_1, FUNCT_4,
      FINSEQ_1, FINSEQ_2, QC_LANG1, QC_LANG2, QC_LANG3, XXREAL_0, NAT_1,
      ZFMISC_1;
 constructors ENUMSET1, PARTFUN1, BINOP_1, FUNCOP_1, FUNCT_4, XXREAL_0,
      MEMBERED, QC_LANG2, QC_LANG3, FINSEQ_2, RELSET_1, NUMBERS;
 registrations XBOOLE_0, RELSET_1, FUNCOP_1, MEMBERED, QC_LANG1, XXREAL_0,
      FINSEQ_2;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions TARSKI, RELAT_1;
 equalities FUNCOP_1, FINSEQ_2;
 theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FINSEQ_1, PARTFUN1, FUNCOP_1,
      QC_LANG1, QC_LANG2, QC_LANG3, FINSEQ_2, RELSET_1, FINSEQ_3, RELAT_1,
      CARD_1, XBOOLE_0, XTUPLE_0;
 schemes FINSEQ_1, QC_LANG1, QC_LANG3;

begin

reserve A for QC-alphabet;
reserve i,j,k for Nat;

Lm1: for x being bound_QC-variable of A holds not x in fixed_QC-variables(A)
proof
  let x be bound_QC-variable of A;
  x in bound_QC-variables(A);
  then x in [: {4},QC-symbols(A) :] by QC_LANG1:def 4;
  then consider x1,x2 being object such that
A1: x1 in {4} and
  x2 in QC-symbols(A) and
A2: x = [x1,x2] by ZFMISC_1:def 2;
A3: x1 = 4 by A1,TARSKI:def 1;
  assume x in fixed_QC-variables(A);
  then x in [: {5},QC-symbols(A) :] by QC_LANG1:def 5;
  then consider c1,c2 being object such that
A4: c1 in {5} and
  c2 in QC-symbols(A) and
A5: x = [c1,c2] by ZFMISC_1:def 2;
  c1 = 5 by A4,TARSKI:def 1;
  hence contradiction by A2,A5,A3,XTUPLE_0:1;
end;

theorem Th1:
  for x being set holds x in QC-variables(A) iff x in
  fixed_QC-variables(A) or x in free_QC-variables(A) or
  x in bound_QC-variables(A)
proof
  let x be set;
  thus x in QC-variables(A) implies x in fixed_QC-variables(A) or x in
  free_QC-variables(A) or x in bound_QC-variables(A)
  proof
    assume x in QC-variables(A);
    then x in [: {6}, NAT :] \/ [: {4,5}, QC-symbols(A) :] by QC_LANG1:def 3;
    then x in [: {6}, NAT :] or x in [: {4,5}, QC-symbols(A) :]
      by XBOOLE_0:def 3;
    then consider x1,x2 being object such that
A1: (x1 in {6} & x2 in NAT & x = [x1,x2]) or
    (x1 in {4,5} & x2 in QC-symbols(A) & x = [x1,x2]) by ZFMISC_1:def 2;
    (x1 in {6} & x2 in NAT & x = [x1,x2]) or
    ((x1 = 4 or x1 = 5) & x2 in QC-symbols(A) & x = [x1,x2])
    by A1,TARSKI:def 2;
   then ((x1 in {4} & x2 in QC-symbols(A)) or (x1 in {5} & x2 in QC-symbols(A))
         or (x1 in {6} & x2 in NAT)) & x = [x1,x2] by TARSKI:def 1;
    then x in [:{4},QC-symbols(A):] or x in [:{5}, QC-symbols(A):] or
         x in [:{6},NAT:] by ZFMISC_1:def 2;
    hence thesis by QC_LANG1:def 4,def 5,def 6;
  end;
  thus thesis;
end;

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

reserve f for Substitution of A;

definition
  let A;
  let l be FinSequence of QC-variables(A);
  let f;
  func Subst(l,f) -> FinSequence of QC-variables(A) means
  :Def1:
  len it = len l &
for k st 1 <= k & k <= len l holds (l.k in dom f implies it.k = f.(l.k)) & (not
  l.k in dom f implies it.k = l.k);
  existence
  proof
    defpred P[set,object] means
     (l.$1 in dom f implies $2 = f.(l.$1)) & (not l.$1
    in dom f implies $2 = l.$1);
A1: for k be Nat st k in Seg len l ex y being object st P[k,y]
    proof
      let k be Nat;
      assume k in Seg len l;
      l.k in dom f implies thesis;
      hence thesis;
    end;
    consider s being FinSequence such that
A2: dom s = Seg len l and
A3: for k be Nat st k in Seg len l holds P[k,s.k]
      from FINSEQ_1:sch 1(
    A1);
    rng s c= QC-variables(A)
    proof
      let y be object;
      assume y in rng s;
      then consider x being object such that
A4:   x in dom s and
A5:   s.x = y by FUNCT_1:def 3;
      reconsider x as Nat by A4;
A6:   now
        per cases;
        case
          l.x in dom f;
          hence s.x = f.(l.x) & f.(l.x) in QC-variables(A)
           by A2,A3,A4,PARTFUN1:4;
        end;
        case
          not l.x in dom f;
          hence s.x = l.x by A2,A3,A4;
        end;
      end;
      dom l = Seg len l by FINSEQ_1:def 3;
      hence thesis by A2,A4,A5,A6,FINSEQ_2:11;
    end;
    then reconsider s as FinSequence of QC-variables(A) by FINSEQ_1:def 4;
    take s;
    thus len s = len l by A2,FINSEQ_1:def 3;
    let k;
    assume 1 <= k & k <= len l;
    then k in dom l by FINSEQ_3:25;
    then k in Seg len l by FINSEQ_1:def 3;
    hence thesis by A3;
  end;
  uniqueness
  proof
    let l1,l2 be FinSequence of QC-variables(A) such that
A7: len l1 = len l and
A8: for k st 1 <= k & k <= len l holds (l.k in dom f implies l1.k = f
    .(l.k)) & (not l.k in dom f implies l1.k = l.k) and
A9: len l2 = len l and
A10: for k st 1 <= k & k <= len l holds (l.k in dom f implies l2.k = f
    .(l.k)) & (not l.k in dom f implies l2.k = l.k);
    now
      let k be Nat;
      assume
A11:  1 <= k & k <= len l;
A12:  not l.k in dom f implies l1.k = l.k by A8,A11;
      l.k in dom f implies l1.k = f.(l.k) by A8,A11;
      hence l1.k = l2.k by A10,A11,A12;
    end;
    hence thesis by A7,A9,FINSEQ_1:14;
  end;
end;

registration
  let A,k;
  let l be QC-variable_list of k, A;
  let f;
  cluster Subst(l,f) -> k-element;
  coherence
  proof
    len Subst(l,f) = len l & len l = k by Def1,CARD_1:def 7;
    hence thesis by CARD_1:def 7;
  end;
end;

theorem Th2:
  for x being bound_QC-variable of A, a being free_QC-variable of A holds
   a .--> x is Substitution of A
proof
  let x be bound_QC-variable of A;
  let a be free_QC-variable of A;
  set f = a .--> x;
  rng f = {x} by FUNCOP_1:8;
  then
A1: rng f c= QC-variables(A) by ZFMISC_1:31;
  dom f c= free_QC-variables(A) by ZFMISC_1:31;
  hence thesis by A1,RELSET_1:4;
end;

definition
  let A;
  let a be free_QC-variable of A, x be bound_QC-variable of A;
  redefine func a .--> x -> Substitution of A;  :: redefines .--> (FUNCOP_1, definition)
  coherence by Th2;
end;

theorem Th3:
  for x being bound_QC-variable of A, a being free_QC-variable of A,
  l, ll being FinSequence of QC-variables(A)
  holds
  f = a .--> x & ll = Subst(l,f) & 1 <= k & k <= len l implies (l.
  k = a implies ll.k = x) & (l.k <> a implies ll.k = l.k)
proof
  let x be bound_QC-variable of A, a be free_QC-variable of A,
  l, ll be FinSequence of QC-variables(A);
  set f9 = a .--> x;
  assume
A1: f = a .--> x & ll = Subst(l,f) & 1 <= k & k <= len l;
  thus l.k = a implies ll.k = x
  proof
A2: f9.a = x by FUNCOP_1:72;
    assume
A3: l.k = a;
    then l.k in { a } by TARSKI:def 1;
    then l.k in dom(f9);
    hence thesis by A1,A3,A2,Def1;
  end;
  assume l.k <> a;
  then not l.k in { a } by TARSKI:def 1;
  then not l.k in dom(f9);
  hence thesis by A1,Def1;
end;

definition
  let A;
  func CQC-WFF(A) -> Subset of QC-WFF(A) equals
  {s where s is QC-formula of A: Fixed s = {} & Free s = {} };
  coherence
  proof
    set F = {s where s is QC-formula of A: Fixed s = {} & Free s = {} };
    F c= QC-WFF(A)
    proof
      let x be object;
      assume x in F;
      then ex s being QC-formula of A st s = x & Fixed s = {} & Free s = {};
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  let A;
  cluster CQC-WFF(A) -> non empty;
  coherence
  proof
    Fixed VERUM(A) = {} & Free VERUM(A) = {} by QC_LANG3:53,63;
    then VERUM(A) in
    {s where s is QC-formula of A: Fixed s = {} & Free s = {} };
    hence thesis;
  end;
end;

theorem Th4:
  for p being Element of QC-WFF(A) holds
  p is Element of CQC-WFF(A) iff Fixed p = {} & Free p = {}
proof
  let p be Element of QC-WFF(A);
  thus p is Element of CQC-WFF(A) implies Fixed p = {} & Free p = {}
  proof
    assume p is Element of CQC-WFF(A);
    then p in CQC-WFF(A);
    then ex s being QC-formula of A st s = p & Fixed s = {} & Free s = {};
    hence thesis;
  end;
  assume Fixed p = {} & Free p = {};
  then p in CQC-WFF(A);
  hence thesis;
end;

registration
  let A;
  let k be Nat;
  cluster bound_QC-variables(A)-valued for QC-variable_list of k, A;
  existence
  proof
    set null = 0;
    reconsider null as QC-symbol of A by QC_LANG1:3;
    set l = k |-> x.null;
    rng l c= QC-variables(A)
    proof
      let y be object;
      assume y in rng l;
      then consider x being object such that
A2:   x in dom l and
A3:   l.x = y by FUNCT_1:def 3;
      y = x.null by A2,A3,FINSEQ_2:57;
      hence thesis;
    end;
    then reconsider l as QC-variable_list of k, A by FINSEQ_1:def 4;
    take l;
    let x be object;
    assume x in rng l;
    then consider i being object such that
A4: i in dom l and
A5: x = l.i by FUNCT_1:def 3;
    reconsider i as Nat by A4;
    l.i = x.null by A4,FINSEQ_2:57;
    hence thesis by A5;
  end;
end;

definition
  let A; let k be Nat;
  mode CQC-variable_list of k,
   A is bound_QC-variables(A)-valued QC-variable_list of k,A;
end;

theorem Th5:
  for l being QC-variable_list of k, A holds l is CQC-variable_list
of k,A iff { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A) }
           = {} & { l.j
  : 1 <= j & j <= len l & l.j in fixed_QC-variables(A) } = {}
proof
  let l be QC-variable_list of k, A;
  set FR = { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A) };
  set FI = { l.j : 1 <= j & j <= len l & l.j in fixed_QC-variables(A) };
  thus l is CQC-variable_list of k, A implies FR = {} & FI = {}
  proof
    assume l is CQC-variable_list of k, A;
    then reconsider l as CQC-variable_list of k, A;
    now
      set x =the  Element of FR;
      assume FR <> {};
      then x in FR;
      then consider i such that
      x = l.i and
A1:   1 <= i & i <= len l and
A2:   l.i in free_QC-variables(A);
      i in dom l by A1,FINSEQ_3:25;
      then rng l c= bound_QC-variables(A) & l.i in rng l by FUNCT_1:def 3
,RELAT_1:def 19;
      hence contradiction by A2,QC_LANG3:34;
    end;
    hence FR = {};
    now
      set x =the  Element of FI;
      assume FI <> {};
      then x in FI;
      then consider i such that
      x = l.i and
A3:   1 <= i & i <= len l and
A4:   l.i in fixed_QC-variables(A);
      i in dom l by A3,FINSEQ_3:25;
      then rng l c= bound_QC-variables(A) & l.i in rng l by FUNCT_1:def 3
,RELAT_1:def 19;
      hence contradiction by A4,QC_LANG3:33;
    end;
    hence thesis;
  end;
  assume that
A5: FR = {} and
A6: FI = {};
  l is bound_QC-variables(A)-valued
  proof
    let x be object;
A7: rng l c= QC-variables(A) by FINSEQ_1:def 4;
    assume x in rng l;
    then consider i being object such that
A8: i in dom l and
A9: l.i = x by FUNCT_1:def 3;
    reconsider i as Nat by A8;
A10: 1 <= i & i <= len l by A8,FINSEQ_3:25;
A11: now
      assume x in fixed_QC-variables(A);
      then x in FI by A9,A10;
      hence contradiction by A6;
    end;
A12: now
      assume x in free_QC-variables(A);
      then x in FR by A9,A10;
      hence contradiction by A5;
    end;
    l.i in rng l by A8,FUNCT_1:def 3;
    hence thesis by A9,A7,A11,A12,Th1;
  end;
  hence thesis;
end;


theorem Th6:
  VERUM(A) is Element of CQC-WFF(A)
proof
    Fixed VERUM(A) = {} & Free VERUM(A) = {} by QC_LANG3:53,63;
    hence thesis by Th4;
end;

theorem Th7:
  for P being QC-pred_symbol of k,A for l being QC-variable_list of
  k,A holds P!l is Element of CQC-WFF(A) iff
  { l.i : 1 <= i & i <= len l & l.i in
  free_QC-variables(A) } = {} & { l.j : 1 <= j & j <= len l & l.j in
  fixed_QC-variables(A) } = {}
proof
  let P be QC-pred_symbol of k,A;
  let l be QC-variable_list of k, A;
A1: Free(P!l) = { l.j : 1 <= j & j <= len l & l.j in free_QC-variables(A) } by
QC_LANG3:54;
  Fixed(P!l) = { l.i : 1 <= i & i <= len l & l.i in fixed_QC-variables(A) }
  by QC_LANG3:64;
  hence thesis by A1,Th4;
end;

definition
  let k,A;
  let P be QC-pred_symbol of k,A;
  let l be CQC-variable_list of k,A;
  redefine func P!l -> Element of CQC-WFF(A);  :: redefines ! (QC_LANG1, definition)
  coherence
  proof
A1: { l.j : 1 <= j & j <= len l & l.j in fixed_QC-variables(A) } = {} by Th5;
    { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A) } = {} by Th5;
    hence thesis by A1,Th7;
  end;
end;

theorem Th8:
  for p being Element of QC-WFF(A) holds
  'not' p is Element of CQC-WFF(A) iff p is Element of CQC-WFF(A)
proof
  let p be Element of QC-WFF(A);
  thus 'not' p is Element of CQC-WFF(A) implies p is Element of CQC-WFF(A)
  proof
    assume
A1: 'not' p is Element of CQC-WFF(A);
    then Free 'not' p = {} by Th4;
    then
A2: Free p = {} by QC_LANG3:55;
    Fixed 'not' p = {} by A1,Th4;
    then Fixed p = {} by QC_LANG3:65;
    hence thesis by A2,Th4;
  end;
  assume p is Element of CQC-WFF(A);
  then reconsider r = p as Element of CQC-WFF(A);
  Fixed r = {} by Th4;
  then
A3: Fixed 'not' r = {} by QC_LANG3:65;
  Free r = {} by Th4;
  then Free 'not' r = {} by QC_LANG3:55;
  hence thesis by A3,Th4;
end;

theorem Th9:
  for p,q being Element of QC-WFF(A) holds
  p '&' q is Element of CQC-WFF(A) iff p is Element of CQC-WFF(A) & q is
  Element of CQC-WFF(A)
proof
  let p,q being Element of QC-WFF(A);
  thus p '&' q is Element of CQC-WFF(A) implies
  p is Element of CQC-WFF(A) & q is
  Element of CQC-WFF(A)
  proof
    assume
A1: p '&' q is Element of CQC-WFF(A);
    then Fixed(p '&' q) = {} by Th4;
    then
A2: Fixed p \/ Fixed q = {} by QC_LANG3:67;
    then
A3: Fixed p = {};
    Free(p '&' q) = {} by A1,Th4;
    then
A4: Free p \/ Free q = {} by QC_LANG3:57;
    then Free p = {};
    hence thesis by A4,A2,A3,Th4;
  end;
  assume p is Element of CQC-WFF(A) & q is Element of CQC-WFF(A);
  then reconsider r = p, s = q as Element of CQC-WFF(A);
  Fixed r = {} by Th4;
  then Fixed r \/ Fixed s = {} by Th4;
  then
A5: Fixed(r '&' s) = {} by QC_LANG3:67;
  Free r = {} by Th4;
  then Free r \/ Free s = {} by Th4;
  then Free (r '&' s) = {} by QC_LANG3:57;
  hence thesis by A5,Th4;
end;

definition
  let A;
  redefine func VERUM(A) -> Element of CQC-WFF(A);  :: redefines VERUM (QC_LANG1, definition)
  coherence by Th6;
  let r be Element of CQC-WFF(A);
  redefine func 'not' r -> Element of CQC-WFF(A);  :: redefines 'not' (QC_LANG1, definition)
  coherence by Th8;
  let s be Element of CQC-WFF(A);
  redefine func r '&' s -> Element of CQC-WFF(A);  :: redefines '&' (QC_LANG1, definition)
  coherence by Th9;
end;

theorem Th10:
  for r,s being Element of CQC-WFF(A) holds
  r => s is Element of CQC-WFF(A)
proof
  let r,s be Element of CQC-WFF(A);
  r => s = 'not' (r '&' 'not' s) by QC_LANG2:def 2;
  hence thesis;
end;

theorem Th11:
  for r,s being Element of CQC-WFF(A) holds
  r 'or' s is Element of CQC-WFF(A)
proof
  let r,s be Element of CQC-WFF(A);
  r 'or' s = 'not' ('not' r '&' 'not' s) by QC_LANG2:def 3;
  hence thesis;
end;

theorem Th12:
  for r,s being Element of CQC-WFF(A) holds
  r <=> s is Element of CQC-WFF(A)
proof
  let r,s be Element of CQC-WFF(A);
  r <=> s = (r => s) '&' (s => r) by QC_LANG2:def 4
    .= ( 'not' (r '&' 'not' s) ) '&' (s => r) by QC_LANG2:def 2
    .= ( 'not' (r '&' 'not' s) ) '&' ( 'not' (s '&' 'not' r) ) by
QC_LANG2:def 2;
  hence thesis;
end;

definition
  let A;
  let r,s be Element of CQC-WFF(A);
  redefine func r => s -> Element of CQC-WFF(A);  :: redefines => (QC_LANG2, definition)
  coherence by Th10;
  redefine func r 'or' s -> Element of CQC-WFF(A);  :: redefines 'or' (QC_LANG2, definition)
  coherence by Th11;
  redefine func r <=> s -> Element of CQC-WFF(A);  :: redefines <=> (QC_LANG2, definition)
  coherence by Th12;
end;

theorem Th13:
  for x being bound_QC-variable of A, p being Element of QC-WFF(A) holds
  All(x,p) is Element of CQC-WFF(A) iff p is Element of CQC-WFF(A)
proof
  let x be bound_QC-variable of A, p be Element of QC-WFF(A);
  thus All(x,p) is Element of CQC-WFF(A) implies p is Element of CQC-WFF(A)
  proof
    assume
A1: All(x,p) is Element of CQC-WFF(A);
    then Fixed All(x,p) = {} by Th4;
    then
A2: Fixed p = {} by QC_LANG3:68;
    Free All(x,p) = {} by A1,Th4;
    then Free p = {} by QC_LANG3:58;
    hence thesis by A2,Th4;
  end;
  assume
A3: p is Element of CQC-WFF(A);
  then Fixed p = {} by Th4;
  then
A4: Fixed All(x,p) = {} by QC_LANG3:68;
  Free p = {} by A3,Th4;
  then Free All(x,p) = {} by QC_LANG3:58;
  hence thesis by A4,Th4;
end;

definition
  let A;
  let x be bound_QC-variable of A,r be Element of CQC-WFF(A);
  redefine func All(x,r) -> Element of CQC-WFF(A);  :: redefines All (QC_LANG1, definition)
  coherence by Th13;
end;

theorem Th14:
  for x being bound_QC-variable of A,r being Element of CQC-WFF(A) holds
  Ex(x,r) is Element of CQC-WFF(A)
proof
  let x be bound_QC-variable of A,r be Element of CQC-WFF(A);
  Ex(x,r) = 'not' All(x,'not' r) by QC_LANG2:def 5;
  hence thesis;
end;

definition
  let A;
  let x be bound_QC-variable of A,r be Element of CQC-WFF(A);
  redefine func Ex(x,r) -> Element of CQC-WFF(A);  :: redefines Ex (QC_LANG2, definition)
  coherence by Th14;
end;

scheme
  CQCInd { A() -> QC-alphabet, P[set] }
:
for r being Element of CQC-WFF(A()) holds P[r]
provided
A1: for r,s being Element of CQC-WFF(A())
for x being bound_QC-variable of A() for k
for l being CQC-variable_list of k, A() for P being
QC-pred_symbol of k,A() holds P[VERUM(A())] & P[P!l] &
 (P[r] implies P['not' r]) & (P[r]
& P[s] implies P[r '&' s]) & (P[r] implies P[All(x, r)])
proof
  defpred Prop[Element of QC-WFF(A())] means $1 is Element of CQC-WFF(A())
                                           implies P[ $1 ];
A2: for p being Element of QC-WFF(A()) st Prop[p] holds Prop['not' p]
  proof
    let p be Element of QC-WFF(A());
    assume
A3: Prop[p];
    assume 'not' p is Element of CQC-WFF(A());
    then p is Element of CQC-WFF(A()) by Th8;
    hence thesis by A1,A3;
  end;
A4: for p,q being Element of QC-WFF(A()) st Prop[p]
    & Prop[q] holds Prop[p '&' q ]
  proof
    let p,q be Element of QC-WFF(A());
    assume
A5: ( Prop[p])& Prop[q];
    assume p '&' q is Element of CQC-WFF(A());
    then p is Element of CQC-WFF(A()) & q is Element of CQC-WFF(A()) by Th9;
    hence thesis by A1,A5;
  end;
A6: for k being Nat, P being (QC-pred_symbol of k,A()), l being
  QC-variable_list of k, A() holds Prop[P!l]
  proof
    let k be Nat, P be (QC-pred_symbol of k,A()),
    l be QC-variable_list of k, A();
    assume
A7: P!l is Element of CQC-WFF(A());
    reconsider k as Nat;
    reconsider l as QC-variable_list of k, A();
A8: { l.j :1 <= j & j <= len l & l.j in fixed_QC-variables(A()) } = {}
    by Th7,A7;
    { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A()) }
      = {} by A7,Th7;
    then l is CQC-variable_list of k, A() by A8,Th5;
    hence thesis by A1;
  end;
A9: for x being bound_QC-variable of A(), p being Element of QC-WFF(A())
st Prop[p] holds Prop[All(x, p)]
  proof
    let x be bound_QC-variable of A(), p be Element of QC-WFF(A());
    assume
A10: Prop[p];
    assume All(x,p) is Element of CQC-WFF(A());
    then p is Element of CQC-WFF(A()) by Th13;
    hence thesis by A1,A10;
  end;
A11: Prop[VERUM(A())] by A1;
  for p being Element of QC-WFF(A()) holds Prop[p]
  from QC_LANG1:sch 1 (A6,A11,A2,A4,A9);
  hence thesis;
end;

scheme
  CQCFuncEx { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), A(set,set,set) -> (Element of D()),
N(set) -> (Element of D()), C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()} : ex F being Function of CQC-WFF(Al()),
D() st F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() 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)
proof
  deffunc q((Element of QC-WFF(Al())), Element of D()) = Q(bound_in $1,$2);
  deffunc a(Element of QC-WFF(Al())) = A(the_arity_of the_pred_symbol_of $1,
  the_pred_symbol_of $1,the_arguments_of $1);
  consider F being Function of QC-WFF(Al()), D() such that
A1: F.VERUM(Al()) = V() & for p being Element of QC-WFF(Al())
holds (p is atomic implies F.p = a(p)) &
(p is negative implies F.p = N(F.the_argument_of p)) &
(p is conjunctive implies F.p = C(F.the_left_argument_of p, F.
the_right_argument_of p)) & (p is universal implies
F.p = q(p, F.the_scope_of p)) from QC_LANG1:sch 3;
  reconsider G = F|CQC-WFF(Al()) as Function of CQC-WFF(Al()),D()
  by FUNCT_2:32;
  take G;
  thus G.VERUM(Al()) = V() by A1,FUNCT_1:49;
  let r,s being Element of CQC-WFF(Al());
  let x being bound_QC-variable of Al();
  let k;
  let l be CQC-variable_list of k, Al();
  let P be QC-pred_symbol of k,Al();
A2: the_arity_of P = k by QC_LANG1:11;
A3: P!l is atomic by QC_LANG1:def 18;
  then
A4: the_arguments_of (P!l) = l & the_pred_symbol_of (P!l) = P by
QC_LANG1:def 22,def 23;
  thus G.(P!l) = F.(P!l) by FUNCT_1:49
    .= A(k,P,l) by A1,A3,A4,A2;
  set r9 = G.r, s9 = G.s;
A5: r9 = F.r by FUNCT_1:49;
A6: r '&' s is conjunctive by QC_LANG1:def 20;
  then
A7: the_left_argument_of(r '&' s) = r & the_right_argument_of(r '&' s) = s
  by QC_LANG1:def 25,def 26;
A8: 'not' r is negative by QC_LANG1:def 19;
  then
A9: the_argument_of 'not' r = r by QC_LANG1:def 24;
  thus G.('not' r) = F.('not' r) by FUNCT_1:49
    .= N(r9) by A1,A5,A8,A9;
A10: s9 = F.s by FUNCT_1:49;
  thus G.(r '&' s) = F.(r '&' s) by FUNCT_1:49
    .= C(r9,s9) by A1,A5,A10,A6,A7;
A11: All(x,r) is universal by QC_LANG1:def 21;
  then
A12: bound_in All(x,r) = x & the_scope_of All(x,r)=r by QC_LANG1:def 27,def 28;
  thus G.All(x,r) = F.All(x,r) by FUNCT_1:49
    .= Q(x,r9) by A1,A5,A11,A12;
end;

scheme
  CQCFuncUniq { Al() -> QC-alphabet, D() -> non empty set,
  F1() -> (Function of CQC-WFF(Al()), D()),
  F2()-> (Function of CQC-WFF(Al()), D()),
  V() -> (Element of D()), A(set,set,set) -> (Element of D()),
  N(set) -> (Element of D()), C(set,set) -> (Element of D()),
  Q(set,set) -> Element of D()} : F1() = F2()
provided
A1: F1().VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F1().(P!l) = A(k,P,l) &
F1().('not' r) = N(F1().r) & F1().(r '&' s) = C(F1().r,F1().s) &
F1().All(x,r) = Q(x,F1().r) and
A2: F2().VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F2().(P!l) =
A(k,P,l) & F2().('not' r) =
N(F2().r) & F2().(r '&' s) = C(F2().r,F2().s) & F2().All(x,r) = Q(x,F2().r)
proof
  defpred P[set] means F1().$1 = F2().$1;
A3:for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for P being
QC-pred_symbol of k,Al() holds P[VERUM(Al())] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]) &
(P[r] implies P[All(x, r)])
  proof
  let r,s be Element of CQC-WFF(Al());
  let x be bound_QC-variable of Al();
  let k;
    let l be CQC-variable_list of k, Al();
    let P be QC-pred_symbol of k,Al();
    thus F1().VERUM(Al()) = F2().VERUM(Al()) by A1,A2;
    F1().(P!l) = A(k,P,l) by A1;
    hence F1().(P!l) = F2().(P!l) by A2;
    F1().('not' r) = N(F1().r) by A1;
    hence F1().r = F2().r implies F1().('not' r) = F2().('not' r) by A2;
    F1().(r '&' s) = C(F1().r,F1().s) by A1;
    hence F1().r = F2().r & F1().s = F2().s implies F1().(r '&' s) = F2().(r
    '&' s) by A2;
    F1().All(x,r) = Q(x,F1().r) by A1;
    hence thesis by A2;
  end;
  for r being Element of CQC-WFF(Al()) holds P[r] from CQCInd(A3);
  hence thesis by FUNCT_2:63;
end;

scheme
  CQCDefcorrectness { Al() -> QC-alphabet, D() -> non empty set,
    p() -> (Element of CQC-WFF(Al())), V() -> (Element of D()),
    A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
    C(set,set) -> (Element of D()), Q(set,set) -> Element of D()}
:
  (ex d being Element of D() st ex F being Function of CQC-WFF(Al()),
   D() st d = F.p() & F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
   for l being CQC-variable_list of k, Al() for P being
   QC-pred_symbol of k,Al() 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(Al()),
   D() st d1 = F.p() & F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
   for l being CQC-variable_list of k, Al()
   for P being QC-pred_symbol of k,Al()
   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(Al()), D() st d2 = F.p() &
   F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
   for P being QC-pred_symbol of k,Al() 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
proof
  thus ex d being Element of D() st ex F being Function of CQC-WFF(Al()), D()
  st d = F.p() & F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
  for l being CQC-variable_list of k, Al() for P being QC-pred_symbol of k,Al()
  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)
  proof
    consider F being Function of CQC-WFF(Al()), D() such that
A1: F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() 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)
from CQCFuncEx;
    take F.p(),F;
    thus thesis by A1;
  end;
  let d1,d2 be Element of D();
  given F1 being Function of CQC-WFF(Al()), D() such that
A2: d1 = F1.p() and
A3: F1.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F1.(P!l) = A(k,P,l) &
F1.('not' r) = N(F1.r) & F1.(r '&' s) = C(F1.r,F1.s) & F1.All(x,r) = Q(x,F1.r);
  given F2 being Function of CQC-WFF(Al()), D() such that
A4: d2 = F2.p() and
A5: F2.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F2.(P!l) = A(k,P,l) &
F2.('not' r) = N(F2.r) & F2.(r '&' s) = C(F2.r,F2.s) &
F2.All(x,r) = Q(x,F2.r);
  F1 = F2 from CQCFuncUniq(A3,A5);
  hence thesis by A2,A4;
end;

scheme
  CQCDefVERUM { Al() -> QC-alphabet, D() -> non empty set,
F(set) -> (Element of D()), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
C(set,set) -> (Element of D()), Q(set,set) -> Element of D()} :
F(VERUM(Al())) = V()
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds
d = F (p) iff ex F being Function of CQC-WFF(Al()), D() st
d = F.p & F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() 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)
proof
  ex F being Function of CQC-WFF(Al()), D() st F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() 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)
from CQCFuncEx;
  hence thesis by A1;
end;

scheme
  CQCDefatomic { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), F(set) -> (Element of D()),
A(set,set,set) -> (Element of D()), k() -> Nat, P()
  -> (QC-pred_symbol of k(),Al()), l() -> (CQC-variable_list of k(), Al()),
  N(set) -> (Element of D()), C(set,set) -> (Element of D()),
  Q(set,set) -> Element of D()}
  : F(P()!l()) = A(k(),P(),l())
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds d = F
(p) iff ex F being Function of CQC-WFF(Al()), D()
st d = F.p & F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() 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)
proof
  consider F being Function of CQC-WFF(Al()), D() such that
A2: F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() 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) from CQCFuncEx;
  A(k(),P(),l()) = F.(P()!l()) by A2;
  hence thesis by A1,A2;
end;

scheme
  CQCDefnegative { Al() -> QC-alphabet, D() -> non empty set,
F(set) -> (Element of D()), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
r() -> (Element of CQC-WFF(Al())), C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()}
:
F('not' r()) = N(F(r()))
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds
d = F (p) iff ex F being Function of CQC-WFF(Al()), D() st
d = F.p & F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() 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)
proof
  consider G being Function of CQC-WFF(Al()), D() such that
A2: F(r()) = G.r() and
A3: G.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() holds G.(P!l) = A(k,P,l) &
G.('not' r) = N(G.r) &
G.(r '&' s) = C(G.r,G.s) & G.All(x,r) = Q(x,G.r) by A1;
  consider F being Function of CQC-WFF(Al()), D() such that
A4: F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() 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)
from CQCFuncEx;
A5: F.('not' r()) = N(F.r()) by A4;
  F = G from CQCFuncUniq(A4,A3);
  hence thesis by A1,A4,A5,A2;
end;

scheme
  QCDefconjunctive { Al() -> QC-alphabet, D() -> non empty set,
F(set) -> (Element of D()), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
C(set,set) -> (Element of D()), r() -> (Element of CQC-WFF(Al())),
s() -> (Element of CQC-WFF(Al())), Q(set,set) -> Element of D()}
:
F(r() '&' s()) = C(F(r()), F(s()))
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds d = F
(p) iff ex F being Function of CQC-WFF(Al()), D() st d = F.p &
F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() 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)
proof
  consider F2 being Function of CQC-WFF(Al()), D() such that
A2: F(s()) = F2.s() and
A3: F2.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F2.(P!l) = A(k,P,l) &
F2.('not' r) = N(F2.r)
  & F2.(r '&' s) = C(F2.r,F2.s) & F2.All(x,r) = Q(x,F2.r) by A1;
  consider F1 being Function of CQC-WFF(Al()), D() such that
A4: F(r()) = F1.r() and
A5: F1.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F1.(P!l) = A(k,P,l) &
F1.('not' r) = N(F1.r)
  & F1.(r '&' s) = C(F1.r,F1.s) & F1.All(x,r) = Q(x,F1.r) by A1;
  consider F being Function of CQC-WFF(Al()), D() such that
A6: F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() 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)
from CQCFuncEx;
A7: F.(r() '&' s()) = C(F.r(),F.s()) by A6;
A8: F = F2 from CQCFuncUniq(A6,A3);
  F = F1 from CQCFuncUniq(A6,A5);
  hence thesis by A1,A6,A7,A4,A2,A8;
end;

scheme
  QCDefuniversal { Al() -> QC-alphabet, D() -> non empty set,
F(set) -> (Element of D()), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
C(set,set) -> (Element of D()), Q(set,set) -> (Element of D()),
x() -> bound_QC-variable of Al(), r() -> Element of CQC-WFF(Al())}
:
F(All(x(),r())) = Q(x(),F(r()))
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds d = F
(p) iff ex F being Function of CQC-WFF(Al()), D() st
d = F.p & F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() 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)
proof
  consider G being Function of CQC-WFF(Al()), D() such that
A2: F(r()) = G.r() and
A3: G.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() holds
G.(P!l) = A(k,P,l) & G.('not' r) = N(G.r) &
G.(r '&' s) = C(G.r,G.s) & G.All(x,r) = Q(x,G.r) by A1;
  consider F being Function of CQC-WFF(Al()), D() such that
A4: F.VERUM(Al()) = V() &
  for r,s being Element of CQC-WFF(Al())
  for x being bound_QC-variable of Al()
  for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() 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) from CQCFuncEx;
A5: F.All(x(),r()) = Q(x(),F.r()) by A4;
  F = G from CQCFuncUniq(A4,A3);
  hence thesis by A1,A4,A5,A2;
end;

reserve x,y for bound_QC-variable of A;
reserve a for free_QC-variable of A;
reserve p,q for Element of QC-WFF(A);
reserve l,l1,l2,ll for FinSequence of QC-variables(A);
reserve r,s for Element of CQC-WFF(A);

Lm2: for F1,F2 being Function of QC-WFF(A),QC-WFF(A) st
( for q holds F1.VERUM(A) = VERUM(A) & (q is atomic implies F1.q =
(the_pred_symbol_of q)!Subst( the_arguments_of q,(A)a.0.-->x)) &
(q is negative implies F1.q = 'not' (F1.
the_argument_of q) ) & (q is conjunctive implies F1.q = (F1.
the_left_argument_of q) '&' (F1.the_right_argument_of q)) & (q is universal
implies F1.q = IFEQ(bound_in q,x,q,All(bound_in q,F1.the_scope_of q)))) & ( for
q holds F2.VERUM(A) = VERUM(A) & (q is atomic implies F2.q =
(the_pred_symbol_of q)!
Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative implies
F2.q = 'not' (F2.the_argument_of q) ) & (q is conjunctive implies F2.q = (F2.
the_left_argument_of q) '&' (F2.the_right_argument_of q)) & (q is universal
implies F2.q = IFEQ(bound_in q,x,q,All(bound_in q,F2.the_scope_of q)))) holds
F1 = F2
proof
  deffunc c((Element of QC-WFF(A)), Element of QC-WFF(A)) = $1 '&' $2;
  deffunc n(Element of QC-WFF(A)) = 'not' ($1);
  let F1,F2 be Function of QC-WFF(A),QC-WFF(A);
  deffunc a(Element of QC-WFF(A)) = (the_pred_symbol_of $1)!Subst(
  the_arguments_of $1,(A)a.0.-->x);
  deffunc q((Element of QC-WFF(A)), Element of QC-WFF(A)) =
      IFEQ(bound_in $1,x,$1,All(bound_in $1,$2));
  assume for q holds F1.VERUM(A) = VERUM(A) &
  (q is atomic implies F1.q = a(q)) & (q is negative implies
  F1.q = 'not' (F1.the_argument_of q) ) & (q is conjunctive
implies F1.q = (F1.the_left_argument_of q) '&' (F1.the_right_argument_of q)) &
  (q is universal implies F1.q = IFEQ(bound_in q,x,q,All(bound_in q,F1.
  the_scope_of q)));
  then
A1: for p being Element of QC-WFF(A) for d1,d2 being Element of QC-WFF(A)
holds (p = VERUM(A) implies F1.p = VERUM(A)) &
(p is atomic implies F1.p = a(p)) & (p is
negative & d1 = F1.the_argument_of p implies F1.p = n(d1)) & (p is conjunctive
& d1 = F1.the_left_argument_of p & d2 = F1.the_right_argument_of p implies F1.p
= c(d1,d2)) & (p is universal & d1 = F1.the_scope_of p implies F1.p = q(p,d1));
  assume for q holds F2.VERUM(A) = VERUM(A) & (q is atomic implies F2.q = (
  the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F2.q = 'not' (F2.the_argument_of q) ) & (q is conjunctive implies F2.q
  = (F2.the_left_argument_of q) '&' (F2.the_right_argument_of q)) & (q is
universal implies F2.q = IFEQ(bound_in q,x,q,All(bound_in q,F2.the_scope_of q))
  );
  then
A2: for p being Element of QC-WFF(A) for d1,d2 being Element of QC-WFF(A)
holds (p = VERUM(A) implies F2.p = VERUM(A)) &
(p is atomic implies F2.p = a(p)) & (p is negative &
d1 = F2.the_argument_of p implies F2.p = n(d1)) & (p is conjunctive
& d1 = F2.the_left_argument_of p & d2 = F2.the_right_argument_of p implies F2.p
= c(d1,d2)) & (p is universal & d1 = F2.the_scope_of p implies F2.p = q(p,d1));
  thus F1 = F2 from QC_LANG3:sch 1(A1,A2);
end;

definition
  let A,p,x;
  func p.x -> Element of QC-WFF(A) means
  :Def3:
  ex F being Function of QC-WFF(A),
QC-WFF(A) st it = F.p & for q holds F.VERUM(A) = VERUM(A) &
(q is atomic implies F.q =
(the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) &
(q is negative implies F.q = 'not' (F.the_argument_of q) ) &
(q is conjunctive implies F.q = (F.the_left_argument_of q) '&'
(F.the_right_argument_of q)) & (q is universal implies F.q =
IFEQ(bound_in q,x,q,All(bound_in q,F.the_scope_of q)));
  existence
  proof
    deffunc q((Element of QC-WFF(A)), Element of QC-WFF(A)) =
    IFEQ(bound_in $1,x,$1,
    All(bound_in $1,$2));
    deffunc c((Element of QC-WFF(A)), Element of QC-WFF(A)) = $1 '&' $2;
    deffunc n(Element of QC-WFF(A)) = 'not' ($1);
    deffunc a(Element of QC-WFF(A)) = (the_pred_symbol_of $1)!Subst(
    the_arguments_of $1,(A)a.0.-->x);
    consider F being Function of QC-WFF(A), QC-WFF(A) such that
A1: F.VERUM(A) = VERUM(A) & for p being Element of QC-WFF(A) holds (p is atomic
implies F.p = a(p)) & (p is negative implies F.p = n(F.the_argument_of p)) & (p
is conjunctive implies F.p = c(F.the_left_argument_of p,F.the_right_argument_of
p)) & (p is universal implies F.p = q(p,F.the_scope_of p)) from QC_LANG1:sch 3;
    take F.p,F;
    thus F.p = F.p;
    thus thesis by A1;
  end;
  uniqueness by Lm2;
end;

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

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

theorem Th17:
  for k being Nat
  for P being QC-pred_symbol of k,A for l being QC-variable_list of
  k,A holds (P!l).x = P!Subst(l,(A)a.0.-->x)
proof let k be Nat;
  let P be QC-pred_symbol of k,A;
  let l be QC-variable_list of k, A;
  reconsider P9 = P as QC-pred_symbol of A;
A1: P!l is atomic by QC_LANG1:def 18;
  then the_arguments_of (P!l) = l & the_pred_symbol_of (P!l) = P9 by
QC_LANG1:def 22,def 23;
  hence thesis by A1,Th16;
end;

theorem Th18:
  p is negative implies p.x = 'not'((the_argument_of p).x)
proof
  consider F being Function of QC-WFF(A),QC-WFF(A) such that
A1: p.x = F.p and
A2: for q holds F.VERUM(A) = VERUM(A) & (q is atomic implies F.q = (
  the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F.q = 'not' (F.the_argument_of q) ) & (q is conjunctive implies F.q = (
  F.the_left_argument_of q) '&' (F.the_right_argument_of q)) & (q is universal
  implies F.q = IFEQ(bound_in q,x,q,All(bound_in q,F.the_scope_of q))) by Def3;
  consider G being Function of QC-WFF(A),QC-WFF(A) such that
A3: (the_argument_of p).x = G.(the_argument_of p) and
A4: for q holds G.VERUM(A) = VERUM(A) & (q is atomic implies G.q = (
  the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies G.q = 'not' (G.the_argument_of q) ) & (q is conjunctive implies G.q = (
  G.the_left_argument_of q) '&' (G.the_right_argument_of q)) & (q is universal
  implies G.q = IFEQ(bound_in q,x,q,All(bound_in q,G.the_scope_of q))) by Def3;
  F = G by A2,A4,Lm2;
  hence thesis by A1,A2,A3;
end;

theorem Th19:
  ('not' p).x = 'not'(p.x)
proof
  set 9p = 'not' p;
A1: 9p is negative by QC_LANG1:def 19;
  then the_argument_of 9p = p by QC_LANG1:def 24;
  hence thesis by A1,Th18;
end;

theorem Th20:
  p is conjunctive implies p.x = ((the_left_argument_of p).x) '&'
  ((the_right_argument_of p).x)
proof
  consider F being Function of QC-WFF(A),QC-WFF(A) such that
A1: p.x = F.p and
A2: for q holds F.VERUM(A) = VERUM(A) & (q is atomic implies F.q = (
  the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F.q = 'not' (F.the_argument_of q) ) & (q is conjunctive implies F.q = (
  F.the_left_argument_of q) '&' (F.the_right_argument_of q)) & (q is universal
  implies F.q = IFEQ(bound_in q,x,q,All(bound_in q,F.the_scope_of q))) by Def3;
  consider F2 being Function of QC-WFF(A),QC-WFF(A) such that
A3: (the_right_argument_of p).x = F2.(the_right_argument_of p) and
A4: for q holds F2.VERUM(A) = VERUM(A) & (q is atomic implies F2.q = (
  the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F2.q = 'not' (F2.the_argument_of q) ) & (q is conjunctive implies F2.q
  = (F2.the_left_argument_of q) '&' (F2.the_right_argument_of q)) & (q is
universal implies F2.q = IFEQ(bound_in q,x,q,All(bound_in q,F2.the_scope_of q))
  ) by Def3;
A5: F2 = F by A2,A4,Lm2;
  consider F1 being Function of QC-WFF(A),QC-WFF(A) such that
A6: (the_left_argument_of p).x = F1.(the_left_argument_of p) and
A7: for q holds F1.VERUM(A) = VERUM(A) & (q is atomic implies F1.q = (
  the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F1.q = 'not' (F1.the_argument_of q) ) & (q is conjunctive implies F1.q
  = (F1.the_left_argument_of q) '&' (F1.the_right_argument_of q)) & (q is
universal implies F1.q = IFEQ(bound_in q,x,q,All(bound_in q,F1.the_scope_of q))
  ) by Def3;
  F1 = F by A2,A7,Lm2;
  hence thesis by A1,A2,A6,A3,A5;
end;

theorem Th21:
  (p '&' q).x = (p.x) '&' (q.x)
proof
  set pq = p '&' q;
A1: p '&' q is conjunctive by QC_LANG1:def 20;
  then the_left_argument_of pq = p & the_right_argument_of pq = q by
QC_LANG1:def 25,def 26;
  hence thesis by A1,Th20;
end;

Lm3: p is universal implies p.x = IFEQ(bound_in p,x,p,All(bound_in p,(
the_scope_of p).x))
proof
  consider F being Function of QC-WFF(A),QC-WFF(A) such that
A1: p.x = F.p and
A2: for q holds F.VERUM(A) = VERUM(A) & (q is atomic implies F.q = (
  the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F.q = 'not' (F.the_argument_of q) ) & (q is conjunctive implies F.q = (
  F.the_left_argument_of q) '&' (F.the_right_argument_of q)) & (q is universal
  implies F.q = IFEQ(bound_in q,x,q,All(bound_in q,F.the_scope_of q))) by Def3;
  consider G being Function of QC-WFF(A),QC-WFF(A) such that
A3: (the_scope_of p).x = G.(the_scope_of p) and
A4: for q holds G.VERUM(A) = VERUM(A) & (q is atomic implies G.q = (
  the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies G.q = 'not' (G.the_argument_of q) ) & (q is conjunctive implies G.q = (
  G.the_left_argument_of q) '&' (G.the_right_argument_of q)) & (q is universal
  implies G.q = IFEQ(bound_in q,x,q,All(bound_in q,G.the_scope_of q))) by Def3;
  F = G by A2,A4,Lm2;
  hence thesis by A1,A2,A3;
end;

theorem Th22:
  p is universal & bound_in p = x implies p.x = p
proof
  assume p is universal;
  then (p.x) = IFEQ(bound_in p,x,p,All(bound_in p,(the_scope_of p).x)) by Lm3;
  hence thesis by FUNCOP_1:def 8;
end;

theorem Th23:
  p is universal & bound_in p <> x implies p.x = All(bound_in p,(
  the_scope_of p).x)
proof
  assume p is universal;
  then (p.x) = IFEQ(bound_in p,x,p,All(bound_in p,(the_scope_of p).x)) by Lm3;
  hence thesis by FUNCOP_1:def 8;
end;

theorem Th24:
  (All(x,p)).x = All(x,p)
proof
  set q = All(x,p);
A1: q is universal by QC_LANG1:def 21;
  then bound_in q = x by QC_LANG1:def 27;
  hence thesis by A1,Th22;
end;

theorem Th25:
  x<>y implies (All(x,p)).y = All(x,p.y)
proof
  set q = All(x,p);
A1: q is universal by QC_LANG1:def 21;
  then the_scope_of q = p & bound_in q = x by QC_LANG1:def 27,def 28;
  hence thesis by A1,Th23;
end;

theorem Th26:
  Free p = {} implies p.x = p
proof
  defpred P[Element of QC-WFF(A)] means Free $1 = {} implies $1.x = $1;
A1: for p st P[p] holds P['not' p] by Th19,QC_LANG3:55;
A2: for p,q st P[p] & P[q] holds P[p '&' q]
  proof
    let p,q;
    assume
A3: ( Free p = {} implies p.x = p)&( Free q = {} implies q.x = q);
    assume Free(p '&' q) = {};
    then (Free p) \/ (Free q) = {} by QC_LANG3:57;
    hence thesis by A3,Th21;
  end;
A4: for k being Nat
  for P being (QC-pred_symbol of k,A),l being QC-variable_list of k, A
  holds P[P!l]
  proof
    let k be Nat;
    let P be (QC-pred_symbol of k,A),l be QC-variable_list of k, A;
    assume
A5: Free(P!l) = {};
A6: now
      let j be Nat;
      assume
A7:   1 <= j & j <= len l;
      now
        assume l.j = (A)a.0;
        then (A)a.0 in { l.i where i is Nat : 1 <= i &
            i <= len l & l.i in free_QC-variables(A) }
        by A7;
        hence contradiction by A5,QC_LANG3:54;
      end;
      hence Subst(l,(A)a.0.-->x).j = l.j by A7,Th3;
    end;
    len Subst(l,(A)a.0.-->x) = len l by Def1;
    then Subst(l,(A)a.0.-->x) = l by A6,FINSEQ_1:14;
    hence thesis by Th17;
  end;
A8: for y,p st P[p] holds P[All(y, p)]
  proof
    let y,p;
    assume
A9: Free p = {} implies p.x = p;
A10: x = y implies All(y, p).x = All(y, p) by Th24;
    assume Free All(y,p) = {};
    hence thesis by A9,A10,Th25,QC_LANG3:58;
  end;
A11: P[VERUM(A)] by Th15;
  for p holds P[p] from QC_LANG1:sch 1(A4,A11,A1,A2,A8);
  hence thesis;
end;

theorem
  r.x = r
proof
  Free r = {} by Th4;
  hence thesis by Th26;
end;

theorem
  Fixed(p.x) = Fixed p
proof
  defpred P[Element of QC-WFF(A)] means Fixed($1.x) = Fixed $1;
A1: for p st P[p] holds P['not' p]
  proof
    let p such that
A2: Fixed (p.x) = Fixed p;
    thus Fixed(('not' p).x) = Fixed('not' (p.x)) by Th19
      .= Fixed p by A2,QC_LANG3:65
      .= Fixed 'not' p by QC_LANG3:65;
  end;
A3: for p,q st P[p] & P[q] holds P[p '&' q]
  proof
    let p,q such that
A4: Fixed(p.x) = Fixed(p) & Fixed(q.x) = Fixed q;
    thus Fixed((p '&' q).x) = Fixed((p.x) '&' (q.x)) by Th21
      .= Fixed(p) \/ Fixed(q) by A4,QC_LANG3:67
      .= Fixed (p '&' q) by QC_LANG3:67;
  end;
A5: for k for P being (QC-pred_symbol of k,A),l being QC-variable_list of k, A
  holds P[P!l]
  proof
    let k;
    let P be (QC-pred_symbol of k,A),l be QC-variable_list of k, A;
    set F1 = { l.i : 1 <= i & i <= len l & l.i in fixed_QC-variables(A) };
    set ll = Subst(l,(A)a.0.-->x);
    set F2 = { ll.i : 1 <= i & i <= len ll & ll.i in fixed_QC-variables(A) };
A6: len l = len ll by Def1;
    now
      let y be object;
      thus y in F1 implies y in F2
      proof
        assume y in F1;
        then consider i such that
A7:     y = l.i and
A8:     1 <= i & i <= len l and
A9:     l.i in fixed_QC-variables(A);
        l.i <> (A)a.0 by A9,QC_LANG3:32;
        then ll.i = l.i by A8,Th3;
        hence thesis by A6,A7,A8,A9;
      end;
      assume y in F2;
      then consider i such that
A10:  y = ll.i and
A11:  1 <= i & i <= len ll and
A12:  ll.i in fixed_QC-variables(A);
      now
        assume l.i = (A)a.0;
        then ll.i = x by A6,A11,Th3;
        hence contradiction by A12,Lm1;
      end;
      then ll.i = l.i by A6,A11,Th3;
      hence y in F1 by A6,A10,A11,A12;
    end;
    then
A13: F1 = F2 by TARSKI:2;
    Fixed(P!l) = F1 & Fixed(P!ll) = F2 by QC_LANG3:64;
    hence thesis by A13,Th17;
  end;
A14: for y,p st P[p] holds P[All(y,p)]
  proof
    let y,p such that
A15: Fixed(p.x) = Fixed p;
    now
      assume x <> y;
      hence Fixed(All(y,p).x) = Fixed(All(y,p.x)) by Th25
        .= Fixed(p) by A15,QC_LANG3:68
        .= Fixed(All(y,p)) by QC_LANG3:68;
    end;
    hence thesis by Th24;
  end;
A16: P[VERUM(A)] by Th15;
  for p holds P[p] from QC_LANG1:sch 1(A5,A16,A1,A3,A14);
  hence thesis;
end;