:: A First Order Language
::  by Piotr Rudnicki and Andrzej Trybulec
::
:: Received August 8, 1989
:: Copyright (c) 1990-2019 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, XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI, XXREAL_0,
      MARGREL1, MCART_1, ARYTM_3, NAT_1, FINSEQ_1, RELAT_1, ORDINAL4, CARD_1,
      REALSET1, XBOOLEAN, BVFUNC_2, ZF_LANG, CLASSES2, FUNCT_1, FUNCOP_1,
      RCOMP_1, QC_LANG1, WELLORD1, RELAT_2, MEMBER_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1,
      ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, MCART_1, RELAT_1, FUNCT_1,
      RELSET_1, NAT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, WELLORD1, WELLORD2,
      RELAT_2;
 constructors ENUMSET1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, RELSET_1,
      WELLORD1, WELLORD2, RELAT_2, XTUPLE_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0,
      FINSEQ_1, CARD_1, XTUPLE_0, NAT_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, CARD_1;
 equalities FINSEQ_1;
 expansions TARSKI, XBOOLE_0, FINSEQ_1;
 theorems ZFMISC_1, SUBSET_1, TARSKI, FINSEQ_1, MCART_1, NAT_1, FUNCT_1,
      FUNCT_2, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, XXREAL_0, ORDINAL1,
      CARD_1, RELAT_1, WELLORD1, WELLORD2, RELAT_2, ORDERS_1;
 schemes NAT_1, FUNCT_2, CLASSES1, XBOOLE_0;

begin :: Preliminaries

theorem
  for D1 being non empty set, D2 being set, k being Element of D1 holds
  [: {k}, D2 :] c= [: D1, D2 :]
proof
  let D1 be non empty set, D2 be set, k be Element of D1;
  {k} is Subset of D1 by SUBSET_1:41;
  hence thesis by ZFMISC_1:95;
end;

theorem
  for D1 being non empty set, D2 being set, k1, k2, k3 being
  Element of D1 holds [: {k1, k2, k3}, D2 :] c= [: D1, D2 :]
proof
  let D1 be non empty set, D2 be set, k1, k2, k3 be Element of D1;
  {k1, k2, k3} is Subset of D1 by SUBSET_1:35;
  hence thesis by ZFMISC_1:95;
end;

definition
  mode QC-alphabet -> set means :Def1:
  it is non empty set & ex X being set st NAT c= X & it = [: NAT, X :];
  existence
  proof
    [: NAT, NAT :] = [: NAT, NAT :];
    hence thesis;
  end;
end;

registration
  cluster -> non empty Relation-like for QC-alphabet;
coherence
  proof
    let A be QC-alphabet;
    ex X being set st NAT c= X & A = [: NAT, X :] by Def1;
    hence thesis by Def1;
  end;
end;

reserve A for QC-alphabet;
reserve k,n,m for Nat;

definition
  let A be QC-alphabet;
  func QC-symbols(A) -> non empty set equals
    rng A;
  coherence;
end;

definition let A be QC-alphabet;
  mode QC-symbol of A is Element of QC-symbols(A);
end;

theorem Th3: NAT c= QC-symbols(A) & 0 in QC-symbols(A)
proof
    consider X being set such that A1: NAT c= X & A = [: NAT, X :] by Def1;
    thus A2: NAT c= QC-symbols(A) by A1,RELAT_1:160;
    thus 0 in QC-symbols(A) by A2;
end;

registration let A be QC-alphabet;
  cluster QC-symbols(A) -> non empty;
  coherence;
end;

definition let A be QC-alphabet;
  func QC-variables(A) -> set equals
    [: {6}, NAT :] \/ [: {4,5}, QC-symbols(A) :];
  coherence;
end;

registration
  let A be QC-alphabet;
  cluster QC-variables(A) -> non empty;
  coherence;
end;

Lm1: [: {4}, QC-symbols(A) :] c= QC-variables(A) &
     [: {5}, QC-symbols(A) :] c= QC-variables(A) &
     [: {6}, NAT :] c= QC-variables(A)
proof
  {5} c= {4,5} by ZFMISC_1:7;
  then
A1: [: {5}, QC-symbols(A) :] c= [: {4,5}, QC-symbols(A) :] by ZFMISC_1:96;
  {4} c= {4,5} by ZFMISC_1:7;
  then [: {4}, QC-symbols(A) :] c= [: {4,5}, QC-symbols(A) :] by ZFMISC_1:96;
  hence thesis by A1,XBOOLE_1:10;
end;

theorem Th4:
  QC-variables(A) c= [: NAT, QC-symbols(A) :]
proof
  { 6 } c= NAT & NAT c= QC-symbols(A) by Th3,ZFMISC_1:31;
  then
A1: [: { 6 }, NAT :] c= [: NAT, QC-symbols(A) :] by ZFMISC_1:96;
  {4, 5} c= NAT & QC-symbols(A) c= QC-symbols(A) by ZFMISC_1:32;
  then [: {4,5}, QC-symbols(A) :] c= [: NAT, QC-symbols(A) :] by ZFMISC_1:96;
  hence thesis by A1,XBOOLE_1:8;
end;

definition
  let A be QC-alphabet;
  mode QC-variable of A is Element of QC-variables(A);
  func bound_QC-variables(A) -> Subset of QC-variables(A) equals
  [: {4}, QC-symbols(A) :];
  coherence by Lm1;
  func fixed_QC-variables(A) -> Subset of QC-variables(A) equals
  [: {5}, QC-symbols(A) :];
  coherence by Lm1;
  func free_QC-variables(A) -> Subset of QC-variables(A) equals
  [: {6}, NAT :];
  coherence by Lm1;
  func QC-pred_symbols(A) -> set equals
  { [n, x] where x is QC-symbol of A : 7 <= n };
  coherence;
end;

registration
  let A be QC-alphabet;
  cluster bound_QC-variables(A) -> non empty;
  coherence;
  cluster fixed_QC-variables(A) -> non empty;
  coherence;
  cluster free_QC-variables(A) -> non empty;
  coherence;
  cluster QC-pred_symbols(A) -> non empty;
  coherence
  proof
    0 is QC-symbol of A by Th3;
    then [7, 0] in { [n, x] where x is QC-symbol of A: 7 <= n };
    hence thesis;
  end;
end;

theorem
  A = [: NAT, QC-symbols(A) :]
proof
  consider X being set such that A1: NAT c= X & A = [: NAT, X :] by Def1;
  X <> {} by A1;
  hence A = [: NAT, QC-symbols(A) :] by A1,RELAT_1:160;
end;

theorem Th6:
  QC-pred_symbols(A) c= [: NAT, QC-symbols(A) :]
proof
  let y be object;
  assume y in QC-pred_symbols(A);
  then consider k being Nat, x being QC-symbol of A such that
A1:  y = [k, x] & 7 <= k;
   k in NAT by ORDINAL1:def 12;
  hence thesis by ZFMISC_1:def 2,A1;
end;

definition
  let A be QC-alphabet;
  mode QC-pred_symbol of A is Element of QC-pred_symbols(A);
end;

definition
  let A be QC-alphabet;
  let P be Element of QC-pred_symbols(A);
  func the_arity_of P -> Nat means
  :Def8:
  P`1 = 7+it;
  existence
  proof
    P in {[k, x] where x is QC-symbol of A : 7 <= k};
    then consider k being Nat, x being QC-symbol of A such that
A1: P = [k, x] and
A2: 7 <= k;
    consider w being Nat such that
A3: k=7+w by A2,NAT_1:10;
    thus thesis by A1,A3;
  end;
  uniqueness;
end;

reserve P for QC-pred_symbol of A;

definition
  let A,k;
  func k-ary_QC-pred_symbols(A) -> Subset of QC-pred_symbols(A) equals
  { P : the_arity_of P = k };
  coherence
  proof
    set Y = {7+k};
    [: {7+k}, QC-symbols(A) :] c= QC-pred_symbols(A)
    proof
      let y be object;
      assume
A1:   y in [: {7+k}, QC-symbols(A) :];
      reconsider y1 = y`1 as Nat by MCART_1:12,A1;
      reconsider y2 = y`2 as QC-symbol of A by A1,MCART_1:12;
      y`1 = 7+k by A1,MCART_1:12;
      then 7 <= y1 by NAT_1:12;
      then [y1, y2] in { [m, x] where x is QC-symbol of A : 7 <= m };
      hence thesis by A1,MCART_1:21;
    end;
    then reconsider X = [: Y, QC-symbols(A) :] as Subset of QC-pred_symbols(A);
    X = { P : the_arity_of P = k }
    proof
      thus X c= { P : the_arity_of P = k }
      proof
        let x be object;
        assume
A2:     x in X;
        then reconsider Q = x as QC-pred_symbol of A;
        x`1 in Y by A2,MCART_1:10;
        then x`1 = 7+k by TARSKI:def 1;
        then the_arity_of Q = k by Def8;
        hence thesis;
      end;
      let x be object;
      assume x in { P : the_arity_of P = k };
      then consider P such that
A3:   x = P and
A4:   the_arity_of P = k;
      P`1 = 7+k by A4,Def8;
      then
A5:   P`1 in Y by TARSKI:def 1;
A6:   QC-pred_symbols(A) c= [: NAT, QC-symbols(A) :] by Th6;
      then P in [: NAT, QC-symbols(A) :];
      then P`2 in QC-symbols(A) by MCART_1:10;
      then [P`1, P`2] in X by A5,ZFMISC_1:87;
      hence thesis by A3,A6,MCART_1:21;
    end;
    hence thesis;
  end;
end;

registration
  let k, A;
  cluster k-ary_QC-pred_symbols(A) -> non empty;
  coherence
  proof
    set Y = {7+k};
    [: {7+k}, QC-symbols(A) :] c= QC-pred_symbols(A)
    proof
      let x be object;
      assume
A1:   x in [: {7+k}, QC-symbols(A) :];
      reconsider x1 = x`1 as Nat by MCART_1:12,A1;
      reconsider x2 = x`2 as QC-symbol of A by A1,MCART_1:12;
      x`1 = 7+k by A1,MCART_1:12;
      then 7 <= x1 by NAT_1:12;
      then [x1, x2] in { [m, y] where y is QC-symbol of A : 7 <= m };
      hence thesis by A1,MCART_1:21;
    end;
    then reconsider X = [: Y, QC-symbols(A) :] as
         non empty Subset of QC-pred_symbols(A);
    X = { P : the_arity_of P = k }
    proof
      thus X c= { P : the_arity_of P = k }
      proof
        let x be object;
        assume
A2:     x in X;
        then reconsider Q = x as QC-pred_symbol of A;
        x`1 in Y by A2,MCART_1:10;
        then x`1 = 7+k by TARSKI:def 1;
        then the_arity_of Q = k by Def8;
        hence thesis;
      end;
      let x be object;
      assume x in { P : the_arity_of P = k };
      then consider P such that
