SUBSTUT2

:: Substitution in First-Order Formulas -- Part II. {T}he Construction of
:: First-Order Formulas
::  by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-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 NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, SUBSTUT1, MCART_1,
      MARGREL1, REALSET1, FINSEQ_1, ORDINAL4, XBOOLEAN, CARD_1, ZFMISC_1,
      RELAT_1, BVFUNC_2, XBOOLE_0, FUNCT_1, TARSKI, ZF_LANG, FUNCT_4, FUNCOP_1,
      CLASSES2, SUBLEMMA, PARTFUN1, CQC_SIM1, ARYTM_3, XXREAL_0, ARYTM_1,
      SUBSTUT2, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, ORDINAL1, SUBSET_1, FINSEQ_1,
      FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3, PARTFUN1, NUMBERS, XCMPLX_0,
      XXREAL_0, NAT_1, CQC_LANG, FUNCOP_1, RELAT_1, FUNCT_4, FUNCT_2, CQC_SIM1,
      DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA;
 constructors PARTFUN1, DOMAIN_1, XXREAL_0, NAT_1, INT_1, QC_LANG3, CQC_SIM1,
      SUBLEMMA, RELSET_1, XTUPLE_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      XREAL_0, NAT_1, INT_1, QC_LANG1, CQC_LANG, SUBSTUT1, SUBLEMMA, XTUPLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI;
 equalities FUNCOP_1;
 expansions TARSKI;
 theorems TARSKI, FUNCT_1, XBOOLE_0, XBOOLE_1, CQC_LANG, QC_LANG1, ZFMISC_1,
      RELAT_1, QC_LANG3, PARTFUN1, RELSET_1, QC_LANG2, SUBSTUT1, FUNCT_4,
      SUBLEMMA, CQC_SIM1, FUNCT_2, NAT_1, INT_1, XREAL_1, XXREAL_0, FUNCOP_1,
      CARD_1, XTUPLE_0;
 schemes CQC_LANG, NAT_1;

begin :: Further Properties of Substitution

reserve Al for QC-alphabet;
reserve a,b,b1 for object,
  i,j,k,n for Nat,
  p,q,r,s for Element of CQC-WFF(Al),
  x,y,y1 for bound_QC-variable of Al,
  P for QC-pred_symbol of k,Al,
  l,ll for CQC-variable_list of k,Al,
  Sub,Sub1 for CQC_Substitution of Al,
  S,S1,S2 for Element of CQC-Sub-WFF(Al),
  P1,P2 for Element of QC-pred_symbols(Al);

theorem Th1:
  for Sub holds ex S st S`1 = VERUM(Al) & S`2 = Sub
proof
  let Sub;
  VERUM(Al) = <*[0,0]*> by QC_LANG1:def 14;
  then reconsider S = [VERUM(Al),Sub] as Element of QC-Sub-WFF(Al)
    by SUBSTUT1:def 16;
  take S;
    set X = { G where G is Element of QC-Sub-WFF(Al) :
              G`1 is Element of CQC-WFF(Al) };
    X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
    then A1: for G being Element of QC-Sub-WFF(Al) holds
        G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
  S`1 = VERUM(Al);
  then reconsider S as Element of CQC-Sub-WFF(Al) by A1;
  S`2 = Sub;
  hence thesis;
end;

Lm1: for k,l being Nat st P is (QC-pred_symbol of k,Al) & P is (
QC-pred_symbol of l,Al) holds k = l
proof
  let k,l be Nat;
  assume
A1: P is (QC-pred_symbol of k,Al) & P is (QC-pred_symbol of l,Al);
  then P in l-ary_QC-pred_symbols(Al);
  then P in {P2 : the_arity_of P2 = l} by QC_LANG1:def 9;
  then
A2: ex P2 st P2 = P & the_arity_of P2 = l;
  P in k-ary_QC-pred_symbols(Al) by A1;
  then P in {P1 : the_arity_of P1 = k} by QC_LANG1:def 9;
  then ex P1 st P1 = P & the_arity_of P1 = k;
  hence thesis by A2;
end;

theorem Th2:
  for Sub holds ex S st S`1 = P!ll & S`2 = Sub
proof
  let Sub;
  P is QC-pred_symbol of the_arity_of P,Al by QC_LANG3:1;
  then k = the_arity_of P by Lm1;
  then [<*P*>^ll,Sub] in QC-Sub-WFF(Al) & len ll = the_arity_of P
    by CARD_1:def 7,SUBSTUT1:def 16;
  then reconsider S = [P!ll,Sub] as Element of QC-Sub-WFF(Al)
    by QC_LANG1:def 12;
    set X = { G where G is Element of QC-Sub-WFF(Al) :
              G`1 is Element of CQC-WFF(Al) };
    X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
    then A1: for G being Element of QC-Sub-WFF(Al) holds
        G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
  take S;
  S`1 = P!ll;
  then reconsider S as Element of CQC-Sub-WFF(Al) by A1;
  S`2 = Sub;
  hence thesis;
end;

theorem
  for k,l being Nat st P is (QC-pred_symbol of k,Al) & P is (
  QC-pred_symbol of l,Al) holds k = l by Lm1;

theorem Th4:
  (for Sub holds ex S st S`1 = p & S`2 = Sub) implies for Sub holds
  ex S st S`1 = 'not' p & S`2 = Sub
proof
  assume
A1: for Sub holds ex S st S`1 = p & S`2 = Sub;
  let Sub;
  consider S such that