A3:   x = P and
A4:   the_arity_of P = k;
      P`1 = 7+k by A4,Def8;
      then
A5:   P`1 in Y by TARSKI:def 1;
A6:   QC-pred_symbols(A) c= [: NAT, QC-symbols(A) :] by Th6;
      then P in [: NAT, QC-symbols(A) :];
      then P`2 in QC-symbols(A) by MCART_1:10;
      then [P`1, P`2] in X by A5,ZFMISC_1:87;
      hence thesis by A3,A6,MCART_1:21;
    end;
    hence thesis;
  end;
end;

definition
  let A be QC-alphabet;
  mode bound_QC-variable of A is Element of bound_QC-variables(A);
  mode fixed_QC-variable of A is Element of fixed_QC-variables(A);
  mode free_QC-variable of A is Element of free_QC-variables(A);
  let k;
  mode QC-pred_symbol of k, A is Element of k-ary_QC-pred_symbols(A);
end;

registration
  let k be Nat;
  let A be QC-alphabet;
  cluster k-element for FinSequence of QC-variables(A);
  existence
  proof
    consider p being FinSequence of QC-variables(A) such that
A1: len p = k by FINSEQ_1:19;
    take p;
    thus len p = k by A1;
  end;
end;

definition
  let k be Nat;
  let A be QC-alphabet;
  mode QC-variable_list of k, A is k-element FinSequence of QC-variables(A);
end;

definition
  let A be QC-alphabet;
  let D be set;
  attr D is A-closed means
  :Def10:
   D is Subset of [:NAT, QC-symbols(A):]* &  :: Includes atomic formulae
  (for k being Nat, p being (QC-pred_symbol of k,A),
  ll being QC-variable_list of k,A holds <*p*>^ll in D) &

:: Is closed under VERUM, 'not', '&', and quantification
  <*[0, 0]*> in D &
  (for p being FinSequence of [:NAT,QC-symbols(A):]
    st p in D holds <*[1, 0]*>^p in D) &
  (for p, q being FinSequence of [:NAT, QC-symbols(A):] st p in D &
    q in D holds <*[2, 0]*>^p^q in D) &
  (for x being bound_QC-variable of A,
    p being FinSequence of [:NAT, QC-symbols(A):]
    st p in D holds <*[3, 0]*>^<*x*>^p in D);
end;

Lm2: for k being Nat, x being QC-symbol of A
     holds <*[k, x]*> is FinSequence of [:NAT, QC-symbols(A):]
proof
  let k;
  let x be QC-symbol of A;
  k in NAT by ORDINAL1:def 12;
  then [k, x] in [:NAT, QC-symbols(A):] by ZFMISC_1:def 2;
  then rng <*[k, x]*> = {[k, x]} &
       {[k, x]} c= [:NAT, QC-symbols(A):] by FINSEQ_1:39,ZFMISC_1:31;
  hence thesis by FINSEQ_1:def 4;
end;

Lm3: for k being Nat, p being (QC-pred_symbol of k,A), ll being (
QC-variable_list of k,A) holds <*p*>^ll is FinSequence of [:NAT,QC-symbols(A):]
proof
  let k be Nat, p be (QC-pred_symbol of k,A),
     ll be QC-variable_list of k,A;
  QC-variables(A) c= [:NAT,QC-symbols(A):] by Th4;
  then
A1: rng ll c= [:NAT,QC-symbols(A):];
  QC-pred_symbols(A) c= [:NAT,QC-symbols(A):] by Th6;
  then k-ary_QC-pred_symbols(A) c= [:NAT,QC-symbols(A):];
  then rng <*p*> c= [:NAT,QC-symbols(A):];
  then rng <*p*> \/ rng ll c= [:NAT,QC-symbols(A):] by A1,XBOOLE_1:8;
  then rng (<*p*>^ll) c= [:NAT,QC-symbols(A):] by FINSEQ_1:31;
  hence thesis by FINSEQ_1:def 4;
end;

Lm4: for x being bound_QC-variable of A,
     p being FinSequence of [:NAT, QC-symbols(A):] holds
<*[3, 0]*>^<*x*>^p is FinSequence of [:NAT, QC-symbols(A):]
proof
  A1: 0 is QC-symbol of A by Th3;
  reconsider y = <*[3, 0]*> as FinSequence of [:NAT,QC-symbols(A):] by A1,Lm2;
  let x be bound_QC-variable of A, p be FinSequence of [:NAT, QC-symbols(A):];
  QC-variables(A) c= [: NAT, QC-symbols(A) :] by Th4;
  then bound_QC-variables(A) c= [:NAT,QC-symbols(A):];
  then rng <*x*> c= [:NAT,QC-symbols(A):];
  then reconsider z = <*x*> as FinSequence of
       [:NAT, QC-symbols(A):] by FINSEQ_1:def 4;
  y^z^p is FinSequence of [:NAT, QC-symbols(A):];
  hence thesis;
end;

definition
  let A be QC-alphabet;
  func QC-WFF(A) -> non empty set means
  :Def11:
  it is A-closed & for D being non empty set st D is A-closed holds it c= D;
  existence
  proof
    0 is QC-symbol of A by Th3;
    then <*[0, 0]*> is FinSequence of [:NAT, QC-symbols(A):] by Lm2;
    then
A1: <*[0, 0]*> in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
    defpred P[object] means
      for D being non empty set st D is A-closed holds $1
    in D;
    consider D0 being set such that
A2: for x being object holds x in D0 iff x in [:NAT, QC-symbols(A):]* & P[x]
     from
    XBOOLE_0:sch 1;
A3: for D being non empty set st D is A-closed holds <*[0, 0]*> in D;
    then reconsider D0 as non empty set by A2,A1;
    take D0;
    D0 c= [:NAT, QC-symbols(A):]*
    by A2;
    hence D0 is Subset of [:NAT, QC-symbols(A):]*;
    thus for k being Nat, p being (QC-pred_symbol of k,A), ll being
    QC-variable_list of k,A holds <*p*>^ll in D0
    proof
      let k be Nat, p be (QC-pred_symbol of k,A), ll be
      QC-variable_list of k,A;
      <*p*>^ll is FinSequence of [:NAT, QC-symbols(A):] by Lm3;
      then
A4:   <*p*>^ll in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
      for D being non empty set st D is A-closed holds <*p*>^ll in D;
      hence thesis by A2,A4;
    end;
    thus <*[0, 0]*> in D0 by A2,A1,A3;
    thus for p being FinSequence of [:NAT, QC-symbols(A):]
         st p in D0 holds <*[1, 0]*>^p
    in D0
    proof
      A5: 0 is QC-symbol of A by Th3;
      reconsider h = <*[1, 0]*> as
                 FinSequence of [:NAT, QC-symbols(A):] by Lm2,A5;
      let p be FinSequence of [:NAT, QC-symbols(A):];
      assume
A6:   p in D0;
A7:   for D being non empty set st D is A-closed holds <*[1, 0]*>^p in D
      proof
        let D be non empty set;
        assume
A8:     D is A-closed;
        then p in D by A2,A6;
        hence thesis by A8;
      end;
      h^p is FinSequence of [:NAT, QC-symbols(A):];
      then <*[1, 0]*>^p in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
      hence thesis by A2,A7;
    end;
    thus for p, q being FinSequence of [:NAT, QC-symbols(A):]
         st p in D0 & q in D0 holds
    <*[2, 0]*>^p^q in D0
    proof
      A9: 0 is QC-symbol of A by Th3;
      reconsider h = <*[2, 0]*> as FinSequence
                 of [:NAT, QC-symbols(A):] by A9,Lm2;
      let p, q be FinSequence of [:NAT, QC-symbols(A):] such that
A10:   p in D0 & q in D0;
A11:   for D being non empty set st D is A-closed holds <*[2, 0]*>^p^q in D
      proof
        let D be non empty set;
        assume
A12:    D is A-closed;
        then p in D & q in D by A2,A10;
        hence thesis by A12;
      end;
      h^p^q is FinSequence of [:NAT, QC-symbols(A):];
      then <*[2, 0]*>^p^q in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
      hence thesis by A2,A11;
    end;
    thus for x being bound_QC-variable of A,
         p being FinSequence of [:NAT, QC-symbols(A):] st
    p in D0 holds <*[3, 0]*>^<*x*>^p in D0
    proof
      let x be bound_QC-variable of A,
          p be FinSequence of [:NAT, QC-symbols(A):];
      assume
A13:  p in D0;
A14:  for D being non empty set st D is A-closed holds <*[3, 0]*>^<*x*>^
      p in D
      proof
        let D be non empty set;
        assume
A15:    D is A-closed;
        then p in D by A2,A13;
        hence thesis by A15;
      end;
      <*[3, 0]*>^<*x*>^p is FinSequence of [:NAT, QC-symbols(A):] by Lm4;
      then <*[3, 0]*>^<*x*>^p in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
      hence thesis by A2,A14;
    end;
    let D be non empty set such that
A16: D is A-closed;
    let x be object;
    assume x in D0;
    hence thesis by A2,A16;
  end;
  uniqueness;
end;

theorem
  QC-WFF(A) is A-closed by Def11;

registration
  let A be QC-alphabet;
  cluster A-closed non empty for set;
  existence
  proof
    QC-WFF(A) is A-closed by Def11;
    hence thesis;
  end;
end;

definition
  let A be QC-alphabet;
  mode QC-formula of A is Element of QC-WFF(A);
end;

definition
  let A be QC-alphabet;
  let P be QC-pred_symbol of A;
  let l be FinSequence of QC-variables(A);
  assume
A1: the_arity_of P = len l;
  func P!l -> Element of QC-WFF(A) equals :Def12:
  <*P*>^l;
  coherence
  proof
    set k = len l;
    set QCP = {Q where Q is QC-pred_symbol of A: the_arity_of Q = k };
    P in QCP by A1;
    then reconsider P as QC-pred_symbol of k, A;
    reconsider l as QC-variable_list of k, A by CARD_1:def 7;
    A2: QC-WFF(A) is A-closed non empty set by Def11;
    for D being A-closed non empty set st not contradiction holds
      <*P*>^l in D by Def10;
    hence thesis by A2;
  end;
end;

theorem Th8:
  for k being Nat, p being QC-pred_symbol of k, A, ll be
  QC-variable_list of k, A holds p!ll = <*p*>^ll
proof
  let k be Nat, p be QC-pred_symbol of k, A,
      ll be QC-variable_list of k, A;
  set QCP = {Q where Q is QC-pred_symbol of A: the_arity_of Q = k };
  p in QCP;
  then
A1: ex Q being QC-pred_symbol of A st p = Q & the_arity_of Q = k;
  len ll = k by CARD_1:def 7;
  hence thesis by A1,Def12;
end;

Lm5: QC-WFF(A) is Subset of [:NAT, QC-symbols(A):]*
proof
  A1: QC-WFF(A) is A-closed non empty set by Def11;
  thus thesis by A1,Def10;
end;

definition
  let A be QC-alphabet;
  let p be Element of QC-WFF(A);
  func @p -> FinSequence of [:NAT, QC-symbols(A):] equals
  p;
  coherence
  proof
    QC-WFF(A) is Subset of [:NAT, QC-symbols(A):]* &
    p in QC-WFF(A) by Lm5;
    hence thesis by FINSEQ_1:def 11;
  end;
end;

definition
  let A be QC-alphabet;
  func VERUM(A) -> QC-formula of A equals
  <*[0, 0]*>;
  coherence
  proof
    QC-WFF(A) is A-closed non empty set by Def11;
    hence thesis by Def10;
  end;
  let p be Element of QC-WFF(A);
  func 'not' p -> QC-formula of A equals
  <*[1, 0]*>^@p;
  coherence
  proof
    QC-WFF(A) is A-closed non empty set by Def11;
    hence thesis by Def10;
  end;
  let q be Element of QC-WFF(A);
  func p '&' q -> QC-formula of A equals
  <*[2, 0]*>^@p^@q;
  coherence
  proof
    QC-WFF(A) is A-closed non empty set by Def11;
    hence thesis by Def10;
  end;
end;

definition
  let A be QC-alphabet;
  let x be bound_QC-variable of A, p be Element of QC-WFF(A);
  func All(x, p) -> QC-formula of A equals
  <*[3, 0]*>^<*x*>^@p;
  coherence
  proof
    QC-WFF(A) is A-closed non empty set by Def11;
    hence thesis by Def10;
  end;
end;

reserve F for Element of QC-WFF(A);

scheme
  QCInd { A() -> QC-alphabet, Prop[Element of QC-WFF(A())] }:
          for F being Element of QC-WFF(A()) holds Prop[F]
provided
A1: for k being Nat, P being (QC-pred_symbol of k, A()), ll being
QC-variable_list of k, A() holds Prop[P!ll] and
A2: Prop[VERUM(A())] and
A3: for p being Element of QC-WFF(A()) st Prop[p] holds Prop['not' p] and
A4: for p, q being Element of QC-WFF(A()) st Prop[p] & Prop[q] holds Prop[p
'&' q] and
A5: for x being bound_QC-variable of A(),
    p being Element of QC-WFF(A()) st Prop[p]
    holds Prop[All(x, p)]
proof
  VERUM(A()) in { F where F is Element of QC-WFF(A()) : Prop[F] } by A2;
  then reconsider X = { F where F is Element of QC-WFF(A()) : Prop[F] }
       as non empty set;
A6: for k being Nat, P being (QC-pred_symbol of k, A()), ll being
  QC-variable_list of k,A() holds <*P*>^ll in X
  proof
    let k be Nat, P be (QC-pred_symbol of k, A()), ll be
    QC-variable_list of k, A();
    Prop[P!ll] by A1;
    then P!ll in X;
    hence thesis by Th8;
  end;
A7: for x being bound_QC-variable of A(),
        p being FinSequence of [:NAT, QC-symbols(A()):]
     st p in X holds <*[3, 0]*>^<*x*>^p in X
  proof
    let x be bound_QC-variable of A(),
        p be FinSequence of [:NAT, QC-symbols(A()):];
    assume p in X;
    then consider p9 being Element of QC-WFF(A()) such that
A8: p = p9 and
A9: Prop[p9];
    Prop[All(x, p9)] by A5,A9;
    hence thesis by A8;
  end;
A10: for p, q being FinSequence of [:NAT, QC-symbols(A()):]
      st p in X & q in X holds <*[2, 0]*>^p^q in X
  proof
    let p, q be FinSequence of [:NAT, QC-symbols(A()):];
    assume p in X;
    then consider p9 being Element of QC-WFF(A()) such that
A11: p = p9 and
A12: Prop[p9];
    assume q in X;
    then consider q9 being Element of QC-WFF(A()) such that
A13: q = q9 and
A14: Prop[q9];
    Prop[p9 '&' q9] by A4,A12,A14;
    hence thesis by A11,A13;
  end;
A15: for p being FinSequence of [:NAT, QC-symbols(A()):]
      st p in X holds <*[1, 0]*>^p in X
  proof
    let p be FinSequence of [:NAT, QC-symbols(A()):];
    assume p in X;
    then consider p9 being Element of QC-WFF(A()) such that
A16: p = p9 and
A17: Prop[p9];
    Prop['not' p9] by A3,A17;
    hence thesis by A16;
  end;
  let F9 be Element of QC-WFF(A());
A18: X c= [:NAT, QC-symbols(A()):]*
  proof
    let x be object;
    assume x in X;
    then consider p being Element of QC-WFF(A()) such that
A19: x = p and
    Prop[p];
    p = @p;
    hence thesis by A19,FINSEQ_1:def 11;
  end;
A20: <*[0, 0]*> in X by A2;
  X is A()-closed by A6,A18,A20,A15,A10,A7;
  then QC-WFF(A()) c= X by Def11;
  then F9 in X;
  then ex F99 being Element of QC-WFF(A()) st F9 = F99 & Prop[F99];
  hence thesis;
end;

definition
  let A be QC-alphabet;
  let F be Element of QC-WFF(A);
  attr F is atomic means
  :Def18:
  ex k being Nat, p being (
  QC-pred_symbol of k, A), ll being QC-variable_list of k, A st F = p!ll;
  attr F is negative means
  :Def19:
  ex p being Element of QC-WFF(A) st F = 'not' p;
  attr F is conjunctive means
  :Def20:
  ex p, q being Element of QC-WFF(A) st F = p '&' q;
  attr F is universal means
  :Def21:
  ex x being bound_QC-variable of A,
     p being Element of QC-WFF(A) st F = All(x, p);
end;

theorem Th9:
  for F being Element of QC-WFF(A) holds F = VERUM(A) or F is atomic or
  F is negative or F is conjunctive or F is universal
proof
  defpred P[Element of QC-WFF(A)] means $1 = VERUM(A) or $1 is atomic or $1 is
  negative or $1 is conjunctive or $1 is universal;
A1: P[VERUM(A)];
A2: for p being Element of QC-WFF(A) st P[p] holds P['not' p] by Def19;
A3: for x being bound_QC-variable of A,
        p being Element of QC-WFF(A) st P[p] holds P[All(x, p)] by Def21;
A4: for p, q being Element of QC-WFF(A)
     st P[p] & P[q] holds P[p '&' q] by Def20;
A5: for k being Nat, p being (QC-pred_symbol of k, A), ll being
  QC-variable_list of k,A holds P[p!ll] by Def18;
  thus for F being Element of QC-WFF(A)
             holds P[F] from QCInd (A5, A1, A2, A4, A3);
end;

theorem Th10:
  for F being Element of QC-WFF(A) holds 1 <= len @F
proof
  let F be Element of QC-WFF(A);
  now
    per cases by Th9;
    suppose
      F = VERUM(A);
      hence thesis by FINSEQ_1:39;
    end;
    suppose
      F is atomic;
      then consider
      k being Nat, p being (QC-pred_symbol of k, A), ll being
      QC-variable_list of k, A such that
A1:   F = p!ll;
      @F = <*p*>^ll by A1,Th8;
      then len @F = len <*p*> + len ll by FINSEQ_1:22
        .= 1 + len ll by FINSEQ_1:39;
      hence thesis by NAT_1:11;
    end;
    suppose
      F is negative;
      then consider p being Element of QC-WFF(A) such that
A2:   F = 'not' p;
      len @F = len <*[1, 0]*> + len @p by A2,FINSEQ_1:22
        .= 1 + len @p by FINSEQ_1:39;
      hence thesis by NAT_1:11;
    end;
    suppose
      F is conjunctive;
      then consider p, q being Element of QC-WFF(A) such that
A3:   F = p '&' q;
      @F = <*[2, 0]*>^(@p^@q) by A3,FINSEQ_1:32;
      then len @F = len <*[2, 0]*> + len (@p^@q) by FINSEQ_1:22
        .= 1 + len (@p^@q) by FINSEQ_1:39;
      hence thesis by NAT_1:11;
    end;
    suppose
      F is universal;
      then consider
      x being bound_QC-variable of A, p being Element of QC-WFF(A) such that
A4:   F = All(x, p);
      @F = <*[3, 0]*>^(<*x*>^@p) by A4,FINSEQ_1:32;
      then len @F = len <*[3, 0]*> + len (<*x*>^@p) by FINSEQ_1:22
        .= 1 + len (<*x*>^@p) by FINSEQ_1:39;
      hence thesis by NAT_1:11;
    end;
  end;
  hence thesis;
end;

reserve Q for QC-pred_symbol of A;

theorem Th11:
  for k being Nat, P being QC-pred_symbol of k, A holds
  the_arity_of P = k
proof
  let k be Nat, P be QC-pred_symbol of k, A;
  reconsider P as Element of k-ary_QC-pred_symbols(A);
  P in { Q : the_arity_of Q = k };
  then ex Q st P = Q & the_arity_of Q = k;
  hence thesis;
end;

reserve F, G for (Element of QC-WFF(A)), s for FinSequence;

theorem Th12:
  ((@F.1)`1 = 0 implies F = VERUM(A)) & ((@F.1)`1 = 1 implies F is
  negative) & ((@F.1)`1 = 2 implies F is conjunctive) & ((@F.1)`1 = 3 implies F
  is universal) & ((ex k being Nat
                     st @F.1 is QC-pred_symbol of k, A)
  implies F is atomic)
proof
A1: now
    per cases by Th9;
    case
      F is atomic;
      then consider
      k being Nat, P being (QC-pred_symbol of k, A), ll being
      QC-variable_list of k, A such that
A2:   F = P!ll;
      @F = <*P*>^ll by A2,Th8;
      then @F.1 = P by FINSEQ_1:41;
      hence ex k being Nat st @F.1 is QC-pred_symbol of k, A;
    end;
    case
      F = VERUM(A);
      hence (@F.1)`1 = [0,0]`1 by FINSEQ_1:def 8
        .= 0;
    end;
    case
      F is negative;
      then ex p being Element of QC-WFF(A) st F = 'not' p;
      then @F.1 = [1, 0] by FINSEQ_1:41;
      hence (@F.1)`1 = 1;
    end;
    case
      F is conjunctive;
      then consider p, q being Element of QC-WFF(A) such that
A3:   F = p '&' q;
      @F = <*[2, 0]*>^(@p^@q) by A3,FINSEQ_1:32;
      then @F.1 = [2, 0] by FINSEQ_1:41;
      hence (@F.1)`1 = 2;
    end;
    case
      F is universal;
      then consider
      x being bound_QC-variable of A, p being Element of QC-WFF(A) such that
A4:   F = All(x, p);
      @F = <*[3, 0]*>^(<*x*>^@p) by A4,FINSEQ_1:32;
      then @F.1 = [3, 0] by FINSEQ_1:41;
      hence (@F.1)`1 = 3;
    end;
  end;
  now
    let k be Nat, P be QC-pred_symbol of k, A;
    reconsider P9 = P as QC-pred_symbol of A;
    P9`1 = 7+the_arity_of P9 by Def8;
    hence P`1 <> 0 & P`1 <> 1 & P`1 <> 2 & P`1 <> 3 by NAT_1:11;
  end;
  hence thesis by A1;
end;

theorem Th13:
  @F = @G^s implies @F = @G
proof
  defpred P[set] means for F,G,s st len @F = $1 & @F = @G^s holds @F = @G;
A1: for n being Nat st for k being Nat st k < n holds P[k] holds P[n]
  proof
    let n be Nat such that
A2: for k being Nat st k < n holds for F, G, s st len @F = k & @F = @G
    ^s holds @F = @G;
    let F, G be (Element of QC-WFF(A)), s be FinSequence such that
A3: len @F = n and
A4: @F = @G^s;
    dom @G = Seg len @G & 1 <= len @G by Th10,FINSEQ_1:def 3;
    then 1 in dom @G;
    then
A5: @F.1 = @G.1 by A4,FINSEQ_1:def 7;
A6: len (@G^s) = len @G + len s by FINSEQ_1:22;
    now
      per cases by Th9;
      suppose
A7:     F = VERUM(A);
A8:     1 <= len @G by Th10;
A9:     len @F = 1 by A7,FINSEQ_1:39;
        then len @G <= 1 by A4,A6,NAT_1:11;
        then 1 + 0 = 1 + len s by A4,A6,A9,A8,XXREAL_0:1;
        then s = {};
        hence thesis by A4,FINSEQ_1:34;
      end;
      suppose
        F is atomic;
        then consider
        k being Nat, P being (QC-pred_symbol of k, A), ll
        being QC-variable_list of k, A such that
A10:    F = P!ll;
A11:    @F = <*P*>^ll by A10,Th8;
        then
A12:    @G.1 = P by A5,FINSEQ_1:41;
        then G is atomic by Th12;
        then consider
        k9 being Nat, P9 being (QC-pred_symbol of k9, A), ll9
        being QC-variable_list of k9, A such that
A13:    G = P9!ll9;
A14:    @G = <*P9*>^ll9 by A13,Th8;
        then
A15:    @G.1 = P9 by FINSEQ_1:41;
        then <*P*>^ll = <*P*>^(ll9^s) by A4,A11,A12,A14,FINSEQ_1:32;
        then ll = ll9^s by FINSEQ_1:33;
        then
A16:    len ll + 0 = len ll9 + len s by FINSEQ_1:22;
        len ll9 = k9 by CARD_1:def 7
          .= the_arity_of P by A12,A15,Th11
          .= k by Th11
          .= len ll by CARD_1:def 7;
        then s = {} by A16;
        hence thesis by A4,FINSEQ_1:34;
      end;
      suppose
        F is negative;
        then consider p being Element of QC-WFF(A) such that
A17:    F = 'not' p;
        @F.1 = [1, 0] by A17,FINSEQ_1:41;
        then (@G.1)`1 = 1 by A5;
        then G is negative by Th12;
        then consider p9 being Element of QC-WFF(A) such that
A18:    G = 'not' p9;
        <*[1, 0]*>^@p = <*[1, 0]*>^(@p9^s) by A4,A17,A18,FINSEQ_1:32;
        then
A19:    @p = @p9^s by FINSEQ_1:33;
        len @F = len @p + len <*[1, 0]*> by A17,FINSEQ_1:22
          .= len @p + 1 by FINSEQ_1:40;
        then len @p < len @F by NAT_1:13;
        then @p = @p9 by A2,A3,A19;
        then @p9^{} = @p9^s by A19,FINSEQ_1:34;
        then s = {} by FINSEQ_1:33;
        hence thesis by A4,FINSEQ_1:34;
      end;
      suppose
        F is conjunctive;
        then consider p, q being Element of QC-WFF(A) such that
A20:    F = p '&' q;
A21:    @F = <*[2, 0]*>^(@p^@q) by A20,FINSEQ_1:32;
        then
A22:    len @F = len (@p^@q) + len <*[2, 0]*> by FINSEQ_1:22
          .= len (@p^@q) + 1 by FINSEQ_1:40;
        then
A23:    len @F = len @p + len @q + 1 by FINSEQ_1:22;
        @F.1 = [2, 0] by A21,FINSEQ_1:41;
        then (@G.1)`1 = 2 by A5;
        then G is conjunctive by Th12;
        then consider p9, q9 being Element of QC-WFF(A) such that
A24:    G = p9 '&' q9;
A25:    len @p9 <= len @p9 + len (@q9^s) by NAT_1:11;
A26:    @G = <*[2, 0]*>^(@p9^@q9) by A24,FINSEQ_1:32;
        then <*[2, 0]*>^(@p^@q) = <*[2, 0]*>^(@p9^@q9^s) by A4,A21,FINSEQ_1:32;
        then
A27:    @p^@q = @p9^@q9^s by FINSEQ_1:33
          .= @p9^(@q9^s) by FINSEQ_1:32;
        then len @F = len @p9 + len (@q9^s) + 1 by A22,FINSEQ_1:22;
        then
A28:    len @p9 < len @F by A25,NAT_1:13;
        len @q <= len @p + len @q by NAT_1:11;
        then
A29:    len @q < len @F by A23,NAT_1:13;
        len @p <= len @p + len @q by NAT_1:11;
        then
A30:    len @p < len @F by A23,NAT_1:13;
        len @p <= len @p9 or len @p9 <= len @p;
        then consider a, b, c, d being FinSequence such that
A31:    a = @p & b = @p9 or a = @p9 & b = @p and
A32:    len a <= len b & a^c = b^d by A27;
        ex t being FinSequence st a^t = b by A32,FINSEQ_1:47;
        then
A33:    @p = @p9 by A2,A3,A31,A30,A28;
        then @q = @q9^s by A27,FINSEQ_1:33;
        hence thesis by A2,A3,A21,A26,A33,A29;
      end;
      suppose
        F is universal;
        then consider
        x being bound_QC-variable of A, p being Element of QC-WFF(A) such
        that
A34:    F = All(x, p);
A35:    @F = <*[3, 0]*>^(<*x*>^@p) by A34,FINSEQ_1:32;
        then len @F = len (<*x*>^@p) + len <*[3, 0]*> by FINSEQ_1:22
          .= len (<*x*>^@p) + 1 by FINSEQ_1:40
          .= len <*x*> + len @p + 1 by FINSEQ_1:22
          .= 1 + len @p + 1 by FINSEQ_1:40;
        then len @p + 1 <= len @F by NAT_1:13;
        then
A36:    len @p < len @F by NAT_1:13;
        @F.1 = [3, 0] by A35,FINSEQ_1:41;
        then (@G.1)`1 = 3 by A5;
        then G is universal by Th12;
        then consider
        x9 being bound_QC-variable of A,p9 being Element of QC-WFF(A) such that
A37:    G = All(x9, p9);
        <*[3, 0]*>^<*x*>^@p = <*[3, 0]*>^(<*x9*>^@p9)^s by A4,A34,A37,
FINSEQ_1:32
          .= <*[3, 0]*>^(<*x9*>^@p9^s) by FINSEQ_1:32;
        then
A38:    <*x*>^@p = <*x9*>^@p9^s by A34,A35,FINSEQ_1:33
          .= <*x9*>^(@p9^s) by FINSEQ_1:32;
        then
A39:    x = (<*x9*>^(@p9^s)).1 by FINSEQ_1:41
          .= x9 by FINSEQ_1:41;
        then @p = @p9^s by A38,FINSEQ_1:33;
        hence thesis by A2,A3,A34,A37,A39,A36;
      end;
    end;
    hence thesis;
  end;
A40: for n being Nat holds P[n] from NAT_1:sch 4(A1);
  thus thesis by A40;
end;

definition
  let A be QC-alphabet;
  let F be Element of QC-WFF(A) such that
A1: F is atomic;
  func the_pred_symbol_of F -> QC-pred_symbol of A means
  :Def22:
  ex k being Nat, ll being (QC-variable_list of k, A),
        P being QC-pred_symbol of k, A st it = P
  & F = P!ll;
  existence
  by A1;
  uniqueness
  proof
    let P1, P2 be QC-pred_symbol of A;
    given k1 being Nat, ll1 being (QC-variable_list of k1, A), P19
    being QC-pred_symbol of k1, A such that
A2: P1 = P19 & F = P19!ll1;
    given k2 being Nat, ll2 being (QC-variable_list of k2, A), P29
    being QC-pred_symbol of k2, A such that
A3: P2 = P29 & F = P29!ll2;
A4: <*P1*>^ll1 = F by A2,Th8
      .= <*P2*>^ll2 by A3,Th8;
    thus P1 = (<*P1*>^ll1).1 by FINSEQ_1:41
      .= P2 by A4,FINSEQ_1:41;
  end;
end;

definition
  let A be QC-alphabet;
  let F be Element of QC-WFF(A) such that
A1: F is atomic;
  func the_arguments_of F -> FinSequence of QC-variables(A) means
  :Def23:
  ex k
being Nat, P being (QC-pred_symbol of k, A),
                      ll being QC-variable_list
  of k, A st it = ll & F = P!ll;
  existence
  by A1;
  uniqueness
  proof
    let ll1, ll2 be FinSequence of QC-variables(A);
    given k1 being Nat, P1 being (QC-pred_symbol of k1, A),
          ll19 being
    QC-variable_list of k1, A such that
A2: ll1 = ll19 and
A3: F = P1!ll19;
A4: F = <*P1*>^ll19 by A3,Th8;
    given k2 being Nat, P2 being (QC-pred_symbol of k2, A),
          ll29 being QC-variable_list of k2, A such that
A5: ll2 = ll29 and
A6: F = P2!ll29;
A7: F = <*P2*>^ll29 by A6,Th8;
    P1 = the_pred_symbol_of F by A1,A3,Def22
      .= P2 by A1,A6,Def22;
    hence thesis by A2,A5,A4,A7,FINSEQ_1:33;
  end;
end;

definition
  let A be QC-alphabet;
  let F be Element of QC-WFF(A) such that
A1: F is negative;
  func the_argument_of F -> QC-formula of A means
  :Def24:
  F = 'not' it;
  existence by A1;
  uniqueness by FINSEQ_1:33;
end;

definition
  let A be QC-alphabet;
  let F be Element of QC-WFF(A) such that
A1: F is conjunctive;
  func the_left_argument_of F -> QC-formula of A means
  :Def25:
  ex q being Element of QC-WFF(A) st F = it '&' q;
  existence by A1;
  uniqueness
  proof
    let p1, p2 be QC-formula of A;
    given q1 being Element of QC-WFF(A) such that
A2: F = p1 '&' q1;
    given q2 being Element of QC-WFF(A) such that
A3: F = p2 '&' q2;
    <*[2, 0]*>^(@p1^@q1) = p2 '&' q2 by A2,A3,FINSEQ_1:32
      .= <*[2, 0]*>^(@p2^@q2) by FINSEQ_1:32;
    then
A4: @p1^@q1 = @p2^@q2 by FINSEQ_1:33;
    len @p1 <= len @p2 or len @p2 <= len @p1;
    then consider a, b, c, d being FinSequence such that
A5: a = @p1 & b = @p2 or a = @p2 & b = @p1 and
A6: len a <= len b & a^c = b^d by A4;
    ex t being FinSequence st a^t = b by A6,FINSEQ_1:47;
    hence thesis by A5,Th13;
  end;
end;

definition
  let A be QC-alphabet;
  let F be Element of QC-WFF(A) such that
A1: F is conjunctive;
  func the_right_argument_of F -> QC-formula of A means
  :Def26:
  ex p being Element of QC-WFF(A) st F = p '&' it;
  existence
  by A1;
  uniqueness
  proof
    let q1, q2 be QC-formula of A;
    given p1 being Element of QC-WFF(A) such that
A2: F = p1 '&' q1;
    given p2 being Element of QC-WFF(A) such that
A3: F = p2 '&' q2;
    <*[2, 0]*>^(@p1^@q1) = p2 '&' q2 by A2,A3,FINSEQ_1:32
      .= <*[2, 0]*>^(@p2^@q2) by FINSEQ_1:32;
    then
A4: @p1^@q1 = @p2^@q2 by FINSEQ_1:33;
    p1 = the_left_argument_of F by A1,A2,Def25
      .= p2 by A1,A3,Def25;
    hence thesis by A4,FINSEQ_1:33;
  end;
end;

definition
  let A be QC-alphabet;
  let F be Element of QC-WFF(A) such that
A1: F is universal;
  func bound_in F -> bound_QC-variable of A means
  :Def27:
  ex p being Element of QC-WFF(A) st F = All(it, p);
  existence by A1;
  uniqueness
  proof
    let x1, x2 be bound_QC-variable of A;
    given p1 being Element of QC-WFF(A) such that
A2: F = All(x1, p1);
    given p2 being Element of QC-WFF(A) such that
A3: F = All(x2, p2);
    <*[3, 0]*>^(<*x1*>^@p1) = All(x2, p2) by A2,A3,FINSEQ_1:32
      .= <*[3, 0]*>^(<*x2*>^@p2) by FINSEQ_1:32;
    then
A4: <*x1*>^@p1 = <*x2*>^@p2 by FINSEQ_1:33;
    thus x1 = (<*x1*>^@p1).1 by FINSEQ_1:41
      .= x2 by A4,FINSEQ_1:41;
  end;
  func the_scope_of F -> QC-formula of A means
  :Def28:
  ex x being bound_QC-variable of A st F = All(x, it);
  existence
  by A1;
  uniqueness
  proof
    let p1, p2 be QC-formula of A;
    given x1 being bound_QC-variable of A such that
A5: F = All(x1, p1);
    given x2 being bound_QC-variable of A such that
A6: F = All(x2, p2);
    <*[3, 0]*>^(<*x1*>^@p1) = All(x2, p2) by A5,A6,FINSEQ_1:32
      .= <*[3, 0]*>^(<*x2*>^@p2) by FINSEQ_1:32;
    then
A7: <*x1*>^@p1 = <*x2*>^@p2 by FINSEQ_1:33;
    x1 = (<*x1*>^@p1).1 by FINSEQ_1:41
      .= x2 by A7,FINSEQ_1:41;
    hence thesis by A7,FINSEQ_1:33;
  end;
end;

reserve p for Element of QC-WFF(A);

theorem Th14:
  p is negative implies len @the_argument_of p < len @p
proof
  assume
A1: p is negative;
  then consider q being Element of QC-WFF(A) such that
A2: p = 'not' q;
  len @p = len <*[1, 0]*> + len @q by A2,FINSEQ_1:22
    .= len @q + 1 by FINSEQ_1:40;
  then len @q < len @p by NAT_1:13;
  hence thesis by A1,A2,Def24;
end;

theorem Th15:
  p is conjunctive implies len @the_left_argument_of p < len @p &
  len @the_right_argument_of p < len @p
proof
  assume
A1: p is conjunctive;
  then consider l, q being Element of QC-WFF(A) such that
A2: p = l '&' q;
  p = <*[2, 0]*>^(@l^@q) by A2,FINSEQ_1:32;
  then
A3: len @p = len <*[2, 0]*> + len (@l^@q) by FINSEQ_1:22
    .= len (@l^@q) + 1 by FINSEQ_1:40;
A4: len @q + len @l = len (@l^@q) by FINSEQ_1:22;
  then len @q <= len (@l^@q) by NAT_1:11;
  then
A5: len @q < len @p by A3,NAT_1:13;
  len @l <= len (@l^@q) by A4,NAT_1:11;
  then len @l < len @p by A3,NAT_1:13;
  hence thesis by A1,A2,A5,Def25,Def26;
end;

theorem Th16:
  p is universal implies len @the_scope_of p < len @p
proof
  assume
A1: p is universal;
  then consider x being bound_QC-variable of A, q being Element of QC-WFF(A)
       such that
A2: p = All(x, q);
  len @q + len <*x*> = len (<*x*>^@q) by FINSEQ_1:22;
  then
A3: len @q <= len (<*x*>^@q) by NAT_1:11;
  p = <*[3, 0]*>^(<*x*>^@q) by A2,FINSEQ_1:32;
  then len @p = len <*[3, 0]*> + len (<*x*>^@q) by FINSEQ_1:22
    .= len (<*x*>^@q) + 1 by FINSEQ_1:40;
  then len @q < len @p by A3,NAT_1:13;
  hence thesis by A1,A2,Def28;
end;

scheme
  QCInd2 { A() -> QC-alphabet, P[Element of QC-WFF(A())] }:
    for p being Element of QC-WFF(A()) holds P[p]
provided
A1: for p being Element of QC-WFF(A()) holds (p is atomic implies P[p]) & P[
VERUM(A())] & (p is negative & P[the_argument_of p] implies P[p]) & (p is
conjunctive & P[the_left_argument_of p] & P[the_right_argument_of p] implies P[
p]) & (p is universal & P[the_scope_of p] implies P[p])
proof
A2: now
    let x be bound_QC-variable of A(), p be Element of QC-WFF(A()) such that
A3: P[p];
A4: All(x, p) is universal;
    then p = the_scope_of All(x, p) by Def28;
    hence P[All(x, p)] by A1,A3,A4;
  end;
A5: now
    let p be Element of QC-WFF(A()) such that
A6: P[p];
A7: 'not' p is negative;
    then p= the_argument_of 'not' p by Def24;
    hence P['not' p] by A1,A6,A7;
  end;
A8: now
    let p, q be Element of QC-WFF(A()) such that
A9: ( P[p])& P[q];
A10: p '&' q is conjunctive;
    then
    p = the_left_argument_of (p '&' q) & q = the_right_argument_of (p '&'
    q) by Def25,Def26;
    hence P[p '&' q] by A1,A9,A10;
  end;
A11: for k be Nat, P be (QC-pred_symbol of k, A()), ll be
    QC-variable_list of k, A() holds P[P!ll] by A1,Def18;
A12: P[VERUM(A())] by A1;
  thus for p be Element of QC-WFF(A())
       holds P[p] from QCInd (A11, A12, A5, A8, A2);
end;

reserve F for Element of QC-WFF(A);

theorem Th17:
  for k being Nat, P being QC-pred_symbol of k, A holds P
  `1 <> 0 & P`1 <> 1 & P`1 <> 2 & P`1 <> 3
proof
  let k be Nat, P be QC-pred_symbol of k, A;
  reconsider P9 = P as QC-pred_symbol of A;
  P9`1 = 7+the_arity_of P9 by Def8;
  hence thesis by NAT_1:11;
end;

theorem Th18:
  (@VERUM(A).1)`1 = 0 & (F is atomic implies
   ex k being Nat st @F.1 is QC-pred_symbol of k, A)
  & (F is negative implies (@F.1)`1 = 1) &
(F is conjunctive implies (@F.1)`1 = 2) & (F is universal implies (@F.1)`1 = 3)
proof
  thus (@VERUM(A).1)`1 = [0,0]`1 by FINSEQ_1:def 8
    .= 0;
  thus F is atomic implies ex k being Nat st @F.1 is QC-pred_symbol
  of k, A
  proof
    assume F is atomic;
    then consider
    k being Nat, P being (QC-pred_symbol of k, A), ll being
    QC-variable_list of k, A such that
A1: F = P!ll;
    @F = <*P*>^ll by A1,Th8;
    then @F.1 = P by FINSEQ_1:41;
    hence thesis;
  end;
  thus F is negative implies (@F.1)`1 = 1
  proof
    assume F is negative;
    then ex p being Element of QC-WFF(A) st F = 'not' p;
    then @F.1 = [1, 0] by FINSEQ_1:41;
    hence thesis;
  end;
  thus F is conjunctive implies (@F.1)`1 = 2
  proof
    assume F is conjunctive;
    then consider p, q being Element of QC-WFF(A) such that
A2: F = p '&' q;
    @F = <*[2, 0]*>^(@p^@q) by A2,FINSEQ_1:32;
    then @F.1 = [2, 0] by FINSEQ_1:41;
    hence thesis;
  end;
  thus F is universal implies (@F.1)`1 = 3
  proof
    assume F is universal;
    then consider
    x being bound_QC-variable of A, p being Element of QC-WFF(A) such that
A3: F = All(x, p);
    @F = <*[3, 0]*>^(<*x*>^@p) by A3,FINSEQ_1:32;
    then @F.1 = [3, 0] by FINSEQ_1:41;
    hence thesis;
  end;
end;

theorem Th19:
  F is atomic implies (@F.1)`1 <> 0 & (@F.1)`1 <> 1 & (@F.1)`1 <>
  2 & (@F.1)`1 <> 3
proof
  assume F is atomic;
  then ex k being Nat st @F.1 is QC-pred_symbol of k, A by Th18;
  hence thesis by Th17;
end;

reserve p for Element of QC-WFF(A);

theorem Th20:
  not (VERUM(A) is atomic or VERUM(A) is negative or VERUM(A) is
  conjunctive or VERUM(A) is universal)
  & not (ex p st p is atomic & p is negative
  or p is atomic & p is conjunctive or p is atomic & p is universal or p is
  negative & p is conjunctive or p is negative & p is universal or p is
  conjunctive & p is universal)
proof
  (@VERUM(A).1)`1 = 0 by Th18;
  hence not (VERUM(A) is atomic or VERUM(A)
  is negative or VERUM(A) is conjunctive or
  VERUM(A) is universal) by Th18,Th19;
  let p be Element of QC-WFF(A);
A1: p is conjunctive implies (@p.1)`1 = 2 by Th18;
A2: p is universal implies (@p.1)`1 = 3 by Th18;
  p is negative implies (@p.1)`1 = 1 by Th18;
  hence thesis by A1,A2,Th19;
end;

scheme
  QCFuncEx { Al() -> QC-alphabet, D() -> non empty set,
             V() -> (Element of D()),
             A(Element of QC-WFF(Al())) -> (Element of D()),
             N(Element of D()) -> (Element of D()),
             C((Element of D()), Element of D()) -> (Element of D()),
             Q((Element of QC-WFF(Al())), Element of D()) -> Element of D()} :
        ex F being Function of QC-WFF(Al()), D() st 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))
  proof
  defpred Pfn[Function of QC-WFF(Al()), D(), Nat]
    means $1.VERUM(Al()) = V()
    & for p being Element of QC-WFF(Al()) st len @p <= $2 holds
      (p is atomic implies $1.p = A(p))
    & (p is negative implies $1.p = N($1.the_argument_of p))
    & (p is conjunctive implies $1.p = C($1.the_left_argument_of p,
       $1.the_right_argument_of p))
    & (p is universal implies $1.p = Q(p, $1.the_scope_of p));
  defpred Pfgp[(Element of D()), (Function of QC-WFF(Al()), D()),
               Element of QC-WFF(Al())]
  means ($3 = VERUM(Al()) implies $1 = V())
        & ($3 is atomic implies $1 = A($3))
        & ($3 is negative implies $1 = N($2.the_argument_of $3))
        & ($3 is conjunctive implies $1 = C($2.the_left_argument_of $3,
           $2.the_right_argument_of $3))
        & ($3 is universal implies $1 = Q($3, $2.the_scope_of $3));
  defpred S[Nat] means ex F being Function of QC-WFF(Al()), D()
          st Pfn[F, $1];
  defpred Qfn[object, object] means ex p being Element of QC-WFF(Al())
         st p = $1 & for g being Function of QC-WFF(Al()), D()
                      st Pfn[g, len @p qua Nat] holds $2 = g.p;
A1: for n be Nat st S[n] holds S[n+1]
  proof
    let n be Nat;
    given F being Function of QC-WFF(Al()), D() such that
A2: Pfn[F, n];
    defpred R[Element of QC-WFF(Al()),Element of D()] means
    (len @$1 <> n+1 implies $2 = F.$1) & (len @$1 = n+1 implies Pfgp[$2,F,$1]);
A3: for p be Element of QC-WFF(Al()) ex y be Element of D() st R[p,y]
    proof
      let p be Element of QC-WFF(Al());
      now
        per cases by Th9;
        case
          len @p <> n+1;
          take y = F.p;
          thus y =F.p;
        end;
        case
A4:       len @p = n+1 & p = VERUM(Al());
          take y = V();
          thus Pfgp[y, F, p] by A4,Th20;
        end;
        case
A5:       len @p = n+1 & p is atomic;
          take y = A(p);
          thus Pfgp[y, F, p] by A5,Th20;
        end;
        case
A6:       len @p = n+1 & p is negative;
          take y = N(F.the_argument_of p);
          thus Pfgp[y, F, p] by A6,Th20;
        end;
        case
A7:       len @p = n+1 & p is conjunctive;
          take y = C(F.the_left_argument_of p, F.the_right_argument_of p);
          thus Pfgp[y, F, p] by A7,Th20;
        end;
        case