A2: S`1 = p & S`2 = Sub by A1;
  S = [p,Sub] by A2,SUBSTUT1:10;
  then [p,Sub] in QC-Sub-WFF(Al);
  then [@p,Sub] in QC-Sub-WFF(Al) by QC_LANG1:def 13;
  then [<*[1, 0]*>^@p,Sub] in QC-Sub-WFF(Al) by SUBSTUT1:def 16;
  then reconsider S = ['not' p,Sub] as Element of QC-Sub-WFF(Al)
   by QC_LANG1:def 15;
    set X = { G where G is Element of QC-Sub-WFF(Al) :
              G`1 is Element of CQC-WFF(Al) };
    X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
    then A3: for G being Element of QC-Sub-WFF(Al) holds
        G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
  take S;
  S`1 = 'not' p;
  then reconsider S as Element of CQC-Sub-WFF(Al) by A3;
  S`2 = Sub;
  hence thesis;
end;

theorem Th5:
  (for Sub holds ex S st S`1 = p & S`2 = Sub) & (for Sub holds ex S
st S`1 = q & S`2 = Sub) implies for Sub holds ex S st S`1 = p '&' q & S`2 = Sub
proof
  assume that
A1: for Sub holds ex S st S`1 = p & S`2 = Sub and
A2: for Sub holds ex S st S`1 = q & S`2 = Sub;
  let Sub;
  consider S1 such that
A3: S1`1 = p & S1`2 = Sub by A1;
  consider S2 such that
A4: S2`1 = q & S2`2 = Sub by A2;
  S2 = [q,Sub] by A4,SUBSTUT1:10;
  then [q,Sub] in QC-Sub-WFF(Al);
  then
A5: [@q,Sub] in QC-Sub-WFF(Al) by QC_LANG1:def 13;
  S1 = [p,Sub] by A3,SUBSTUT1:10;
  then [p,Sub] in QC-Sub-WFF(Al);
  then [@p,Sub] in QC-Sub-WFF(Al) by QC_LANG1:def 13;
  then [<*[2, 0]*>^@p^@q,Sub] in QC-Sub-WFF(Al) by A5,SUBSTUT1:def 16;
  then reconsider S = [p '&' q,Sub] as Element of QC-Sub-WFF(Al)
     by QC_LANG1:def 16;
    set X = { G where G is Element of QC-Sub-WFF(Al) :
              G`1 is Element of CQC-WFF(Al) };
    X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
    then A6: for G being Element of QC-Sub-WFF(Al) holds
        G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
  take S;
  S`1 = p '&' q;
  then reconsider S as Element of CQC-Sub-WFF(Al) by A6;
  S`2 = Sub;
  hence thesis;
end;