A8:       len @p = n+1 & p is universal;
          take y = Q(p, F.the_scope_of p);
          thus Pfgp[y, F, p] by A8,Th20;
        end;
      end;
      hence thesis;
    end;
    consider G being Function of QC-WFF(Al()), D() such that
A9: for p being Element of QC-WFF(Al()) holds R[p,G.p] from FUNCT_2:sch 3 (
    A3);
    take H = G;
    thus Pfn[H, n+1]
    proof
      thus H.VERUM(Al()) = V()
      proof
        per cases;
        suppose
          len @VERUM(Al()) <> n+1;
          hence thesis by A2,A9;
        end;
        suppose
          len @VERUM(Al()) = n+1;
          hence thesis by A9;
        end;
      end;
      let p be Element of QC-WFF(Al()) such that
A10:  len @p <= n+1;
      thus p is atomic implies H.p = A(p)
      proof
        now
          per cases;
          suppose
            len @p <> n+1;
            then len @p <= n & H.p = F.p by A9,A10,NAT_1:8;
            hence thesis by A2;
          end;
          suppose
            len @p = n+1;
            hence thesis by A9;
          end;
        end;
        hence thesis;
      end;
      thus p is negative implies H.p = N(H.the_argument_of p)
      proof
        assume
A11:    p is negative;
        then len @the_argument_of p <> n+1 by A10,Th14;
        then
A12:    H.the_argument_of p = F.the_argument_of p by A9;
        now
          per cases;
          suppose
            len @p <> n+1;
            then len @p <= n & H.p = F.p by A9,A10,NAT_1:8;
            hence thesis by A2,A11,A12;
          end;
          suppose
            len @p = n+1;
            hence thesis by A9,A11,A12;
          end;
        end;
        hence thesis;
      end;
      thus p is conjunctive implies H.p = C(H.the_left_argument_of p, H.
      the_right_argument_of p)
      proof
        assume
A13:    p is conjunctive;
        then len @the_right_argument_of p <> n+1 by A10,Th15;
        then
A14:    H.the_right_argument_of p = F.the_right_argument_of p by A9;
        len @the_left_argument_of p <> n+1 by A10,A13,Th15;
        then
A15:    H.the_left_argument_of p = F.the_left_argument_of p by A9;
        now
          per cases;
          suppose
            len @p <> n+1;
            then len @p <= n & H.p = F.p by A9,A10,NAT_1:8;
            hence thesis by A2,A13,A15,A14;
          end;
          suppose
            len @p = n+1;
            hence thesis by A9,A13,A15,A14;
          end;
        end;
        hence thesis;
      end;
      thus p is universal implies H.p = Q(p, H.the_scope_of p)
      proof
        assume