definition
  let Al, p, Sub;
  redefine func [p,Sub] -> Element of [:QC-WFF(Al),vSUB(Al):];  :: redefines [ (TARSKI, definition)
  coherence by ZFMISC_1:def 2;
end;

theorem Th6:
  dom RestrictSub(x,All(x,p),Sub) misses {x}
proof
  set finSub = RestrictSub(x,All(x,p),Sub);
  now
    set q = All(x,p);
    set X = {y1 : y1 in still_not-bound_in q & y1 is Element of dom Sub & y1
    <> x & y1 <> Sub.y1};
    assume dom finSub meets {x};
    then consider b being object such that
A1: b in dom finSub and
A2: b in {x} by XBOOLE_0:3;
    finSub = Sub|X by SUBSTUT1:def 6;
    then finSub = (@Sub)|X by SUBSTUT1:def 2;
    then @finSub = (@Sub)|X by SUBSTUT1:def 2;
    then dom @finSub = dom @Sub /\ X by RELAT_1:61;
    then
A3: dom @finSub c= X by XBOOLE_1:17;
    b in dom @finSub by A1,SUBSTUT1:def 2;
    then b in X by A3;
    then ex y st y = b & y in still_not-bound_in q & y is Element of dom Sub &
    y <> x & y <> Sub.y;
    hence contradiction by A2,TARSKI:def 1;
  end;
  hence thesis;
end;

theorem Th7:
  x in rng RestrictSub(x,All(x,p),Sub) implies S_Bound([All(x,p),
  Sub]) = x.upVar(RestrictSub(x,All(x,p),Sub),p)
proof
  set finSub = RestrictSub(x,All(x,p),Sub);
  set S = [All(x,p),Sub];
  assume
A1: x in rng finSub;
  reconsider q = S`1 as Element of CQC-WFF(Al);
A2: S`2 = Sub;
  bound_in q = x & the_scope_of q = p by QC_LANG2:7;
  hence thesis by A1,A2,SUBSTUT1:def 36;
end;

theorem Th8:
  not x in rng RestrictSub(x,All(x,p),Sub) implies S_Bound([All(x,p ),Sub]) = x
proof
  set finSub = RestrictSub(x,All(x,p),Sub);
  set S = [All(x,p),Sub];
  assume
A1: not x in rng finSub;
  reconsider q = S`1 as Element of CQC-WFF(Al);
  S`2 = Sub & bound_in q = x by QC_LANG2:7;
  hence thesis by A1,SUBSTUT1:def 36;
end;

theorem Th9:
  ExpandSub(x,p,RestrictSub(x,All(x,p),Sub)) = @RestrictSub(x,All(x
  ,p),Sub) +* (x|S_Bound([All(x,p),Sub]))
proof
  set finSub = RestrictSub(x,All(x,p),Sub);
A1: now
    reconsider F = {[x,x.upVar(finSub,p)]} as Function;
    dom F = {x} by RELAT_1:9;
    then dom finSub misses dom F by Th6;
    then dom @finSub misses dom F by SUBSTUT1:def 2;
    then
A2: @finSub \/ F = @finSub +* F by FUNCT_4:31;
    assume
A3: x in rng finSub;
    then ExpandSub(x,p,finSub) = finSub \/ F by SUBSTUT1:def 13;
    then {[x,x.upVar(finSub,p)]} = x .--> x.upVar(finSub,p) &
    ExpandSub(x,p,finSub) = @finSub +* F by A2,FUNCT_4:82,SUBSTUT1:def 2;
    hence thesis by A3,Th7;
  end;
  now
    reconsider F = {[x,x]} as Function;
    dom F = {x} by RELAT_1:9;
    then dom finSub misses dom F by Th6;
    then dom @finSub misses dom F by SUBSTUT1:def 2;
    then
A4: @finSub \/ F = @finSub +* F by FUNCT_4:31;
    assume
A5: not x in rng finSub;
    then ExpandSub(x,p,finSub) = finSub \/ F by SUBSTUT1:def 13;
    then {[x,x]} = x .--> x & ExpandSub(x,p,finSub) = @finSub +* F by A4,
FUNCT_4:82,SUBSTUT1:def 2;
    hence thesis by A5,Th8;
  end;
  hence thesis by A1;
end;

theorem Th10:
  S`2 = @RestrictSub(x,All(x,p),Sub) +* (x|S_Bound([All(x,p),Sub])
  ) & S`1 = p implies [S,x] is quantifiable & ex S1 st S1 = [All(x,p),Sub]
proof
  set Sub1 = @RestrictSub(x,All(x,p),Sub) +* (x|S_Bound([All(x,p),Sub]));
  reconsider Sub as CQC_Substitution of Al;
  assume that
A1: S`2 = Sub1 and
A2: S`1 = p;
A3: [S,x]`2 = x & ([S,x]`1)`1 = p by A2;
A4: the_scope_of All(x,p) = p & All(x,p) is universal by QC_LANG1:def 21
,QC_LANG2:7;
  Sub1 = ExpandSub(x,p,RestrictSub(x,All(x,p),Sub)) & bound_in All(x,p) =
  x by Th9,QC_LANG2:7;
  then All(x,p),Sub PQSub Sub1 by A4,SUBSTUT1:def 14;
  then consider a such that
A5: a = [[All(x,p),Sub],Sub1] and
A6: All(x,p),Sub PQSub Sub1;
  a in QSub(Al) by A5,A6,SUBSTUT1:def 15;
  then
A7: (QSub(Al)).[All(x,p),Sub] = Sub1 by A5,FUNCT_1:1;
A8: ([S,x]`1)`2 = Sub1 by A1;
  hence [S,x] is quantifiable by A7,A3,SUBSTUT1:def 22;
A9: [S,x] is quantifiable by A7,A8,A3,SUBSTUT1:def 22;
  then reconsider Sub as second_Q_comp of [S,x] by A7,A8,A3,SUBSTUT1:def 23;
  take S1 = CQCSub_All([S,x],Sub);
  S1 = Sub_All([S,x],Sub) by A9,SUBLEMMA:def 5;
  hence thesis by A3,A9,SUBSTUT1:def 24;
end;

theorem Th11:
  (for Sub holds ex S st S`1 = p & S`2 = Sub) implies for Sub
  holds ex S st S`1 = All(x,p) & S`2 = Sub
proof
  assume
A1: for Sub holds ex S st S`1 = p & S`2 = Sub;
  let Sub;
  set Sub1 = @RestrictSub(x,All(x,p),Sub) +* (x|S_Bound([All(x,p),Sub]));
  Sub1 is CQC_Substitution of Al iff Sub1 is Element of
    PFuncs(bound_QC-variables(Al),bound_QC-variables(Al)) by SUBSTUT1:def 1;
  then reconsider Sub1 as CQC_Substitution of Al
   by PARTFUN1:45;
  ex S st S`1 = p & S`2 = Sub1 by A1;
  then consider S1 such that
A2: S1 = [All(x,p),Sub] by Th10;
  take S1;
  thus thesis by A2;
end;

theorem Th12:
  for p, Sub holds ex S st S`1 = p & S`2 = Sub
proof
  defpred P[Element of CQC-WFF(Al)] means
      for Sub holds ex S st S`1 = $1 & S`2 = Sub;
A1: for p,q,x,k for ll being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!ll] &
(P[p] implies P['not' p]) & (P[p] & P[q] implies P[p '&' q]) &
(P[p] implies P[All(x,p)]) by Th1,Th2,Th4,Th5,Th11;
  thus for p holds P[p] from CQC_LANG:sch 1(A1);
end;

definition
  let Al,p,Sub;
  redefine func [p,Sub] -> Element of CQC-Sub-WFF(Al);  :: redefines [ (TARSKI, definition)
  coherence
  proof
    ex S st S`1 = p & S`2 = Sub by Th12;
    hence thesis by SUBSTUT1:10;
  end;
end;

notation
  let Al,x,y;
  synonym Sbst(x,y) for x .--> y;
end;

definition
  let Al,x,y;
  redefine func Sbst(x,y) -> CQC_Substitution of Al;  :: redefines Sbst (SUBSTUT2, synonym) → .--> (FUNCOP_1, definition)
  coherence
  proof
A1: x .--> y is CQC_Substitution of Al iff x .--> y is Element of
    PFuncs(bound_QC-variables(Al),bound_QC-variables(Al)) by SUBSTUT1:def 1;
    dom(x .--> y) = {x} & rng(x .--> y) = {y} by FUNCOP_1:8;
    then x .--> y is PartFunc of bound_QC-variables(Al),bound_QC-variables(Al)
       by RELSET_1:4;
    hence thesis by A1,PARTFUN1:45;
  end;
end;

begin :: Facts about Substitution and Quantifiers of a Formula

definition
  let Al,p,x,y;
  func p.(x,y) -> Element of CQC-WFF(Al) equals
  CQC_Sub([p,Sbst(x,y)]);
  coherence;
end;

scheme
  CQCInd1 { Al() -> QC-alphabet, P[set]} :
for p being Element of CQC-WFF(Al()) holds P[p]
provided
A1: for p being Element of CQC-WFF(Al()) st QuantNbr(p) = 0 holds P[p] and
A2: for k st for p being Element of CQC-WFF(Al()) st QuantNbr(p) = k
holds P[p] holds for p being Element of CQC-WFF(Al()) st QuantNbr(p) = k+1
holds P[p]
proof
  let p be Element of CQC-WFF(Al());
  defpred Q[Nat] means for p being Element of CQC-WFF(Al())
   st QuantNbr(p) = $1 holds P[p];
A3: for k being Nat st Q[k] holds Q[k + 1] by A2;
A4: Q[0] by A1;
  for k holds Q[k] from NAT_1:sch 2(A4,A3);
  then Q[QuantNbr(p)];
  hence thesis;
end;

scheme
  CQCInd2 {Al() -> QC-alphabet, P[set]}:
   for p being Element of CQC-WFF(Al()) holds P[p]
provided
A1: for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= 0 holds P[p] and
A2: for k st for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= k
holds P[p] holds for p being Element of CQC-WFF(Al())
st QuantNbr(p) <= k+1 holds P[p]
proof
  let p being Element of CQC-WFF(Al());
  defpred Q[Nat] means
    for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= $1 holds P[p];
A3: for k st Q[k] holds Q[k + 1] by A2;
A4: Q[0] by A1;
  for k holds Q[k] from NAT_1:sch 2(A4,A3);
  then Q[QuantNbr(p)];
  hence thesis;
end;

theorem
  VERUM(Al).(x,y) = VERUM(Al)
proof
  set S = [VERUM(Al),Sbst(x,y)];
  S is Al-Sub_VERUM by SUBSTUT1:def 19;
  hence thesis by SUBLEMMA:3;
end;

theorem
  (P!l).(x,y) = P!CQC_Subst(l,Sbst(x,y)) & QuantNbr(P!l) = QuantNbr((P!l
  ).(x,y))
proof
  set S = [P!l,Sbst(x,y)];
  S = Sub_P(P,l,Sbst(x,y)) by SUBSTUT1:9;
  then
A1: (P!l).(x,y) = P!CQC_Subst(l,Sbst(x,y)) by SUBLEMMA:8;
  QuantNbr(P!CQC_Subst(l,Sbst(x,y))) = 0 by CQC_SIM1:15;
  hence thesis by A1,CQC_SIM1:15;
end;

theorem Th15:
  QuantNbr(P!l) = QuantNbr(CQC_Sub([P!l,Sub]))
proof
  set S = [P!l,Sub];
  S = Sub_P(P,l,Sub) by SUBSTUT1:9;
  then
A1: CQC_Sub([(P!l),Sub]) = P!CQC_Subst(l,Sub) by SUBLEMMA:8;
  QuantNbr(P!CQC_Subst(l,Sub)) = 0 by CQC_SIM1:15;
  hence thesis by A1,CQC_SIM1:15;
end;

definition
  let Al;
  let S be Element of QC-Sub-WFF(Al);
  redefine func S`2 -> CQC_Substitution of Al;  :: redefines `2 (XTUPLE_0, definition)
  coherence
  proof
    ex p being Element of QC-WFF(Al),Sub st S = [p,Sub] by SUBSTUT1:8;
    hence thesis;
  end;
end;

theorem Th16:
  ['not' p,Sub] = Sub_not [p,Sub]
proof
  set S = [p,Sub];
  Sub_not S = ['not' S`1,S`2] by SUBSTUT1:def 20;
  hence thesis;
end;

theorem
  'not' p.(x,y) = 'not' (p.(x,y)) & (QuantNbr(p) = QuantNbr(p.(x,y))
  implies QuantNbr('not' p) = QuantNbr('not' p.(x,y)))
proof
  set S = ['not' p,Sbst(x,y)];
A1: S = Sub_not [p,Sbst(x,y)] by Th16;
  then
A2: ('not' p).(x,y) = 'not' CQC_Sub([p,Sbst(x,y)]) by SUBSTUT1:29;
  QuantNbr(p) = QuantNbr(p.(x,y)) implies QuantNbr('not' p) = QuantNbr((
  'not' p).(x,y))
  proof
    assume
A3: QuantNbr(p) = QuantNbr(p.(x,y));
    QuantNbr(('not' p).(x,y)) = QuantNbr(p.(x,y)) by A2,CQC_SIM1:16;
    hence thesis by A3,CQC_SIM1:16;
  end;
  hence thesis by A1,SUBSTUT1:29;
end;

theorem Th18:
  (for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) implies
  for Sub holds QuantNbr('not' p) = QuantNbr(CQC_Sub(['not' p,Sub]))
proof
  assume
A1: for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]));
  let Sub;
  set S = ['not' p,Sub];
  S = Sub_not [p,Sub] by Th16;
  then QuantNbr(CQC_Sub(S)) = QuantNbr('not' CQC_Sub([p,Sub])) by SUBSTUT1:29
    .= QuantNbr(CQC_Sub([p,Sub])) by CQC_SIM1:16
    .= QuantNbr(p) by A1;
  hence thesis by CQC_SIM1:16;
end;

theorem Th19:
  [p '&' q,Sub] = CQCSub_&([p,Sub],[q,Sub])
proof
  set S1 = [p,Sub];
  set S2 = [q,Sub];
A1: S1`1 = p & S2`1 = q;
A2: S1`2 = Sub & S2`2 = Sub;
  then CQCSub_&(S1,S2) = Sub_&(S1,S2) by SUBLEMMA:def 3;
  hence thesis by A2,A1,SUBSTUT1:def 21;
end;

theorem
  (p '&' q).(x,y) = (p.(x,y)) '&' (q.(x,y)) & ( QuantNbr(p) = QuantNbr(p
.(x,y)) & QuantNbr(q) = QuantNbr(q.(x,y)) implies QuantNbr(p '&'q) = QuantNbr((
  p '&' q).(x,y)))
proof
  set S = [p '&' q,Sbst(x,y)];
  set S1 = [p,Sbst(x,y)];
  set S2 = [q,Sbst(x,y)];
A1: S1`2 = Sbst(x,y) & S2`2 = Sbst(x,y);
  S = CQCSub_&(S1,S2) by Th19;
  then
A2: S = Sub_&(S1,S2) by A1,SUBLEMMA:def 3;
  then
A3: (p '&' q).(x,y) = (CQC_Sub(S1)) '&' (CQC_Sub(S2)) by A1,SUBSTUT1:31;
  QuantNbr(p) = QuantNbr(p.(x,y)) & QuantNbr(q) = QuantNbr(q.(x,y))
  implies QuantNbr(p '&' q) = QuantNbr((p '&' q).(x,y))
  proof
    assume
A4: QuantNbr(p) = QuantNbr(p.(x,y)) & QuantNbr(q) = QuantNbr(q.(x,y));
    QuantNbr((p '&' q).(x,y)) = QuantNbr(p.(x,y)) + QuantNbr(q.(x,y)) by A3,
CQC_SIM1:17;
    hence thesis by A4,CQC_SIM1:17;
  end;
  hence thesis by A1,A2,SUBSTUT1:31;
end;

theorem Th21:
  (for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) & (for
  Sub holds QuantNbr(q) = QuantNbr(CQC_Sub([q,Sub]))) implies for Sub holds
  QuantNbr(p '&' q) = QuantNbr(CQC_Sub[p '&' q,Sub])
proof
  assume that
A1: for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub])) and
A2: for Sub holds QuantNbr(q) = QuantNbr(CQC_Sub([q,Sub]));
  let Sub;
  set S = [p '&' q,Sub];
  set S1 = [p,Sub];
  set S2 = [q,Sub];
A3: S1`2 = Sub & S2`2 = Sub;
  S = CQCSub_&(S1,S2) by Th19;
  then S = Sub_&(S1,S2) by A3,SUBLEMMA:def 3;
  then CQC_Sub(S) = (CQC_Sub(S1)) '&' (CQC_Sub(S2)) by A3,SUBSTUT1:31;
  then
  QuantNbr(CQC_Sub(S)) = QuantNbr(CQC_Sub(S1)) + QuantNbr(CQC_Sub(S2)) by
CQC_SIM1:17
    .= QuantNbr(p) + QuantNbr(CQC_Sub(S2)) by A1
    .= QuantNbr(p) + QuantNbr(q) by A2;
  hence thesis by CQC_SIM1:17;
end;

definition
  let Al;
  func CFQ(Al) -> Function of CQC-Sub-WFF(Al),vSUB(Al) equals
  (QSub(Al))|CQC-Sub-WFF(Al);
  coherence
  proof
    now
      let a be object;
      assume a in CQC-Sub-WFF(Al);
      then consider p being Element of QC-WFF(Al),Sub such that
A1:   a = [p,Sub] by SUBSTUT1:8;
A2:   now
        set b = {};
        assume not p is universal;
        then p,Sub PQSub b by SUBSTUT1:def 14;
        then [[p,Sub],b] in QSub(Al) by SUBSTUT1:def 15;
        hence a in dom QSub(Al) by A1,FUNCT_1:1;
      end;
      now
        set b = ExpandSub(bound_in p,the_scope_of p, RestrictSub(bound_in p,p,
        Sub));
        assume p is universal;
        then p,Sub PQSub b by SUBSTUT1:def 14;
        then [[p,Sub],b] in QSub(Al) by SUBSTUT1:def 15;
        hence a in dom QSub(Al) by A1,FUNCT_1:1;
      end;
      hence a in dom QSub(Al) by A2;
    end;
    then CQC-Sub-WFF(Al) c= dom QSub(Al);
    then
A3: dom((QSub(Al))|CQC-Sub-WFF(Al)) = CQC-Sub-WFF(Al) by RELAT_1:62;
    rng((QSub(Al))|CQC-Sub-WFF(Al)) c= vSUB(Al)
    proof
      let b be object;
      assume b in rng((QSub(Al))|CQC-Sub-WFF(Al));
      then consider a being object such that
A4:   a in dom((QSub(Al))|CQC-Sub-WFF(Al)) & ((QSub(Al))|CQC-Sub-WFF(Al)).a = b
        by FUNCT_1:def 3;
A5:   (QSub(Al))|CQC-Sub-WFF(Al) c= QSub(Al) by RELAT_1:59;
      [a,b] in (QSub(Al))|CQC-Sub-WFF(Al) by A4,FUNCT_1:1;
      then consider p being Element of QC-WFF(Al),Sub,b1 such that
A6:   [a,b] = [[p,Sub],b1] and
A7:   p,Sub PQSub b1 by A5,SUBSTUT1:def 15;
A8:   now
A9:    b1 is CQC_Substitution of Al iff b1 is Element of
       PFuncs(bound_QC-variables(Al),bound_QC-variables(Al)) by SUBSTUT1:def 1;
       assume not p is universal;
       then b1 = {} by A7,SUBSTUT1:def 14;
       then b1 is PartFunc of bound_QC-variables(Al),bound_QC-variables(Al) by
RELSET_1:12;
       hence b is CQC_Substitution of Al by A9,A6,PARTFUN1:45,XTUPLE_0:1;
      end;
      now
        assume p is universal;
        then
        b1 = ExpandSub(bound_in p,the_scope_of p, RestrictSub(bound_in p,
        p,Sub)) by A7,SUBSTUT1:def 14;
        hence b is CQC_Substitution of Al by A6,XTUPLE_0:1;
      end;
      hence thesis by A8;
    end;
    hence thesis by A3,FUNCT_2:2;
  end;
end;

definition
  let Al,p,x,Sub;
  func QScope(p,x,Sub) -> CQC-WFF-like Element of [:QC-Sub-WFF(Al),
  bound_QC-variables(Al):] equals
  [[p,(CFQ(Al)).[All(x,p),Sub]],x];
  coherence;
end;

definition
  let Al,p,x,Sub;
  func Qsc(p,x,Sub) -> second_Q_comp of QScope(p,x,Sub) equals
  Sub;
  coherence
  proof
A1: (QScope(p,x,Sub)`1)`2 = (QSub(Al)).[All(x,p),Sub] by FUNCT_1:49;
A2: QScope(p,x,Sub)`2 = x & (QScope(p,x,Sub)`1)`1 = p;
    then QScope(p,x,Sub) is quantifiable by A1,SUBSTUT1:def 22;
    hence thesis by A2,A1,SUBSTUT1:def 23;
  end;
end;

theorem Th22:
  [All(x,p),Sub] = CQCSub_All(QScope(p,x,Sub),Qsc(p,x,Sub)) &
  QScope(p,x,Sub) is quantifiable
proof
  set S = [p,(CFQ(Al)).[All(x,p),Sub]];
  set B = [[p,(CFQ(Al)).[All(x,p),Sub]],x];
A1: B`2 = x & (B`1)`1 = p;
  [All(x,p),Sub] in CQC-Sub-WFF(Al);
  then
A2: [All(x,p),Sub] in dom CFQ(Al) by FUNCT_2:def 1;
  (B`1)`2 = (QSub(Al)).[All(B`2,(B`1)`1),Sub] by A2,FUNCT_1:47;
  then