A16:    p is universal;
        then len @the_scope_of p <> n+1 by A10,Th16;
        then
A17:    H.the_scope_of p = F.the_scope_of p by A9;
        now
          per cases;
          suppose
            len @p <> n+1;
            then len @p <= n & H.p = F.p by A9,A10,NAT_1:8;
            hence thesis by A2,A16,A17;
          end;
          suppose
            len @p = n+1;
            hence thesis by A9,A16,A17;
          end;
        end;
        hence thesis;
      end;
    end;
  end;
A18: S[0]
  proof
    reconsider F = QC-WFF(Al()) --> V() as Function of QC-WFF(Al()), D();
    take F;
    thus F.VERUM(Al()) = V() by FUNCOP_1:7;
    let p be Element of QC-WFF(Al()) such that
A19: len @p <= 0;
    1 <= len @p by Th10;
    hence thesis by A19;
  end;
A20: for n being Nat holds S[n] from NAT_1:sch 2(A18, A1);
  then
A21: ex G being Function of QC-WFF(Al()), D()
      st Pfn[G, len @VERUM(Al()) qua Nat];
A22: for x being object st x in QC-WFF(Al()) ex y being object st Qfn[x, y]
  proof
    let x be object;
    assume x in QC-WFF(Al());
    then reconsider x9 = x as Element of QC-WFF(Al());
    consider F being Function of QC-WFF(Al()), D() such that
A23: Pfn[F, len @x9 qua Nat] by A20;
    take F.x, x9;
    thus x = x9;
    let G be Function of QC-WFF(Al()), D() such that
A24: Pfn[G, len @x9 qua Nat];
    defpred Prop[Element of QC-WFF(Al())]
      means len @$1 <= len@x9 implies F.$1 = G.$1;
A25: now
      let p be Element of QC-WFF(Al());
      thus p is atomic implies Prop[p]
      proof
        assume
A26:    p is atomic & len @p <= len@x9;
        hence F.p = A(p) by A23
          .= G.p by A24,A26;
      end;
      thus Prop[VERUM(Al())] by A23,A24;
      thus p is negative & Prop[the_argument_of p] implies Prop[p]
      proof
        assume that
A27:    p is negative and
A28:    Prop[the_argument_of p] and
A29:    len @p <= len @x9;
        len @the_argument_of p < len @p by A27,Th14;
        hence F.p = N(G.the_argument_of p) by A23,A27,A28,A29,XXREAL_0:2
          .= G.p by A24,A27,A29;
      end;
      thus p is conjunctive & Prop[the_left_argument_of p] & Prop[
      the_right_argument_of p] implies Prop[p]
      proof
        assume that
A30:    p is conjunctive and
A31:    ( Prop[the_left_argument_of p])& Prop[the_right_argument_of p ] and
A32:    len @p <= len @x9;
        len @the_left_argument_of p < len @p & len @the_right_argument_of
        p < len @p by A30,Th15;
        hence F.p = C(G.the_left_argument_of p, G.the_right_argument_of p) by
A23,A30,A31,A32,XXREAL_0:2
          .= G.p by A24,A30,A32;
      end;
      thus p is universal & Prop[the_scope_of p] implies Prop[p]
      proof
        assume that
A33:    p is universal and
A34:    Prop[the_scope_of p] and
A35:    len @p <= len @x9;
        len @the_scope_of p < len @p by A33,Th16;
        hence F.p = Q(p, G.the_scope_of p) by A23,A33,A34,A35,XXREAL_0:2
          .= G.p by A24,A33,A35;
      end;
    end;
    for p being Element of QC-WFF(Al()) holds Prop[p] from QCInd2 (A25);
    hence thesis;
  end;
  consider F being Function such that
A36: dom F = QC-WFF(Al()) and
A37: for x being object st x in QC-WFF(Al()) holds Qfn[x, F.x]
from CLASSES1:sch
  1 (A22);
  rng F c= D()
  proof
    let y be object;
    assume y in rng F;
    then consider x being object such that
A38: x in QC-WFF(Al()) & y = F.x by A36,FUNCT_1:def 3;
    consider p being Element of QC-WFF(Al()) such that
    p = x and
A39: for g being Function of QC-WFF(Al()), D() st Pfn[g, len @p qua Element
    of NAT] holds y = g.p by A37,A38;
    consider G being Function of QC-WFF(Al()), D() such that
A40: Pfn[G, len @p qua Nat] by A20;
    y = G.p by A39,A40;
    hence thesis;
  end;
  then reconsider F as Function of QC-WFF(Al()), D()
       by A36,FUNCT_2:def 1,RELSET_1:4;
  take F;
  Qfn[VERUM(Al()), F.VERUM(Al())] by A37;
  hence F.VERUM(Al()) = V() by A21;
  let p be Element of QC-WFF(Al());
  consider p1 being Element of QC-WFF(Al()) such that
A41: p1 = p and
A42: for g being Function of QC-WFF(Al()), D() st Pfn[g, len @p1 qua Element
  of NAT] holds F.p = g.p1 by A37;
  consider G being Function of QC-WFF(Al()), D() such that
A43: Pfn[G, len @p1 qua Nat] by A20;
  set p9 = the_scope_of p;
A44: ex p1 being Element of QC-WFF(Al()) st p1 = p9 & for g being Function of
  QC-WFF(Al()), D() st Pfn[g, len @p1 qua Nat]
  holds F.p9 = g.p1 by A37;
A45: F.p = G.p by A41,A42,A43;
  hence p is atomic implies F.p = A(p) by A41,A43;
A46: for k being Nat st k < len @p holds Pfn[G, k]
  proof
    let k be Nat;
    assume
A47: k < len @p;
    thus G.VERUM(Al()) = V() by A43;
    let p9 be Element of QC-WFF(Al());
    assume len @p9 <= k;
    then len @p9 <= len@p by A47,XXREAL_0:2;
    hence thesis by A41,A43;
  end;
  thus p is negative implies F.p = N(F.the_argument_of p)
  proof
    set p9 = the_argument_of p;
    set k = len @p9;
A48: ex p1 being Element of QC-WFF(Al()) st p1 = p9 & for g being Function of
    QC-WFF(Al()), D() st Pfn[g, len @p1 qua Nat]
    holds F.p9 = g.p1 by A37;
    assume
A49: p is negative;
    then k < len @p by Th14;
    then Pfn[G, k qua Nat] by A46;
    then F.p9 = G.p9 by A48;
    hence thesis by A41,A43,A45,A49;
  end;
  thus p is conjunctive implies F.p = C(F.the_left_argument_of p, F.
  the_right_argument_of p)
  proof
    set p99 = the_right_argument_of p;
    set p9 = the_left_argument_of p;
    set k9 = len @p9;
    set k99 = len @p99;
A50: ex p2 being Element of QC-WFF(Al()) st p2 = p99
        & for g being Function of QC-WFF(Al()), D()
           st Pfn[g, len @p2 qua Nat] holds F.p99 = g.p2 by A37;
    assume
A51: p is conjunctive;
    then k9 < len @p by Th15;
    then
A52: Pfn[G, k9 qua Nat] by A46;
    k99 < len @p by A51,Th15;
    then Pfn[G, k99 qua Nat] by A46;
    then
A53: F.p99 = G.p99 by A50;
    ex p1 being Element of QC-WFF(Al()) st p1 = p9 & for g being Function of
    QC-WFF(Al()), D() st Pfn[g, len @p1 qua Nat]
    holds F.p9 = g.p1 by A37;
    then F.p9 = G.p9 by A52;
    hence thesis by A41,A43,A45,A51,A53;
  end;
  set k = len @p9;
  assume
A54: p is universal;
  then k < len @p by Th16;
  then Pfn[G, k qua Nat] by A46;
  then F.p9 = G.p9 by A44;
  hence thesis by A41,A43,A45,A54;
end;

reserve j,k for Nat;

definition
  let A be QC-alphabet;
  let ll be FinSequence of QC-variables(A);
  func still_not-bound_in ll -> Subset of bound_QC-variables(A) equals
  { ll.k : 1
  <= k & k <= len ll & ll.k in bound_QC-variables(A) };
  coherence
  proof
    set IT = { ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables(A) };
    now
      let x be object;
      assume x in IT;
      then
      ex k being Nat st x = ll.k & 1 <= k & k <= len ll & ll.k
      in bound_QC-variables(A);
      hence x in bound_QC-variables(A);
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

reserve k for Nat;

definition
  let A be QC-alphabet;
  let p be QC-formula of A;
  func still_not-bound_in p -> Subset of bound_QC-variables(A) means
  ex F being Function of QC-WFF(A), bool bound_QC-variables(A)
    st it = F.p & for p being Element
of QC-WFF(A) holds F.VERUM(A) = {}
   & (p is atomic implies F.p = { (the_arguments_of p
  ).k : 1 <= k & k <= len the_arguments_of p & (the_arguments_of p).k in
bound_QC-variables(A) })
  & (p is negative implies F.p = F.the_argument_of p) & (p
  is conjunctive implies F.p = (F.the_left_argument_of p) \/ (F.
the_right_argument_of p)) & (p is universal implies F.p = (F.the_scope_of p) \
  {bound_in p});
  existence
  proof
    deffunc Q(Element of QC-WFF(A), Subset of bound_QC-variables(A)) = $2 \ {
    bound_in $1};
    deffunc C(Subset of bound_QC-variables(A),
              Subset of bound_QC-variables(A)) = $1
    \/ $2;
    deffunc N(Subset of bound_QC-variables(A)) = $1;
    deffunc A(Element of QC-WFF(A)) = still_not-bound_in (the_arguments_of $1);
    reconsider Emp = {} as Subset of bound_QC-variables(A) by XBOOLE_1:2;
    consider F being Function of QC-WFF(A), bool bound_QC-variables(A)
    such that A1: F.VERUM(A) = Emp & 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 QCFuncEx;
    take F.p, F;
    thus F.p = F.p;
    let p be Element of QC-WFF(A);
    thus F.VERUM(A) = {} by A1;
    thus p is atomic implies F.p = { (the_arguments_of p).k : 1 <= k & k <=
    len the_arguments_of p & (the_arguments_of p).k in bound_QC-variables(A) }
    proof
      assume p is atomic;
      then F.p = still_not-bound_in (the_arguments_of p) by A1;
      hence thesis;
    end;
    thus p is negative implies F.p = F.the_argument_of p by A1;
    thus p is conjunctive implies F.p = (F.the_left_argument_of p) \/ (F.
    the_right_argument_of p) by A1;
    assume p is universal;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let IT,IT9 be Subset of bound_QC-variables(A);
    given F1 being Function of QC-WFF(A), bool bound_QC-variables(A) such that
A2: IT = F1.p and
A3: for p being Element of QC-WFF(A) holds F1.VERUM(A) = {} & (p is atomic
implies F1.p = { (the_arguments_of p).k : 1 <= k & k <= len the_arguments_of p
& (the_arguments_of p).k in bound_QC-variables(A) })
& (p is negative implies F1.p = F1.the_argument_of p)
& (p is conjunctive implies F1.p = (F1.the_left_argument_of p)
    \/ (F1.the_right_argument_of p))
& (p is universal implies F1.p = (F1.the_scope_of p) \ {bound_in p});
    given F2 being Function of QC-WFF(A), bool bound_QC-variables(A) such that
A4: IT9 = F2.p and
A5: for p being Element of QC-WFF(A) holds F2.VERUM(A) = {} & (p is atomic
implies F2.p = { (the_arguments_of p).k : 1 <= k & k <= len the_arguments_of p
& (the_arguments_of p).k in bound_QC-variables(A) })
& (p is negative implies F2.p
    = F2.the_argument_of p) & (p is conjunctive implies F2.p = (F2.
    the_left_argument_of p) \/ (F2.the_right_argument_of p)) & (p is universal
    implies F2.p = (F2.the_scope_of p) \ {bound_in p});
    defpred Prop[Element of QC-WFF(A)] means F1.$1 = F2.$1;
A6: for k being Nat, P being (QC-pred_symbol of k, A), ll being
    QC-variable_list of k, A holds Prop[P!ll]
    proof
      let k be Nat, P be (QC-pred_symbol of k, A), ll be
      QC-variable_list of k, A;
A7:   P!ll is atomic;
      then
A8:   the_arguments_of P!ll = ll by Def23;
      hence F1.(P!ll) = { ll.j : 1 <= j & j <= len ll & ll.j in
      bound_QC-variables(A) } by A3,A7
        .= F2.(P!ll) by A5,A7,A8;
    end;
A9: for p being Element of QC-WFF(A) st Prop[p] holds Prop['not' p]
    proof
      let p be Element of QC-WFF(A) such that
A10:  F1.p = F2.p;
A11:  'not' p is negative;
      then
A12:  the_argument_of 'not' p = p by Def24;
      hence F1.'not' p = F2.p by A3,A10,A11
        .= F2.'not' p by A5,A11,A12;
    end;
A13: for x being bound_QC-variable of A, p being Element of QC-WFF(A)
       holds Prop[p] implies Prop[All(x, p)]
    proof
      let x be bound_QC-variable of A, p be Element of QC-WFF(A) such that
A14:  F1.p = F2.p;
A15:  All(x,p) is universal;
      then
A16:  the_scope_of All(x, p) = p & bound_in All(x, p) = x by Def27,Def28;
      hence F1.All(x, p) = (F2.p) \ { x } by A3,A14,A15
        .= F2.All(x, p) by A5,A15,A16;
    end;
A17: 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) such that
A18:  F1.p = F2.p & F1.q = F2.q;
A19:  p '&' q is conjunctive;
      then
A20:  the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q
      ) = q by Def25,Def26;
      hence F1.(p '&' q) = (F2.p) \/ (F2.q) by A3,A18,A19
        .= F2.(p '&' q) by A5,A19,A20;
    end;
A21: Prop[VERUM(A)] by A3,A5;
    for p be Element of QC-WFF(A) holds Prop[p] from QCInd(A6,A21,A9, A17,
    A13);
    hence thesis by A2,A4;
  end;
end;

definition
  let A be QC-alphabet;
  let p be QC-formula of A;
  attr p is closed means
  still_not-bound_in p = {};
end;

reserve s,t,u,v for QC-symbol of A;

definition
  let A;
  mode Relation of A -> Relation means :Def32:
  it well_orders QC-symbols(A) \ NAT;
  existence by WELLORD2:17;
end;

definition
  let A,s,t;
  pred s <= t means :Def33:
  ex n,m st n = s & m = t & n <= m if s in NAT & t in NAT,
  [s,t] in the Relation of A if not s in NAT & not t in NAT
  otherwise t in NAT;
  consistency;
end;

definition
  let A,s,t;
  pred s < t means
  s <= t & s <> t;
end;

theorem Th21:
  s <= t & t <= u implies s <= u
proof
  set R = the Relation of A;
  R well_orders QC-symbols(A) \ NAT by Def32;
  then
A1: R is_transitive_in QC-symbols(A) \ NAT by WELLORD1:def 5;
  assume
A2: s <= t & t <= u;
  per cases;
  suppose
A3: s in NAT;
    then
A4: t in NAT by A2,Def33;
    then
A5: u in NAT by A2,Def33;
    consider m,n such that
A6:  s = m & t = n & m <= n by A2,A3,A4,Def33;
    consider k,j such that
A7:  t = k & u = j & k <= j by A2,A4,A5,Def33;
    m <= j by A6,A7,XXREAL_0:2;
    hence s <= u by A6,A7,Def33,A3,A5;
  end;
  suppose
A8: not s in NAT;
    per cases;
    suppose t in NAT;
      then u in NAT by A2,Def33;
      hence thesis by A8,Def33;
    end;
    suppose
A9:   not t in NAT;
      per cases;
      suppose u in NAT;
        hence thesis by A8,Def33;
      end;
      suppose
A10:    not u in NAT;
        then
A11:    s in QC-symbols(A) \ NAT & t in QC-symbols(A) \ NAT & u in
         QC-symbols(A) \ NAT by A8,A9,XBOOLE_0:def 5;
        [s,t] in R & [t,u] in R by A2,A8,A9,A10,Def33;
        then [s,u] in R by A1,A11,RELAT_2:def 8;
        hence thesis by A8,A10,Def33;
      end;
    end;
  end;
end;

theorem Th22:
  t <= t
proof
  set R = the Relation of A;
  R well_orders QC-symbols(A) \ NAT by Def32;
  then
A1: R is_reflexive_in QC-symbols(A) \ NAT by WELLORD1:def 5;
  per cases;
  suppose t in NAT;
    hence thesis by Def33;
  end;
  suppose
A2: not t in NAT;
    then t in QC-symbols(A) \ NAT by XBOOLE_0:def 5;
    then [t,t] in the Relation of A by A1,RELAT_2:def 1;
    hence thesis by A2,Def33;
  end;