A3: B is quantifiable by SUBSTUT1:def 22;
  then
  CQCSub_All(QScope(p,x,Sub),Qsc(p,x,Sub)) = Sub_All(QScope(p,x,Sub),Qsc(p
  ,x,Sub)) by SUBLEMMA:def 5;
  hence thesis by A1,A3,SUBSTUT1:def 24;
end;

theorem Th23:
  (for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) implies
  for Sub holds QuantNbr(All(x,p)) = QuantNbr(CQC_Sub([All(x,p),Sub]))
proof
  assume
A1: for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]));
  let Sub;
  set S1 = [All(x,p),Sub];
  set S = [p,(CFQ(Al)).[All(x,p),Sub]];
  set y = S_Bound(@CQCSub_All(QScope(p,x,Sub),Qsc(p,x,Sub)));
A2: QScope(p,x,Sub) is quantifiable by Th22;
A3: Sub_All(QScope(p,x,Sub),Qsc(p,x,Sub)) = CQCSub_All(QScope(p,x,Sub),Qsc(p
  ,x,Sub)) by Th22,SUBLEMMA:def 5
    .= S1 by Th22;
  then
A4: S1 is Sub_universal by A2,SUBSTUT1:def 28;
  then
A5: CQC_Sub(S1) = CQCQuant(S1,CQC_Sub(CQCSub_the_scope_of S1)) by SUBLEMMA:28;
  CQCSub_the_scope_of S1 = Sub_the_scope_of Sub_All(QScope(p,x,Sub),Qsc(p,
  x,Sub)) by A3,A4,SUBLEMMA:def 6
    .= [S,x]`1 by A2,SUBSTUT1:21
    .= S;
  then
  CQC_Sub(S1) = CQCQuant(CQCSub_All(QScope(p,x,Sub), Qsc(p,x,Sub)),CQC_Sub
  (S)) by A5,Th22;
  then QuantNbr(CQC_Sub(S1)) = QuantNbr(All(y,CQC_Sub(S))) by Th22,SUBLEMMA:31
    .= QuantNbr(CQC_Sub(S))+1 by CQC_SIM1:18
    .= QuantNbr(p)+1 by A1;
  hence thesis by CQC_SIM1:18;
end;

theorem Th24:
  QuantNbr(VERUM(Al)) = QuantNbr(CQC_Sub([VERUM(Al),Sub]))
proof
  [VERUM(Al),Sub] is Al-Sub_VERUM by SUBSTUT1:def 19;
  hence thesis by SUBLEMMA:3;
end;

theorem
  for p, Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))
proof
  defpred P[Element of CQC-WFF(Al)] means for Sub holds
QuantNbr($1) = QuantNbr(CQC_Sub([$1,Sub]));
A1: for r,s,x,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)]) by Th15,Th18,Th21,Th23,Th24;
  thus for r holds P[r] from CQC_LANG:sch 1(A1);
end;

theorem
  p is atomic implies ex k,P,ll st p = P!ll
proof
  assume p is atomic;
  then consider k being Nat, P being (QC-pred_symbol of k,Al),
l being QC-variable_list of k,Al such that
A1: p = P!l by QC_LANG1:def 18;
A2: { l.j : 1 <= j & j <= len l & l.j in fixed_QC-variables(Al) } = {} by A1,
CQC_LANG:7;
  { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(Al) } = {} by A1,
CQC_LANG:7;
  then reconsider l as CQC-variable_list of k,Al by A2,CQC_LANG:5;
  take k,P,l;
  thus thesis by A1;
end;

scheme
  CQCInd3 {Al() -> QC-alphabet, P[set]} :
for p being Element of CQC-WFF(Al()) st QuantNbr(p) = 0 holds P[p]
provided
A1: 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])
proof
  defpred Prop[Element of CQC-WFF(Al())] means QuantNbr($1) = 0 implies P[$1];
A2: for x being bound_QC-variable of Al(), p being Element of CQC-WFF(Al())
st Prop[p] holds Prop[All(x, p)]
  proof
  let x be bound_QC-variable of Al(), p be Element of CQC-WFF(Al()) such that
    Prop[p];
    assume QuantNbr(All(x,p)) = 0;
    then QuantNbr(p)+1 = 0 by CQC_SIM1:18;
    hence thesis;
  end;
  for p,q being Element of CQC-WFF(Al())
  st Prop[p] & Prop[q] holds Prop[p '&' q]
  proof
    let p,q be Element of CQC-WFF(Al()) such that
A3: Prop[p] & Prop[q];
    assume QuantNbr(p '&' q) = 0;
    then QuantNbr(p) + QuantNbr(q) = 0 by CQC_SIM1:17;
    hence thesis by A1,A3;
  end;
  then
A4: 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 Prop[VERUM(Al())] & Prop[P!l] &
(Prop[r] implies Prop['not' r]) & (Prop[r] & Prop[s] implies Prop[r '&' s])&
(Prop[r] implies Prop[All(x,r)]) by A1,A2,CQC_SIM1:16;
  for p being Element of CQC-WFF(Al()) holds Prop[p] from CQC_LANG:sch 1(A4);
  hence thesis;
end;

begin :: Results about the Construction of Formulas

reserve F1,F2,F3 for QC-formula of Al,
  L for FinSequence;

definition
  let Al;
  let G,H be QC-formula of Al;
  assume
A1: G is_subformula_of H;
  mode PATH of G,H -> FinSequence means
    :Def5:
    1 <= len it & it.1 = G & it.(
len it) = H & for k st 1 <= k & k < len it ex G1,H1
being Element of QC-WFF(Al) st it.k = G1 & it.(k+1) = H1 &
G1 is_immediate_constituent_of H1;
  existence
  proof
    ex n,L st 1 <= n & len L = n & L.1 = G & L.n = H & for k st 1 <= k & k
    < n ex G1,H1 being Element of QC-WFF(Al) st L.k = G1 & L.(k+1) = H1 & G1
    is_immediate_constituent_of H1 by A1,QC_LANG2:def 20;
    then consider L such that
A2: ex n st 1 <= n & len L = n & L.1 = G & L.n = H & for k st 1 <= k &
    k < n ex G1,H1 being Element of QC-WFF(Al) st L.k = G1 & L.(k+1) = H1 & G1
    is_immediate_constituent_of H1;
    take L;
    thus thesis by A2;
  end;
end;

theorem
  for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <=
  len L holds ex F3 st F3 = L.i & F3 is_subformula_of F2
proof
  let L be PATH of F1,F2;
  set n = len L;
  assume that
A1: F1 is_subformula_of F2 and
A2: 1 <= i and
A3: i <= n;
  n+1 <= n+i by A2,XREAL_1:6;
  then n+1+(-1) <= n+i+(-1) by XREAL_1:6;
  then
A4: n+(-i) <= n-1+i+(-i) by XREAL_1:6;
  i+(-i) <= n+(-i) by A3,XREAL_1:6;
  then reconsider l = n-i as Element of NAT by INT_1:3;
  defpred P[Nat] means $1 <= n-1 implies ex F3 st F3 = L.(n-$1) &
  F3 is_subformula_of F2;
A5: for k st P[k] holds P[k+1]
  proof
    let k such that
A6: P[k];
    assume
A7: k+1 <= n-1;
    then k+1+1 <= n-1+1 by XREAL_1:6;
    then
A8: 2+k+(-k) <= n+(-k) by XREAL_1:6;
    then reconsider j = n-k as Element of NAT by INT_1:3;
    n <= n+k by NAT_1:11;
    then n+(-k) <= n+k+(-k) by XREAL_1:6;
    then
A9: j-1 < n by XREAL_1:146,XXREAL_0:2;
A10: 1+1+(-1) <= j+(-1) by A8,XREAL_1:6;
    then reconsider j1 = j-1 as Element of NAT by INT_1:3;
    j1+1 = j;
    then
A11: ex G1,H1 being Element of QC-WFF(Al) st L.j1 = G1 & L.j = H1 & G1
    is_immediate_constituent_of H1 by A1,A10,A9,Def5;
    then reconsider F3 = L.j1 as QC-formula of Al;
    take F3;
    k < k+1 by NAT_1:13;
    then F3 is_proper_subformula_of F2 by A6,A7,A11,QC_LANG2:63,XXREAL_0:2;
    hence thesis by QC_LANG2:def 21;
  end;
  L.n = F2 by A1,Def5;
  then
A12: P[0];
  for k holds P[k] from NAT_1:sch 2(A12,A5);
  then ex F3 st F3 = L.(n-l) & F3 is_subformula_of F2 by A4;
  hence thesis;
end;

theorem Th28:
  for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i
  <= len L holds L.i is Element of CQC-WFF(Al)
proof
  let L be PATH of F1,p;
  set n = len L;
  assume that
A1: F1 is_subformula_of p and
A2: 1 <= i and
A3: i <= n;
  n+1 <= n+i by A2,XREAL_1:6;
  then n+1+(-1) <= n+i+(-1) by XREAL_1:6;
  then
A4: n+(-i) <= n-1+i+(-i) by XREAL_1:6;
  i+(-i) <= n+(-i) by A3,XREAL_1:6;
  then reconsider l = n-i as Element of NAT by INT_1:3;
  defpred P[Nat] means $1 <= n-1 implies L.(n-$1) is Element of
  CQC-WFF(Al);
A5: for k st P[k] holds P[k+1]
  proof
    let k such that
A6: P[k];
    assume
A7: k+1 <= n-1;
    then k+1+1 <= n-1+1 by XREAL_1:6;
    then
A8: 2+k+(-k) <= n+(-k) by XREAL_1:6;
    then reconsider j = n-k as Element of NAT by INT_1:3;
    k < k+1 by NAT_1:13;
    then reconsider q = L.j as Element of CQC-WFF(Al) by A6,A7,XXREAL_0:2;
    n <= n+k by NAT_1:11;
    then n+(-k) <= n+k+(-k) by XREAL_1:6;
    then
A9: j-1 < n by XREAL_1:146,XXREAL_0:2;
A10: 1+1+(-1) <= j+(-1) by A8,XREAL_1:6;
    then reconsider j1 = j-1 as Element of NAT by INT_1:3;
    j1+1 = j;
    then consider G1,H1 being Element of QC-WFF(Al) such that
A11: L.j1 = G1 and
A12: q = H1 & G1 is_immediate_constituent_of H1 by A1,A10,A9,Def5;
A13: (ex F being Element of QC-WFF(Al) st q = G1 '&' F) implies thesis by A11,
CQC_LANG:9;
A14: (ex x st q = All(x,G1)) implies thesis by A11,CQC_LANG:13;
A15: (ex F being Element of QC-WFF(Al) st q = F '&' G1) implies thesis by A11,
CQC_LANG:9;
    q = 'not' G1 implies thesis by A11,CQC_LANG:8;
    hence thesis by A12,A13,A15,A14,QC_LANG2:def 19;
  end;
A16: P[0] by A1,Def5;
  for k holds P[k] from NAT_1:sch 2(A16,A5);
  then L.(n-l) is Element of CQC-WFF(Al) by A4;
  hence thesis;
end;

theorem Th29:
  for L being PATH of q,p st QuantNbr(p) <= n & q is_subformula_of
  p & 1 <= i & i <= len L holds ex r st r = L.i & QuantNbr(r) <= n
proof
  let L be PATH of q,p;
  set m = len L;
  assume that
A1: QuantNbr(p) <= n and
A2: q is_subformula_of p and
A3: 1 <= i and
A4: i <= m;
  i+(-i) <= m+(-i) by A4,XREAL_1:6;
  then reconsider l = m-i as Element of NAT by INT_1:3;
  m+1 <= m+i by A3,XREAL_1:6;
  then m+1+(-1) <= m+i+(-1) by XREAL_1:6;
  then
A5: m+(-i) <= m-1+i+(-i) by XREAL_1:6;
  defpred P[Nat] means $1 <= m-1 implies ex r st r = L.(m-$1) &
  QuantNbr(r) <= n;
A6: for k st P[k] holds P[k+1]
  proof
    let k such that
A7: P[k];
    assume
A8: k+1 <= m-1;
    then k+1+1 <= m-1+1 by XREAL_1:6;
    then
A9: 2+k+(-k) <= m+(-k) by XREAL_1:6;
    then reconsider j = m-k as Element of NAT by INT_1:3;
A10: 1+1+(-1) <= j+(-1) by A9,XREAL_1:6;
    then reconsider j1 = j-1 as Element of NAT by INT_1:3;
    m <= m+k by NAT_1:11;
    then m+(-k) <= m+k+(-k) by XREAL_1:6;
    then
A11: j-1 < m by XREAL_1:146,XXREAL_0:2;
    j1+1 = j;
    then consider G1,H1 being Element of QC-WFF(Al) such that
A12: L.j1 = G1 and
A13: L.j = H1 & G1 is_immediate_constituent_of H1 by A2,A10,A11,Def5;
    reconsider r = G1 as Element of CQC-WFF(Al) by A2,A10,A11,A12,Th28;
    k < k+1 by NAT_1:13;
    then consider q such that
A14: q = L.j and
A15: QuantNbr(q) <= n by A7,A8,XXREAL_0:2;
A16: now
      given x such that
A17:  q = All(x,G1);
      take r;
      QuantNbr(r)+1 <= n by A15,A17,CQC_SIM1:18;
      then QuantNbr(r) <= n by NAT_1:13;
      hence thesis by A12;
    end;
A18: now
      given F being Element of QC-WFF(Al) such that
A19:  q = F '&' G1;
      reconsider F as Element of CQC-WFF(Al) by A19,CQC_LANG:9;
      take r;
      n <= n+QuantNbr(F) by NAT_1:11;
      then
A20:  n+(-QuantNbr(F)) <= n+QuantNbr(F)+(-QuantNbr(F)) by XREAL_1:6;
      QuantNbr(r) + QuantNbr(F) <= n by A15,A19,CQC_SIM1:17;
      then QuantNbr(r) + QuantNbr(F)+(-QuantNbr(F)) <= n +(-QuantNbr(F)) by
XREAL_1:6;
      hence thesis by A12,A20,XXREAL_0:2;
    end;
A21: now
      given F being Element of QC-WFF(Al) such that
A22:  q = G1 '&' F;
      reconsider F as Element of CQC-WFF(Al) by A22,CQC_LANG:9;
      take r;
      n <= n+QuantNbr(F) by NAT_1:11;
      then
A23:  n+(-QuantNbr(F)) <= n+QuantNbr(F)+(-QuantNbr(F)) by XREAL_1:6;
      QuantNbr(r) + QuantNbr(F) <= n by A15,A22,CQC_SIM1:17;
      then QuantNbr(r) + QuantNbr(F)+(-QuantNbr(F)) <= n +(-QuantNbr(F)) by
XREAL_1:6;
      hence thesis by A12,A23,XXREAL_0:2;
    end;
    now
      assume
A24:  q = 'not' G1;
      take r;
      QuantNbr(r) <= n by A15,A24,CQC_SIM1:16;
      hence thesis by A12;
    end;
    hence thesis by A14,A13,A21,A18,A16,QC_LANG2:def 19;
  end;
  L.m = p by A2,Def5;
  then
A25: P[0] by A1;
  for k holds P[k] from NAT_1:sch 2(A25,A6);
  then ex r st r = L.(m-l) & QuantNbr(r) <= n by A5;
  hence thesis;
end;

theorem
  QuantNbr(p) = n & q is_subformula_of p implies QuantNbr(q) <= n
proof
  set L =the  PATH of q,p;
  set m = len L;
  assume that
A1: QuantNbr(p) = n and
A2: q is_subformula_of p;
  1 <= m by A2,Def5;
  then ex r st r = L.1 & QuantNbr(r) <= n by A1,A2,Th29;
  hence thesis by A2,Def5;
end;

theorem
  for n,p st (for q st q is_subformula_of p holds QuantNbr(q) = n) holds n = 0
proof
  let n,p such that
A1: for q st q is_subformula_of p holds QuantNbr(q) = n;
  defpred P[Element of CQC-WFF(Al)] means
   $1 is_subformula_of p implies QuantNbr($1) = 0;
A2: for x, r st P[r] holds P[All(x, r)]
  proof
    let x,r such that
    P[r];
    now
      assume
A3:   All(x, r) is_subformula_of p;
      r is_immediate_constituent_of All(x,r) by QC_LANG2:46;
      then r is_proper_subformula_of p by A3,QC_LANG2:63;
      then r is_subformula_of p by QC_LANG2:def 21;
      then
A4:   QuantNbr(r) = n by A1;
      QuantNbr(All(x,r)) = n by A1,A3;
      then n+(-n) = 1+n+(-n) by A4,CQC_SIM1:18;
      hence contradiction;
    end;
    hence thesis;
  end;
A5: for r,s st P[r] & P[s] holds P[r '&' s]
  proof
    let r,s such that
A6: ( P[r])& P[s];
    assume
A7: r '&' s is_subformula_of p;
    s is_immediate_constituent_of r '&' s by QC_LANG2:45;
    then
A8: s is_proper_subformula_of p by A7,QC_LANG2:63;
    r is_immediate_constituent_of r '&' s by QC_LANG2:45;
    then r is_proper_subformula_of p by A7,QC_LANG2:63;
    then QuantNbr(r '&' s) = 0+0 by A6,A8,CQC_SIM1:17,QC_LANG2:def 21;
    hence thesis;
  end;
  for r st P[r] holds P['not' r]
  proof
    let r such that
A9: P[r];
A10: r is_immediate_constituent_of 'not' r by QC_LANG2:43;
    assume 'not' r is_subformula_of p;
    then r is_proper_subformula_of p by A10,QC_LANG2:63;
    hence thesis by A9,CQC_SIM1:16,QC_LANG2:def 21;
  end;
  then
A11: for r,s,x,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)]) by A5,A2,CQC_SIM1:14,15;
A12: for r holds P[r] from CQC_LANG:sch 1(A11);
  QuantNbr(p) = n by A1;
  hence thesis by A12;
end;

theorem
  for p st (for q st q is_subformula_of p holds for x,r holds q <> All(x
  ,r)) holds QuantNbr(p) = 0
proof
  let p such that
A1: for q st q is_subformula_of p holds for x,r holds q <> All(x,r);
  defpred P[Element of CQC-WFF(Al)] means $1 is_subformula_of p
implies QuantNbr($1) = 0;
A2: for r,s st P[r] & P[s] holds P[r '&' s]
  proof
    let r,s such that
A3: ( P[r])& P[s];
    assume
A4: r '&' s is_subformula_of p;
    s is_immediate_constituent_of r '&' s by QC_LANG2:45;
    then
A5: s is_proper_subformula_of p by A4,QC_LANG2:63;
    r is_immediate_constituent_of r '&' s by QC_LANG2:45;
    then r is_proper_subformula_of p by A4,QC_LANG2:63;
    then QuantNbr(r '&' s) = 0+0 by A3,A5,CQC_SIM1:17,QC_LANG2:def 21;
    hence thesis;
  end;
  for r st P[r] holds P['not' r]
  proof
    let r such that
A6: P[r];
A7: r is_immediate_constituent_of 'not' r by QC_LANG2:43;
    assume 'not' r is_subformula_of p;
    then r is_proper_subformula_of p by A7,QC_LANG2:63;
    hence thesis by A6,CQC_SIM1:16,QC_LANG2:def 21;
  end;
  then
A8: for r,s,x,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)]) by A1,A2,CQC_SIM1:14,15;
  for r holds P[r] from CQC_LANG:sch 1(A8);
  hence thesis;
end;

theorem Th33:
  for p st for q st q is_subformula_of p holds QuantNbr(q) <> 1
  holds QuantNbr(p) = 0
proof
  let p such that
A1: for q st q is_subformula_of p holds QuantNbr(q) <> 1;
  defpred P[Element of CQC-WFF(Al)] means $1 is_subformula_of p
implies QuantNbr($1) = 0;
A2: for x, r st P[r] holds P[All(x, r)]
  proof
    let x,r such that
A3: P[r];
    now
      assume
A4:   All(x, r) is_subformula_of p;
      r is_immediate_constituent_of All(x,r) by QC_LANG2:46;
      then r is_proper_subformula_of p by A4,QC_LANG2:63;
      then QuantNbr(All(x,r)) = 0+1 by A3,CQC_SIM1:18,QC_LANG2:def 21;
      hence contradiction by A1,A4;
    end;
    hence thesis;
  end;
A5: for r,s st P[r] & P[s] holds P[r '&' s]
  proof
    let r,s such that
A6: ( P[r])& P[s];
    assume
A7: r '&' s is_subformula_of p;
    s is_immediate_constituent_of r '&' s by QC_LANG2:45;
    then
A8: s is_proper_subformula_of p by A7,QC_LANG2:63;
    r is_immediate_constituent_of r '&' s by QC_LANG2:45;
    then r is_proper_subformula_of p by A7,QC_LANG2:63;
    then QuantNbr(r '&' s) = 0+0 by A6,A8,CQC_SIM1:17,QC_LANG2:def 21;
    hence thesis;
  end;
  for r st P[r] holds P['not' r]
  proof
    let r such that
A9: P[r];
A10: r is_immediate_constituent_of 'not' r by QC_LANG2:43;
    assume 'not' r is_subformula_of p;
    then r is_proper_subformula_of p by A10,QC_LANG2:63;
    hence thesis by A9,CQC_SIM1:16,QC_LANG2:def 21;
  end;
  then
A11: for r,s,x,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)]) by A5,A2,CQC_SIM1:14,15;
  for r holds P[r] from CQC_LANG:sch 1(A11);
  hence thesis;
end;

theorem
  1 <= QuantNbr(p) implies ex q st q is_subformula_of p & QuantNbr(q)=1
  by Th33;