end;

theorem Th23:
  t <= u & u <= t implies u = t
proof
  set R = the Relation of A;
  R well_orders QC-symbols(A) \ NAT by Def32;
  then
A1: R is_antisymmetric_in QC-symbols(A) \ NAT by WELLORD1:def 5;
  assume
A2: t <= u & u <= t;
  per cases;
    suppose
A3:   t in NAT & u in NAT;
      then consider n,m such that
A4:    t = n & u = m & n <= m by A2,Def33;
      consider k,j such that
A5:    u = k & t = j & k <= j by A2,A3,Def33;
      thus thesis by A4,A5,XXREAL_0:1;
    end;
    suppose not t in NAT or not u in NAT;
      then per cases;
        suppose not t in NAT;
          then
A6:        not t in NAT & not u in NAT by A2,Def33;
          then
A7:        t in QC-symbols(A) \ NAT & u in QC-symbols(A) \ NAT
            by XBOOLE_0:def 5;
          [t,u] in R & [u,t] in R by A2,A6,Def33;
          hence u = t by A1,A7,RELAT_2:def 4;
        end;
        suppose not u in NAT;
          then
A8:        not t in NAT & not u in NAT by A2,Def33;
          then
A9:        t in QC-symbols(A) \ NAT & u in QC-symbols(A) \ NAT
            by XBOOLE_0:def 5;
          [t,u] in R & [u,t] in R by A2,A8,Def33;
          hence u = t by A1,A9,RELAT_2:def 4;
        end;
    end;
end;

theorem Th24:
  t <= u or u <= t
proof
  set R = the Relation of A;
  R well_orders QC-symbols(A) \ NAT by Def32;
  then R is_connected_in QC-symbols(A) \ NAT & R is_reflexive_in
   QC-symbols(A) \ NAT by WELLORD1:def 5;
  then
A1: R is_strongly_connected_in QC-symbols(A) \ NAT by ORDERS_1:7;
  per cases;
    suppose
A2:   t in NAT & u in NAT;
      then consider n,m such that
A3:    n = t & m = u;
      n <= m or m <= n;
      hence thesis by A3,Def33,A2;
    end;
    suppose not t in NAT or not u in NAT;
      then per cases;
        suppose
A4:        not t in NAT;
           per cases;
           suppose u in NAT;
             hence thesis by A4,Def33;
           end;
           suppose
A5:          not u in NAT;
             then t in QC-symbols(A) \NAT & u in QC-symbols(A) \NAT
              by A4,XBOOLE_0:def 5;
             then [t,u] in R or [u,t] in R by A1,RELAT_2:def 7;
             hence thesis by A4,A5,Def33;
           end;
        end;
        suppose
A6:        not u in NAT;
           per cases;
           suppose t in NAT;
             hence thesis by A6,Def33;
           end;
           suppose
A7:          not t in NAT;
             then t in QC-symbols(A) \NAT & u in QC-symbols(A) \NAT
              by A6,XBOOLE_0:def 5;
             then [u,t] in R or [t,u] in R by A1,RELAT_2:def 7;
             hence thesis by A6,A7,Def33;
           end;
        end;
    end;
end;

theorem Th25:
  s < t iff not t <= s
by Th23,Th24;

theorem
  s < t or s = t or t < s
by Th25;

definition
  let A;
  let Y be non empty Subset of QC-symbols(A);
  func min Y -> QC-symbol of A means :Def35:
  it in Y & for t st t in Y holds it <= t;
  existence
  proof
    per cases;
    suppose Y c= NAT;
      then reconsider Y as non empty Subset of NAT;
      set y = min* Y;
      NAT c= QC-symbols(A) by Th3;
      then reconsider yp = y as QC-symbol of A;
      take yp;
      for t st t in Y holds yp <= t
      proof
        let t;
        assume
A1:      t in Y;
        reconsider t as Nat by A1;
        y <= t by A1,NAT_1:def 1;
        hence thesis by A1,Def33;
      end;
      hence thesis by NAT_1:def 1;
    end;
    suppose not Y c= NAT;
      then consider a being object such that
A2:    a in Y & not a in NAT;
      set R = the Relation of A;
      R well_orders QC-symbols(A) \ NAT & Y \ NAT <> {}
       by A2,Def32,XBOOLE_0:def 5;
      then consider y being object such that
A3:    (y in Y \ NAT &
    (for b being object st b in Y \ NAT holds [y,b] in R))
       by WELLORD1:5,XBOOLE_1:33;
      reconsider y as QC-symbol of A by A3;
A4:  not y in NAT & y in Y by A3,XBOOLE_0:def 5;
      for s st s in Y holds y <= s
      proof
        let s;
        assume
A5:     s in Y;
        per cases;
        suppose s in NAT;
          hence thesis by A4,Def33;
        end;
        suppose
A6:      not s in NAT;
          then s in Y \ NAT by A5,XBOOLE_0:def 5;
          then [y,s] in R by A3;
          hence thesis by A4,A6,Def33;
        end;
      end;
      hence thesis by A4;
    end;
  end;
  uniqueness
  proof
    let t,u such that
A7:  (t in Y & for s st s in Y holds t <= s) &
     (u in Y & for s st s in Y holds u <= s);
    t <= u & u <= t by A7;
    hence thesis by Th23;
  end;
end;

definition
  let A;
  func 0(A) -> QC-symbol of A means
  for t holds it <= t;
  existence
  proof
    QC-symbols(A) c= QC-symbols(A);
    then reconsider symb = QC-symbols(A) as non empty Subset of QC-symbols(A);
    set z = min symb;
    take z;
    thus thesis by Def35;
  end;
  uniqueness
  proof
    let s,t such that
A1:  (for u holds s <= u) & (for u holds t <= u);
    s <= t & t <= s by A1;
    hence thesis by Th23;
  end;
end;

definition
  let A,s;
  func Seg s -> non empty Subset of QC-symbols(A) equals
   { t : s < t };
  coherence
  proof
    set e = { t : s < t };
A1: e c= QC-symbols(A)
    proof
      let a be object;
      assume a in e;
      then consider t such that
A2:    a = t & s < t;
      thus thesis by A2;
    end;
    ex a being set st a in e
    proof
      per cases;
      suppose
A3:     s in NAT;
        then consider n such that
A4:      s = n;
        reconsider a = n+1 as Nat;
        NAT c= QC-symbols(A) by Th3;
        then reconsider b = a as QC-symbol of A;
        not n = a & n <= a by NAT_1:19;
        then s <= b & not s = b by A4,Def33,A3;
        then s < b;
        then b in { t : s < t };
        hence thesis;
      end;
      suppose
A5:     not s in NAT;
        reconsider a = 0 as QC-symbol of A by Th3;
        not s = a & s <= a by A5,Def33;
        then s < a;
        then a in e;
        hence thesis;
      end;
    end;
    hence thesis by A1;
  end;
end;

definition
  let A,s;
  func s++ -> QC-symbol of A equals
  min (Seg s);
  coherence;
end;

theorem Th27:
  s < s++
proof
  s++ in Seg s by Def35;
  then consider t such that
A1: t = s++ & s < t;
  thus thesis by A1;
end;

theorem
  for Y1,Y2 being non empty Subset of QC-symbols(A) st Y1 c= Y2 holds
    min Y2 <= min Y1
proof
  let Y1,Y2 be non empty Subset of QC-symbols(A) such that
A1: Y1 c= Y2;
  min Y1 in Y1 by Def35;
  hence min Y2 <= min Y1 by A1,Def35;
end;

theorem Th29:
  s <= t & t < v implies s < v
by Th21,Th25;

theorem
  s < t & t <= v implies s < v
by Th21,Th25;

definition
  let A;
  let s be set;
  func s@A -> QC-symbol of A equals :Def39:
  s if s is QC-symbol of A
  otherwise 0;
  correctness by Th3;
end;

definition
  let A,t,n;
  func t + n -> QC-symbol of A means :Def40:
  ex f being sequence of QC-symbols(A) st
  it = f.n & f.0 = t & for k holds f.(k+1) = (f.k)++;
  existence
  proof
    deffunc F(set,set) = ($2@A)++;
    consider f being sequence of QC-symbols(A) such that
A1:  f.0 = t & for k being Nat holds f.(k+1) = F(k,f.k) from NAT_1:sch 12;
    take f.n;
    for k holds f.(k+1) = (f.k)++
    proof
      let k;
      (f.k)++ = F(k,f.k) & F(k,f.k) = f.(k+1) by A1,Def39;
      hence thesis;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let u,v such that
A2:  (ex f being sequence of  QC-symbols(A) st f.n = u & f.0 = t &
     for k holds f.(k+1) = (f.k)++) & (ex g being sequence of QC-symbols(A)
     st g.n = v & g.0 = t & for k holds g.(k+1) = (g.k)++);
    consider f being sequence of  QC-symbols(A) such that
A3:  f.n = u & f.0 = t & for k holds f.(k+1) = (f.k)++ by A2;
    consider g being sequence of QC-symbols(A) such that
A4:  g.n = v & g.0 = t & for k holds g.(k+1) = (g.k)++ by A2;
    defpred P[Nat] means f.($1) = g.($1);
A5: P[0] by A3,A4;
A6: for k st P[k] holds P[k+1]
    proof
      let k;
      assume
A7:    P[k];
      thus f.(k+1) = (f.k)++ by A3
             .= g.(k+1) by A4,A7;
    end;
    for k holds P[k] from NAT_1:sch 2(A5,A6);
    hence thesis by A3,A4;
  end;
end;

theorem
  t <= t+n
proof
  defpred P[Nat] means t <= t + $1;
A1: P[0]
  proof
    consider f being sequence of QC-symbols(A) such that
A2:  t + 0 = f.0 & f.0 = t & for k holds f.(k+1) = (f.k)++ by Def40;
    thus thesis by A2,Th22;
  end;
A3: for k st P[k] holds P[k+1]
  proof
    let k such that
A4:  t <= t + k;
    consider f being sequence of QC-symbols(A) such that
A5:  t + (k+1) = f.(k+1) & f.0 = t & for k holds f.(k+1) = (f.k)++ by Def40;
    f.k = t + k by A5,Def40;
    then f.(k+1) = (t + k)++ by A5;
    then t < t + (k+1) by A5,A4,Th27,Th29;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 2(A1,A3);
  hence thesis;
end;

definition
  let A;
  let Y be set;
  func A-one_in Y -> QC-symbol of A equals
  the Element of Y if Y is non empty Subset of QC-symbols(A)
  otherwise 0(A);
  coherence
  proof
    thus Y is non empty Subset of QC-symbols(A)
      implies the Element of Y is QC-symbol of A
    proof
      assume
A1:   Y is non empty Subset of QC-symbols(A);
      consider a being set such that
A2:   a = the Element of Y;
A3:   a in Y by A1,A2;
      a is QC-symbol of A by A1,A3;
      hence thesis by A2;
    end;
    thus not Y is non empty Subset of QC-symbols(A)
      implies 0(A) is QC-symbol of A;
  end;
  consistency;
end;