:: Introduction to Modal Propositional Logic
::  by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991-2012 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, TREES_2, ZFMISC_1, FINSEQ_1, XBOOLE_0,
      TREES_1, FUNCT_1, RELAT_1, ORDINAL4, NAT_1, CARD_1, XXREAL_0, PARTFUN1,
      TARSKI, ORDINAL1, ARYTM_3, FINSET_1, FUNCOP_1, MARGREL1, MCART_1,
      QC_LANG1, XBOOLEAN, VALUED_1, ZF_LANG, MODAL_1, TREES_3;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1,
      XTUPLE_0, SUBSET_1, CARD_1, NUMBERS,
      WELLORD2, ORDINAL1, NAT_1, DOMAIN_1, MCART_1, RELAT_1, FUNCT_1, RELSET_1,
      FINSEQ_1, FUNCOP_1, FINSEQ_2, FUNCT_2, FINSET_1, PARTFUN1, TREES_1,
      TREES_2, XXREAL_0, TREES_3;
 constructors PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2,
      TREES_2, RELSET_1, FUNCOP_1, TREES_3, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
      XXREAL_0, XREAL_0, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1, TREES_3,
      XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, FUNCT_1, XTUPLE_0;
 theorems TARSKI, FUNCT_1, NAT_1, ENUMSET1, TREES_1, TREES_2, FUNCOP_1,
      MCART_1, DOMAIN_1, PARTFUN1, FINSEQ_1, FINSET_1, CARD_1, WELLORD2,
      CARD_2, ZFMISC_1, FINSEQ_2, RELAT_1, FUNCT_2, RELSET_1, XBOOLE_0,
      XBOOLE_1, XREAL_1, XXREAL_0, TREES_3, XTUPLE_0;
 schemes TREES_2, CLASSES1, NAT_1, FUNCT_2, XBOOLE_0;

begin

reserve x,y,x1,x2,z for set,
  n,m,k for Element of NAT,
  t1 for (DecoratedTree of [: NAT,NAT :]),
  w,s,t,u for FinSequence of NAT,
  D for non empty set;

Lm1: {} is_a_proper_prefix_of <*m*>
proof
  {} is_a_prefix_of <*m*> by XBOOLE_1:2;
  hence thesis by XBOOLE_0:def 8;
end;

definition
  let Z be Tree;
  func Root Z -> Element of Z equals
  {};
  coherence by TREES_1:22;
end;

definition
  let D;
  let T be DecoratedTree of D;
  func Root T -> Element of D equals
  T.(Root dom T);
  coherence;
end;

theorem Th1:
  n <> m implies not <*n*>,<*m*>^s are_c=-comparable
proof
  assume
A1: n<>m;
  assume
A2: <*n*>,<*m*>^s are_c=-comparable;
  per cases by A2,XBOOLE_0:def 9;
  suppose
    <*n*> is_a_prefix_of <*m*>^s;
    then
A3: ex a be FinSequence st <*m*>^s = <*n*>^a by TREES_1:1;
    m = (<*m*>^s).1 by FINSEQ_1:41
      .= n by A3,FINSEQ_1:41;
    hence contradiction by A1;
  end;
  suppose
    <*m*>^s is_a_prefix_of <*n*>;
    then consider a be FinSequence such that
A4: <*n*> = <*m*>^s^a by TREES_1:1;
    n = (<*m*>^s^a).1 by A4,FINSEQ_1:40
      .= (<*m*>^(s^a)).1 by FINSEQ_1:32
      .= m by FINSEQ_1:41;
    hence contradiction by A1;
  end;
end;

theorem
  for s st s <> {} ex w being FinSequence of NAT,
  n being Element of NAT st s = <*n*>^w by FINSEQ_2:130;

theorem Th3:
  n <> m implies not <*n*> is_a_proper_prefix_of <*m*>^s
proof
  assume
A1: n <> m;
  assume <*n*> is_a_proper_prefix_of <*m*>^s;
  then <*n*> is_a_prefix_of <*m*>^s by XBOOLE_0:def 8;
  then
A2: ex a be FinSequence st <*m*>^s = <*n*>^a by TREES_1:1;
  m = (<*m*>^s).1 by FINSEQ_1:41
    .= n by A2,FINSEQ_1:41;
  hence contradiction by A1;
end;

theorem
  n <> m implies not <*n*> is_a_prefix_of <*m*>^s by TREES_1:50;

theorem
  not <*n*> is_a_proper_prefix_of <*m*> by TREES_1:52;

theorem
  elementary_tree 1 = {{},<*0*>} by TREES_1:51;

theorem
  elementary_tree 2 = {{},<*0*>,<*1*>} by TREES_1:53;

theorem Th8:
  for Z being Tree,n,m st n <= m & <*m*> in Z holds <*n*> in Z
proof
  reconsider s = {} as FinSequence of NAT by TREES_1:22;
  let Z be Tree,n,m;
  assume that
A1: n <= m and
A2: <*m*> in Z;
  {}^<*m*> in Z by A2,FINSEQ_1:34;
  then s^<*n*> in Z by A1,TREES_1:def 3;
  hence thesis by FINSEQ_1:34;
end;

theorem
  w^t is_a_proper_prefix_of w^s implies t is_a_proper_prefix_of s by TREES_1:49
;

theorem Th10:
  t1 in PFuncs(NAT*,[: NAT,NAT :])
proof
  rng t1 c= [: NAT,NAT :] & dom t1 c= NAT* by TREES_1:def 3;
  hence thesis by PARTFUN1:def 3;
end;

theorem Th11:
  for Z,Z1,Z2 being Tree,z being Element of Z st Z
  with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2
proof
  let Z,Z1,Z2 be Tree,z be Element of Z;
  assume
A1: Z with-replacement (z,Z1) = Z with-replacement (z,Z2);
  now
    let s;
    thus s in Z1 implies s in Z2
    proof
      assume
A2:   s in Z1;
      per cases;
      suppose
        s = {};
        hence thesis by TREES_1:22;
      end;
      suppose
        s <> {};
        then
A3:     z is_a_proper_prefix_of z^s by TREES_1:10;
        z^s in Z with-replacement (z,Z2) by A1,A2,TREES_1:def 9;
        then ex w st w in Z2 & z^s = z^w by A3,TREES_1:def 9;
        hence thesis by FINSEQ_1:33;
      end;
    end;
    assume
A4: s in Z2;
    per cases;
    suppose
      s = {};
      hence s in Z1 by TREES_1:22;
    end;
    suppose
      s <> {};
      then
A5:   z is_a_proper_prefix_of z^s by TREES_1:10;
      z^s in Z with-replacement (z,Z1) by A1,A4,TREES_1:def 9;
      then ex w st w in Z1 & z^s = z^w by A5,TREES_1:def 9;
      hence s in Z1 by FINSEQ_1:33;
    end;
  end;
  hence thesis by TREES_2:def 1;
end;

theorem Th12:
  for Z,Z1,Z2 being (DecoratedTree of D),z being Element of dom Z st
  Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2
proof
  let Z,Z1,Z2 be (DecoratedTree of D),z be Element of dom Z;
  assume
A1: Z with-replacement (z,Z1) = Z with-replacement (z,Z2);
  set T2 = Z with-replacement (z,Z2);
  set T1 = Z with-replacement (z,Z1);
A2: dom T1 = dom Z with-replacement (z,dom Z1) by TREES_2:def 11;
  then
A3: dom Z with-replacement (z,dom Z1) = dom Z with-replacement (z,dom Z2) by A1
,TREES_2:def 11;
A4: for s st s in dom Z1 holds Z1.s = Z2.s
  proof
    let s;
A5: z is_a_prefix_of z^s by TREES_1:1;
    assume
A6: s in dom Z1;
    then z^s in dom Z with-replacement (z,dom Z1) by TREES_1:def 9;
    then
A7: ex u st u in dom Z1 & z^s = z^u & T1.(z^s) = Z1.u by A5,TREES_2:def 11;
    z^s in dom Z with-replacement (z,dom Z2) by A3,A6,TREES_1:def 9;
    then consider w such that
    w in dom Z2 and
A8: z^s = z^w and
A9: T2.(z^s) = Z2.w by A5,TREES_2:def 11;
    s = w by A8,FINSEQ_1:33;
    hence thesis by A1,A9,A7,FINSEQ_1:33;
  end;
  dom T2 = dom Z with-replacement (z,dom Z2) by TREES_2:def 11;
  hence thesis by A1,A2,A4,Th11,TREES_2:31;
end;

theorem Th13:
  for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2), w being Element of Z1 st v =
  w & w is_a_proper_prefix_of p holds succ v = succ w
proof
  let Z1,Z2 be Tree,p be FinSequence of NAT;
  assume
A1: p in Z1;
  set Z = Z1 with-replacement (p,Z2);
  let v be Element of Z,w be Element of Z1;
  assume that
A2: v = w and
A3: w is_a_proper_prefix_of p;
  w is_a_prefix_of p by A3,XBOOLE_0:def 8;
  then consider r be FinSequence such that
A4: p = w^r by TREES_1:1;
  now
    let n be Nat;
    assume
A5: n in dom r;
    then len w + n in dom p by A4,FINSEQ_1:28;
    then
A6: p.(len w + n) in rng p by FUNCT_1:def 3;
    p.(len w + n) = r.n by A4,A5,FINSEQ_1:def 7;
    hence r.n in NAT by A6;
  end;
  then reconsider r as FinSequence of NAT by FINSEQ_2:12;
A7: r <> {} by A3,A4,FINSEQ_1:34;
  now
    let x;
    thus x in succ v implies x in succ w
    proof
      assume x in succ v;
      then x in { v^<*n*> : v^<*n*> in Z} by TREES_2:def 5;
      then consider n such that
A8:   x = v^<*n*> and
A9:   v^<*n*> in Z;
      reconsider x9 = x as FinSequence of NAT by A8;
      now
        per cases by A1,A8,A9,TREES_1:def 9;
        suppose
          x9 in Z1 & not p is_a_proper_prefix_of x9;
          then x in { w^<*m*> : w^<*m*> in Z1} by A2,A8;
          hence thesis by TREES_2:def 5;
        end;
        suppose
          ex r be FinSequence of NAT st r in Z2 & x9 = p^r;
          then consider s such that
          s in Z2 and
A10:      v^<*n*> = p^s by A8;
          w^<*n*> = w^(r^s) by A2,A4,A10,FINSEQ_1:32;
          then
A11:      <*n*> = r^s by FINSEQ_1:33;
          s = {}
          proof
            assume not thesis;
            then len s > 0 by NAT_1:3;
            then
A12:        0+1 <= len s by NAT_1:13;
            len r > 0 by A7,NAT_1:3;
            then 0+1 <= len r by NAT_1:13;
            then 1 + 1 <= len r + len s by A12,XREAL_1:7;
            then 2 <= len (<*n*>) by A11,FINSEQ_1:22;
            then 2 <= 1 by FINSEQ_1:39;
            hence contradiction;
          end;
          then <*n*> = r by A11,FINSEQ_1:34;
          then x in { w^<*m*> : w^<*m*> in Z1} by A1,A2,A4,A8;
          hence thesis by TREES_2:def 5;
        end;
      end;
      hence thesis;
    end;
    assume x in succ w;
    then x in { w^<*n*> : w^<*n*> in Z1} by TREES_2:def 5;
    then consider n such that
A13: x = w^<*n*> and
A14: w^<*n*> in Z1;
    now
      assume
A15:  not v^<*n*> in Z;
      now
        per cases by A1,A15,TREES_1:def 9;
        suppose
          not v^<*n*> in Z1;
          hence contradiction by A2,A14;
        end;
        suppose
          p is_a_proper_prefix_of v^<*n*>;
          then r is_a_proper_prefix_of <*n*> by A2,A4,TREES_1:49;
          then r in ProperPrefixes <*n*> by TREES_1:12;
          then r in{{}} by TREES_1:16;
          hence contradiction by A7,TARSKI:def 1;
        end;
      end;
      hence contradiction;
    end;
    then x in { v^<*m*> : v^<*m*> in Z} by A2,A13;
    hence x in succ v by TREES_2:def 5;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th14:
  for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2),w being Element of Z1 st v =
  w & not p,w are_c=-comparable holds succ v = succ w
proof
  let Z1,Z2 be Tree,p be FinSequence of NAT;
  assume
A1: p in Z1;
  set Z = Z1 with-replacement (p,Z2);
  let v be Element of Z,w be Element of Z1;
  assume that
A2: v = w and
A3: not p,w are_c=-comparable;
A4: not p is_a_prefix_of w by A3,XBOOLE_0:def 9;
  now
    let x;
    thus x in succ v implies x in succ w
    proof
      assume x in succ v;
      then x in { v^<*n*> : v^<*n*> in Z} by TREES_2:def 5;
      then consider n such that
A5:   x = v^<*n*> and
A6:   v^<*n*> in Z;
      reconsider x9 = x as FinSequence of NAT by A5;
      v^<*n*> in Z1
      proof
        assume
A7:     not v^<*n*> in Z1;
        then ex t st t in Z2 & x9 = p^t by A1,A5,A6,TREES_1:def 9;
        then
A8:     p is_a_prefix_of v^<*n*> by A5,TREES_1:1;
        per cases by A8,XBOOLE_0:def 8;
        suppose
          p is_a_proper_prefix_of v^<*n*>;
          hence contradiction by A2,A4,TREES_1:9;
        end;
        suppose
          p = v^<*n*>;
          hence contradiction by A1,A7;
        end;
      end;
      then x in { w^<*m*> : w^<*m*> in Z1} by A2,A5;
      hence thesis by TREES_2:def 5;
    end;
    assume x in succ w;
    then x in { w^<*n*> : w^<*n*> in Z1} by TREES_2:def 5;
    then consider n such that
A9: x = w^<*n*> and
A10: w^<*n*> in Z1;
    not p is_a_proper_prefix_of w^<*n*> by A4,TREES_1:9;
    then v^<*n*> in Z by A1,A2,A10,TREES_1:def 9;
    then x in { v^<*m*> : v^<*m*> in Z} by A2,A9;
    hence x in succ v by TREES_2:def 5;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds for v
  being Element of Z1 with-replacement (p,Z2),w being Element of Z2 st v = p^w
  holds succ v,succ w are_equipotent by TREES_2:37;

theorem Th16:
  for Z1 being Tree,p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1,w being Element of Z1|p st v = p^w holds succ v,succ
  w are_equipotent
proof
  let Z1 be Tree,p be FinSequence of NAT such that
A1: p in Z1;
  set T = Z1|p;
  let t be Element of Z1,t2 be Element of Z1|p such that
A2: t = p^t2;
A3: for n holds t^<*n*> in Z1 iff t2^<*n*> in T
  proof
    let n;
A4: t^<*n*> = p^(t2^<*n*>) by A2,FINSEQ_1:32;
    hence t^<*n*> in Z1 implies t2^<*n*> in T by A1,TREES_1:def 6;
    assume t2^<*n*> in T;
    hence thesis by A1,A4,TREES_1:def 6;
  end;
  defpred P[set,set] means for n st $1 = t^<*n*> holds $2 = t2^<*n*>;
A5: for x st x in succ t ex y st P[x,y]
  proof
    let x;
    assume x in succ t;
    then x in { t^<*n*> : t^<*n*> in Z1 } by TREES_2:def 5;
    then consider n such that
A6: x = t^<*n*> and
    t^<*n*> in Z1;
    take t2^<*n*>;
    let m;
    assume x = t^<*m*>;
    hence thesis by A6,FINSEQ_1:33;
  end;
  consider f being Function such that
A7: dom f = succ t & for x st x in succ t holds P[x,f.x] from CLASSES1:
  sch 1 (A5);
  now
    let x;
    thus x in rng f implies x in succ t2
    proof
      assume x in rng f;
      then consider y such that
A8:   y in dom f and
A9:   x = f.y by FUNCT_1:def 3;
      y in { t^<*n*> : t^<*n*> in Z1 } by A7,A8,TREES_2:def 5;
      then consider n such that
A10:  y = t^<*n*> and
A11:  t^<*n*> in Z1;
A12:  t2^<*n*> in T by A3,A11;
      x = t2^<*n*> by A7,A8,A9,A10;
      then x in { t2^<*m*> : t2^<*m*> in T } by A12;
      hence thesis by TREES_2:def 5;
    end;
    assume x in succ t2;
    then x in { t2^<*n*> : t2^<*n*> in T } by TREES_2:def 5;
    then consider n such that
A13: x = t2^<*n*> and
A14: t2^<*n*> in T;
    t^<*n*> in Z1 by A3,A14;
    then t^<*n*> in { t^<*m*> : t^<*m*> in Z1 };
    then
A15: t^<*n*> in dom f by A7,TREES_2:def 5;
    then f.(t^<*n*>) = x by A7,A13;
    hence x in rng f by A15,FUNCT_1:def 3;
  end;
  then
A16: rng f = succ t2 by TARSKI:1;
  now
    let x1,x2;
    assume that
A17: x1 in dom f and
A18: x2 in dom f and
A19: f.x1 = f.x2;
    x2 in { t^<*n*> : t^<*n*> in Z1 } by A7,A18,TREES_2:def 5;
    then consider k such that
A20: x2 = t^<*k*> and
    t^<*k*> in Z1;
    x1 in { t^<*n*> : t^<*n*> in Z1 } by A7,A17,TREES_2:def 5;
    then consider m such that
A21: x1 = t^<*m*> and
    t^<*m*> in Z1;
    t2^<*m*> = f.x1 by A7,A17,A21
      .= t2^<*k*> by A7,A18,A19,A20;
    hence x1 = x2 by A21,A20,FINSEQ_1:33;
  end;
  then f is one-to-one by FUNCT_1:def 4;
  hence thesis by A7,A16,WELLORD2:def 4;
end;

theorem Th17:
  for Z being finite Tree st branchdeg (Root Z) = 0 holds card Z = 1 & Z = {{}}
proof
  let Z be finite Tree;
  assume branchdeg (Root Z) = 0;
  then 0 = card succ (Root Z) by TREES_2:def 12;
  then
A1: succ (Root Z) = {};
  now
    let x;
    thus x in Z implies x in { Root Z }
    proof
      assume x in Z;
      then reconsider z = x as Element of Z;
      assume not thesis;
      then z <> Root Z by TARSKI:def 1;
      then consider w being FinSequence of NAT,
      n being Element of NAT such that
A2:   z = <*n*>^w by FINSEQ_2:130;
      <*n*> is_a_prefix_of z by A2,TREES_1:1;
      then <*n*> in Z by TREES_1:20;
      then {}^<*n*> in Z by FINSEQ_1:34;
      hence contradiction by A1,TREES_2:12;
    end;
    assume x in { Root Z };
    then reconsider x9= x as Element of Z;
    x9 in Z;
    hence x in Z;
  end;
  then Z = { Root Z } by TARSKI:1;
  hence thesis by CARD_2:42;
end;

theorem Th18:
  for Z being finite Tree st branchdeg (Root Z) = 1 holds succ (
  Root Z) = { <*0*> }
proof
  let Z be finite Tree;
  assume branchdeg (Root Z) = 1;
  then card succ (Root Z) = 1 by TREES_2:def 12;
  then consider x such that
A1: succ (Root Z) = {x} by CARD_2:42;
A2: x in succ (Root Z) by A1,TARSKI:def 1;
  then reconsider x9 = x as Element of Z;
  x9 in { (Root Z)^<*n*> : (Root Z)^<*n*> in Z } by A2,TREES_2:def 5;
  then consider m such that
A3: x9 = (Root Z)^<*m*> and
A4: (Root Z)^<*m*> in Z;
A5: x9 = <*m*> by A3,FINSEQ_1:34;
  now
A6: <*0*> = (Root Z)^<*0*> by FINSEQ_1:34;
    <*m*> in Z by A4,FINSEQ_1:34;
    then <*0*> in Z by Th8,NAT_1:2;
    then (Root Z)^<*0*> in succ (Root Z) by A6,TREES_2:12;
    then
A7: <*0*> = x by A1,A6,TARSKI:def 1;
    assume m <> 0;
    hence contradiction by A5,A7,TREES_1:3;
  end;
  hence thesis by A1,A3,FINSEQ_1:34;
end;

theorem Th19:
  for Z being finite Tree st branchdeg (Root Z) = 2 holds succ (
  Root Z) = { <*0*>,<*1*> }
proof
  let Z be finite Tree;
  assume branchdeg (Root Z) = 2;
  then card succ (Root Z) = 2 by TREES_2:def 12;
  then consider x,y such that
A1: x <> y and
A2: succ (Root Z) = {x,y} by CARD_2:60;
A3: x in succ (Root Z) by A2,TARSKI:def 2;
  then reconsider x9 = x as Element of Z;
  x9 in { (Root Z)^<*n*> : (Root Z)^<*n*> in Z } by A3,TREES_2:def 5;
  then consider m such that
A4: x9 = (Root Z)^<*m*> and
  (Root Z)^<*m*> in Z;
A5: x9 = <*m*> by A4,FINSEQ_1:34;
A6: y in succ (Root Z) by A2,TARSKI:def 2;
  then reconsider y9 = y as Element of Z;
  y9 in { (Root Z)^<*n*> : (Root Z)^<*n*> in Z } by A6,TREES_2:def 5;
  then consider k such that
A7: y9 = (Root Z)^<*k*> and
  (Root Z)^<*k*> in Z;
A8: y9 = <*k*> by A7,FINSEQ_1:34;
  per cases;
  suppose
A9: m = 0;
    now
A10:  <*1*> = (Root Z)^<*1*> by FINSEQ_1:34;
      assume
A11:  k <> 1;
      then 2 <= k by A1,A5,A8,A9,NAT_1:26;
      then <*1*> in Z by A8,Th8,XXREAL_0:2;
      then <*1*> in succ (Root Z) by A10,TREES_2:12;
      then <*1*> = <*0*> or <*1*> = <*k*> by A2,A5,A8,A9,TARSKI:def 2;
      hence contradiction by A11,TREES_1:3;
    end;
    hence thesis by A2,A4,A8,A9,FINSEQ_1:34;
  end;
  suppose
A12: m <> 0;
    <*0*> in Z & <*0*> = (Root Z)^<*0*> by A5,Th8,FINSEQ_1:34,NAT_1:2;
    then <*0*> in succ (Root Z) by TREES_2:12;
    then
A13: <*0*> = <*m*> or <*0*> = <*k*> by A2,A5,A8,TARSKI:def 2;
    now
A14:  <*1*> = (Root Z)^<*1*> by FINSEQ_1:34;
      assume
A15:  m <> 1;
      then 2 <= m by A12,NAT_1:26;
      then <*1 *> in Z by A5,Th8,XXREAL_0:2;
      then <*1*> in succ (Root Z) by A14,TREES_2:12;
      then <*1*> = <*0*> or <*1*> = <*m*> by A2,A5,A8,A12,A13,TARSKI:def 2
,TREES_1:3;
      hence contradiction by A15,TREES_1:3;
    end;
    hence thesis by A2,A4,A8,A13,FINSEQ_1:34,TREES_1:3;
  end;
end;

reserve s9,w9,v9 for Element of NAT*;

theorem Th20:
  for Z being Tree,o being Element of Z st o <> Root Z holds Z|o,{
  o^s9: o^s9 in Z } are_equipotent & not Root Z in { o^w9 : o^w9 in Z }
proof
  let Z be Tree,o be Element of Z such that
A1: o <> Root Z;
  set A = { o^s9 : o^s9 in Z };
  thus Z|o,A are_equipotent
  proof
    defpred P[set,set] means for s st $1 = s holds $2 = o^s;
A2: for x st x in Z|o ex y st P[x,y]
    proof
      let x;
      assume x in Z|o;
      then reconsider s = x as FinSequence of NAT by TREES_1:19;
      take o^s;
      let w;
      assume x = w;
      hence thesis;
    end;
    ex f being Function st dom f = Z|o & for x st x in Z|o holds P[x,f.x]
    from CLASSES1:sch 1(A2);
    then consider f being Function such that
A3: dom f = Z|o and
A4: for x st x in Z|o holds for s st x = s holds f.x = o^s;
    now
      let x;
      thus x in rng f implies x in A
      proof
        assume x in rng f;
        then consider x1 such that
A5:     x1 in dom f and
A6:     x = f.x1 by FUNCT_1:def 3;
        reconsider x1 as FinSequence of NAT by A3,A5,TREES_1:19;
        reconsider x1 as Element of NAT* by FINSEQ_1:def 11;
        o^x1 in Z & x = o^x1 by A3,A4,A5,A6,TREES_1:def 6;
        hence thesis;
      end;
      assume x in A;
      then consider v9 such that
A7:   x = o^v9 and
A8:   o^v9 in Z;
      v9 in Z|o by A8,TREES_1:def 6;
      then
A9:   x = f.v9 by A4,A7;
      v9 in dom f by A3,A8,TREES_1:def 6;
      hence x in rng f by A9,FUNCT_1:def 3;
    end;
    then
A10: rng f = A by TARSKI:1;
    now
      let x1,x2;
      assume that
A11:  x1 in dom f and
A12:  x2 in dom f and
A13:  f.x1 = f.x2;
      reconsider s1 = x1, s2 = x2 as FinSequence of NAT by A3,A11,A12,
TREES_1:19;
      o^s1 = f.x2 by A3,A4,A11,A13
        .= o^s2 by A3,A4,A12;
      hence x1 = x2 by FINSEQ_1:33;
    end;
    then f is one-to-one by FUNCT_1:def 4;
    hence thesis by A3,A10,WELLORD2:def 4;
  end;
  assume not thesis;
  then ex v9 st Root Z = o^v9 & o^v9 in Z;
  hence contradiction by A1;
end;

theorem Th21:
  for Z being finite Tree,o being Element of Z st o <> Root Z
  holds card (Z|o) < card Z
proof
  let Z be finite Tree,o be Element of Z such that
A1: o <> Root Z;
  set A = { o^s9 : o^s9 in Z };
A2: Z|o,A are_equipotent by A1,Th20;
  then reconsider A as finite set by CARD_1:38;
  reconsider B = A \/ {Root Z} as finite set;
  now
    let x such that
A3: x in B;
    now
      per cases by A3,XBOOLE_0:def 3;
      suppose
        x in { o^s9 : o^s9 in Z };
        then ex v9 st x = o^v9 & o^v9 in Z;
        hence x in Z;
      end;
      suppose
        x in {Root Z};
        hence x in Z;
      end;
    end;
    hence x in Z;
  end;
  then
A4: B c= Z by TARSKI:def 3;
  card B = card A + 1 by A1,Th20,CARD_2:41
    .= card (Z|o) + 1 by A2,CARD_1:5;
  then card (Z|o) + 1 <= card Z by A4,NAT_1:43;
  hence thesis by NAT_1:13;
end;

theorem Th22:
  for Z being finite Tree,z being Element of Z st succ (Root Z) =
  {z} holds Z = elementary_tree 1 with-replacement (<*0*>,Z|z)
proof
  let Z be finite Tree,z be Element of Z;
  set e = elementary_tree 1;
A1: <*0*> in e by TARSKI:def 2,TREES_1:51;
A2: {} in Z by TREES_1:22;
  assume
A3: succ (Root Z) = {z};
  then card succ (Root Z) = 1 by CARD_1:30;
  then branchdeg (Root Z) = 1 by TREES_2:def 12;
  then {z} = { <*0*> } by A3,Th18;
  then z in { <*0*> } by TARSKI:def 1;
  then
A4: z = <*0*> by TARSKI:def 1;
  then
A5: <*0*> in Z;
  now
    let x;
    thus x in Z implies x in e with-replacement (<*0*>,Z|z)
    proof
      assume x in Z;
      then reconsider x9 = x as Element of Z;
      per cases;
      suppose
        x9 = {};
        hence thesis by TREES_1:22;
      end;
      suppose
        x9 <> {};
        then consider w be FinSequence of NAT,
        n being Element of NAT such that
A6:     x9 = <*n*>^w by FINSEQ_2:130;
        <*n*> is_a_prefix_of x9 by A6,TREES_1:1;
        then
A7:     <*n*> in Z by TREES_1:20;
        <*n*> = (Root Z)^<*n*> by FINSEQ_1:34;
        then
A8:     <*n*> in succ (Root Z) by A7,TREES_2:12;
        then <*n*> = z by A3,TARSKI:def 1;
        then
A9:     w in Z|z by A6,TREES_1:def 6;
        <*n*> = <*0*> by A3,A4,A8,TARSKI:def 1;
        hence thesis by A1,A6,A9,TREES_1:def 9;
      end;
    end;
    assume x in e with-replacement (<*0*>,Z|z);
    then reconsider x9 = x as Element of e with-replacement (<*0*>,Z|z);
    per cases by A1,TREES_1:def 9;
    suppose
      x9 in e & not <*0*> is_a_proper_prefix_of x9;
      hence x in Z by A5,A2,TARSKI:def 2,TREES_1:51;
    end;
    suppose
      ex s st s in Z|z & x9 = <*0*>^s;
      hence x in Z by A4,TREES_1:def 6;
    end;
  end;
  hence thesis by TARSKI:1;
end;

Lm2: for f being Function st dom f is finite holds f is finite
proof
  let f be Function;
  assume
A1: dom f is finite;
  then rng f is finite by FINSET_1:8;
  then [:dom f, rng f:] is finite by A1;
  hence thesis by FINSET_1:1,RELAT_1:7;
end;

theorem Th23:
  for Z being finite (DecoratedTree of D),z be Element of dom Z st
  succ (Root dom Z) = {z} holds Z = ((elementary_tree 1) --> Root Z)
  with-replacement (<*0*>,Z|z)
proof
  set e = elementary_tree 1;
  let Z be finite (DecoratedTree of D),z be Element of dom Z;
  set E = (elementary_tree 1) --> Root Z;
A1: dom E = e by FUNCOP_1:13;
A2: dom (Z|z) = (dom Z)|z by TREES_2:def 10;
A3: <*0*> in e by TARSKI:def 2,TREES_1:51;
  then
A4: <*0*> in dom E by FUNCOP_1:13;
  assume
A5: succ (Root dom Z) = {z};
  then card succ (Root dom Z) = 1 by CARD_1:30;
  then branchdeg (Root dom Z) = 1 by TREES_2:def 12;
  then {z} = { <*0*> } by A5,Th18;
  then z in { <*0*> } by TARSKI:def 1;
  then
A6: z = <*0*> by TARSKI:def 1;
A7: for s st s in dom (E with-replacement (<*0*>,Z|z)) holds (E
  with-replacement (<*0*>,Z|z)).s = Z.s
  proof
    let s;
    assume
A8: s in dom (E with-replacement (<*0*>,Z|z));
A9: dom (E with-replacement (<*0*>,Z|z)) = dom E with-replacement(<*0*>,
    dom (Z|z)) by A4,TREES_2:def 11;
    then
A10: not <*0*> is_a_prefix_of s & (E with-replacement (<*0*>,Z|z)).s = E.s
or ex w st w in dom (Z|z) & s = <*0*>^w & (E with-replacement (<*0*>,Z|z)).s =
    (Z|z).w by A4,A8,TREES_2:def 11;
    now
      per cases by A4,A9,A8,TREES_1:def 9;
      suppose
A11:    s in dom E & not <*0*> is_a_proper_prefix_of s;
        now
          per cases by A11,TARSKI:def 2,TREES_1:51;
          suppose
A12:        s = {};
            then s in e by TREES_1:22;
            then
A13:        E.s = Z.s by A12,FUNCOP_1:7;
            not ex w st w in dom (Z|z) & s = <*0*>^w & (E
            with-replacement (<*0*>,Z|z)).s = (Z|z).w by A12;
            hence thesis by A4,A9,A8,A13,TREES_2:def 11;
          end;
          suppose
            s = <*0*>;
            hence thesis by A6,A2,A10,TREES_2:def 10;
          end;
        end;
        hence thesis;
      end;
      suppose
        ex w st w in dom (Z|z) & s = <*0*>^w;
        hence thesis by A6,A2,A10,TREES_1:1,TREES_2:def 10;
      end;
    end;
    hence thesis;
  end;
  dom (E with-replacement (<*0*>,Z|z)) = e with-replacement (<*0*>, (dom
  Z)|z) by A3,A1,A2,TREES_2:def 11;
  then dom (E with-replacement (<*0*>,Z|z)) = dom Z by A5,Th22;
  hence thesis by A7,TREES_2:31;
end;

theorem Th24:
  for Z being Tree,x1,x2 be Element of Z st x1 = <*0*> & x2 = <*1
*> & succ (Root Z) = {x1,x2} holds Z = (elementary_tree 2 with-replacement (<*0
  *>,Z|x1)) with-replacement (<*1*>,Z|x2)
proof
  set e = elementary_tree 2;
  let Z be Tree,x1,x2 be Element of Z such that
A1: x1 = <*0*> and
A2: x2 = <*1*> and
A3: succ (Root Z) = {x1,x2};
  set T1 = elementary_tree 2 with-replacement (<*0*>,Z|x1);
A4: <*0*> in e by ENUMSET1:def 1,TREES_1:53;
A5: now
    let s;
    thus s in Z implies s in T1 & not <*1*> is_a_proper_prefix_of s or ex w st
    w in Z|x2 & s = <*1*>^w
    proof
      assume
A6:   s in Z;
      per cases;
      suppose
        s = {};
        hence thesis by TREES_1:12,15,22;
      end;
      suppose
        s <> {};
        then consider w be FinSequence of NAT,
         n being Element of NAT such that
A7:     s = <*n*>^w by FINSEQ_2:130;
        <*n*> is_a_prefix_of s by A7,TREES_1:1;
        then
A8:     <*n*> in Z by A6,TREES_1:20;
        <*n*> = (Root Z)^<*n*> by FINSEQ_1:34;
        then
A9:     <*n*> in succ (Root Z) by A8,TREES_2:12;
        now
          per cases by A1,A2,A3,A9,TARSKI:def 2;
          suppose
A10:        <*n*> = <*0*>;
            then w in Z|x1 by A1,A6,A7,TREES_1:def 6;
            hence thesis by A4,A7,A10,Th3,TREES_1:def 9;
          end;
          suppose
A11:        <*n*> = <*1*>;
            then w in Z|x2 by A2,A6,A7,TREES_1:def 6;
            hence thesis by A7,A11;
          end;
        end;
        hence thesis;
      end;
    end;
    assume
A12: s in T1 & not <*1*> is_a_proper_prefix_of s or ex w st w in Z|x2
    & s = <*1*>^w;
    now
      per cases by A12;
      suppose
A13:    s in T1 & not <*1*> is_a_proper_prefix_of s;
        now
          per cases by A4,A13,TREES_1:def 9;
          suppose
            s in e & not <*0*> is_a_proper_prefix_of s;
            then s = {} or s = <*0*> or s = <*1*> by ENUMSET1:def 1,TREES_1:53;
            hence s in Z by A1,A2,A3;
          end;
          suppose
            ex w st w in Z|x1 & s = <*0*>^w;
            hence s in Z by A1,TREES_1:def 6;
          end;
        end;
        hence s in Z;
      end;
      suppose
        ex w st w in Z|x2 & s = <*1*>^w;
        hence s in Z by A2,TREES_1:def 6;
      end;
    end;
    hence s in Z;
  end;
A14: now
    assume <*0*> is_a_proper_prefix_of <*1*>;
    then <*0*> is_a_prefix_of <*1*> by XBOOLE_0:def 8;
    hence contradiction by TREES_1:3;
  end;
  <*1*> in e by ENUMSET1:def 1,TREES_1:53;
  then <*1*> in T1 by A4,A14,TREES_1:def 9;
  hence thesis by A5,TREES_1:def 9;
end;

theorem Th25:
  for Z being (DecoratedTree of D),x1,x2 being Element of dom Z st
  x1 = <*0*> & x2 = <*1*> & succ (Root dom Z) = {x1,x2} holds Z = (((
elementary_tree 2) --> Root Z) with-replacement (<*0*>, Z|x1)) with-replacement
  (<*1*>,Z|x2)
proof
A1: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:52;
  set e = elementary_tree 2;
  let Z be (DecoratedTree of D),x1,x2 be Element of dom Z such that
A2: x1 = <*0*> and
A3: x2 = <*1*> and
A4: succ (Root dom Z) = {x1,x2};
A5: dom (Z|x2) = (dom Z)|x2 by TREES_2:def 10;
  set T1 = ((elementary_tree 2) --> Root Z) with-replacement (<*0*>,Z|x1);
  set E = (elementary_tree 2) --> Root Z;
A6: dom (Z|x1) = (dom Z)|x1 by TREES_2:def 10;
  set T = T1 with-replacement (<*1*>,Z|x2);
A7: <*0*> in e by ENUMSET1:def 1,TREES_1:53;
  then
A8: <*0*> in dom E by FUNCOP_1:13;
  then
A9: dom T1 = dom E with-replacement (<*0*>,dom (Z|x1)) by TREES_2:def 11;
  <*1*> in e by ENUMSET1:def 1,TREES_1:53;
  then <*1*> in dom E by FUNCOP_1:13;
  then
A10: <*1*> in dom T1 by A8,A9,A1,TREES_1:def 9;
  then
A11: dom T = dom T1 with-replacement (<*1*>,dom (Z|x2)) by TREES_2:def 11;
A12: dom E = e by FUNCOP_1:13;
  then
A13: dom T1 = e with-replacement (<*0*>,(dom Z)|x1) by A7,A6,TREES_2:def 11;
A14: for s st s in dom T holds T.s = Z.s
  proof
    let s;
    assume
A15: s in dom T;
    then
A16: not <*1*> is_a_prefix_of s & T.s = T1.s or ex u st u in dom(Z|x2) & s
    = <*1*>^u & T.s = (Z|x2).u by A10,A11,TREES_2:def 11;
    now
      per cases by A10,A11,A15,TREES_1:def 9;
      suppose
A17:    s in dom T1 & not <*1*> is_a_proper_prefix_of s;
        then
A18:    not <*0*> is_a_prefix_of s & T1.s = E.s or ex u st u in dom(Z|x1)
        & s = <*0*>^u & T1.s = (Z|x1).u by A8,A9,TREES_2:def 11;
        now
          per cases by A7,A13,A17,TREES_1:def 9;
          suppose
A19:        s in e & not <*0*> is_a_proper_prefix_of s;
            now
              per cases by A19,ENUMSET1:def 1,TREES_1:53;
              suppose
A20:            s = {};
                then
                ( not ex u st u in dom(Z|x2) & s = <*1*>^u & T.s = (Z|x2)
                .u)& E.s = Z.s by A19,FUNCOP_1:7;
                hence thesis by A10,A11,A15,A18,A20,TREES_2:def 11;
              end;
              suppose
                s = <*0*>;
                hence thesis by A2,A3,A6,A5,A16,A18,TREES_2:def 10;
              end;
              suppose
                s = <*1*>;
                hence thesis by A3,A5,A16,TREES_2:def 10;
              end;
            end;
            hence thesis;
          end;
          suppose
            ex w st w in (dom Z)|x1 & s = <*0*>^w;
            hence thesis by A2,A3,A6,A5,A16,A18,TREES_1:1,TREES_2:def 10;
          end;
        end;
        hence thesis;
      end;
      suppose
        ex w st w in dom (Z|x2) & s = <*1*>^w;
        hence thesis by A3,A5,A16,TREES_1:1,TREES_2:def 10;
      end;
    end;
    hence thesis;
  end;
  dom Z = dom T by A2,A3,A4,A12,A6,A5,A9,A11,Th24;
  hence thesis by A14,TREES_2:31;
end;

definition
  func MP-variables -> set equals
  [: {3},NAT :];
  coherence;
end;

registration
  cluster MP-variables -> non empty;
  coherence;
end;

definition
  mode MP-variable is Element of MP-variables;
end;

definition
  func MP-conectives -> set equals
  [: {0,1,2},NAT :];
  coherence;
end;

registration
  cluster MP-conectives -> non empty;
  coherence;
end;

definition
  mode MP-conective is Element of MP-conectives;
end;

theorem Th26:
  MP-conectives misses MP-variables
proof
  assume not thesis;
  then consider x being set such that
A1: x in [:{0,1,2},NAT:] and
A2: x in [:{3},NAT:] by XBOOLE_0:3;
  consider x1,x2 such that
A3: x1 in {0,1,2} and
  x2 in NAT and
A4: x = [x1,x2] by A1,ZFMISC_1:def 2;
  x1 = 3 by A2,A4,ZFMISC_1:105;
  hence contradiction by A3,ENUMSET1:def 1;
end;

reserve p,q for MP-variable;

definition
  let T be finite Tree,v be Element of T;
  redefine func branchdeg v -> Element of NAT;
  coherence
  proof
    branchdeg v = card succ v by TREES_2:def 12;
    hence thesis;
  end;
end;

definition

  func MP-WFF -> DTree-set of [: NAT,NAT :] means
  :Def5:
  (for x being DecoratedTree of [: NAT,NAT :] st x in it holds x is finite) &
  for x being finite DecoratedTree of [: NAT,NAT :] holds x in it iff
  for v being Element of dom x holds branchdeg v <= 2 &
  (branchdeg v = 0 implies x .v = [0,0] or ex k st x .v = [3,k]) &
  (branchdeg v = 1 implies x .v = [1,0] or x .v = [1,1]) &
  (branchdeg v = 2 implies x .v = [2,0]);
  existence
  proof
    deffunc F(set)=[0,0];
    set t=elementary_tree 0;
    set A = [:NAT,NAT:];
    defpred P[set] means $1 is finite DecoratedTree of A & (for y being finite
DecoratedTree of A st y = $1 holds dom y is finite & for v being Element of dom
y holds branchdeg v <= 2 & (branchdeg v = 0 implies y.v = [0,0] or ex k st y.v
= [3,k]) & (branchdeg v = 1 implies y.v = [1,0] or y.v = [1,1]) & (branchdeg v
    = 2 implies y.v = [2,0]));
    consider Y being set such that
A1: for x holds x in Y iff x in PFuncs(NAT*,A) & P[x] from XBOOLE_0:
    sch 1;
A2: for x being finite DecoratedTree of A holds x in Y iff dom x is finite
    & for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0
implies x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v =
    [1,0] or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0])
    proof
      let x be finite DecoratedTree of A;
      thus x in Y implies dom x is finite & for v being Element of dom x holds
branchdeg v <= 2 & (branchdeg v = 0 implies x .v = [0,0] or ex k st x .v = [3,k
]) & (branchdeg v = 1 implies x .v = [1,0] or x .v = [1,1]) & (branchdeg v = 2
      implies x .v = [2,0]) by A1;
      assume that
      dom x is finite and
A3:   for v being Element of dom x holds branchdeg v <= 2 & (branchdeg
v = 0 implies x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies
      x .v = [1,0] or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0]);
A4:   x in PFuncs(NAT*,A) by Th10;
      for y being finite DecoratedTree of A st y = x holds dom y is finite
      & for v being Element of dom y holds branchdeg v <= 2 & (branchdeg v = 0
implies y.v = [0,0] or ex k st y.v = [3,k]) & (branchdeg v = 1 implies y.v = [1
      ,0] or y.v = [1,1]) & (branchdeg v = 2 implies y.v = [2,0]) by A3;
      hence thesis by A1,A4;
    end;
    consider T being DecoratedTree such that
A5: dom T = t & for p being FinSequence of NAT st p in t holds T.p=F(p
    ) from TREES_2:sch 7;
    rng T c= A
    proof
      let x;
      assume x in rng T;
      then consider z being set such that
A6:   z in dom T and
A7:   x = T.z by FUNCT_1:def 3;
      z = <*>NAT by A5,A6,TARSKI:def 1,TREES_1:29;
      then reconsider z as FinSequence of NAT;
      T.z = [0,0] by A5,A6;
      hence thesis by A7;
    end;
    then reconsider T as finite DecoratedTree of A by A5,Lm2,RELAT_1:def 19;
A8: for y being finite DecoratedTree of A st y = T holds dom y is finite
    & for v being Element of dom y holds branchdeg v <= 2 & (branchdeg v = 0
implies y.v = [0,0] or ex k st y.v = [3,k]) & (branchdeg v = 1 implies y.v = [1
    ,0] or y.v = [1,1]) & (branchdeg v = 2 implies y.v = [2,0])
    proof
      let y be finite DecoratedTree of A;
      assume
A9:   y = T;
      thus dom y is finite;
      let v be Element of dom y;
A10:  succ v = {}
      proof
        set x = the Element of succ v;
        assume not thesis;
        then
A11:    x in succ v;
        succ v = { v^<*n*>: v^<*n*> in dom y } by TREES_2:def 5;
        then ex n st x = v^<*n*> & v^<*n*> in dom y by A11;
        hence contradiction by A5,A9,TARSKI:def 1,TREES_1:29;
      end;
      hence branchdeg v <= 2 by CARD_1:27,TREES_2:def 12;
      thus thesis by A5,A9,A10,CARD_1:27,TREES_2:def 12;
    end;
    T in PFuncs(NAT*,A) by Th10;
    then reconsider Y as non empty set by A1,A8;
    for x st x in Y holds x is DecoratedTree of A by A1;
    then reconsider Y as DTree-set of A by TREES_3:def 6;
    take Y;
    thus thesis by A1,A2;
  end;
  uniqueness
  proof
    let D1,D2 be DTree-set of [:NAT,NAT:] such that
A12: for x being DecoratedTree of [: NAT,NAT :] st x in D1 holds x is
    finite and
A13: for x being finite DecoratedTree of [:NAT,NAT:] holds x in D1 iff
for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0 implies
x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v = [1,0]
    or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0]) and
A14: for x being DecoratedTree of [: NAT,NAT :] st x in D2 holds x is
    finite and
A15: for x being finite DecoratedTree of [:NAT,NAT:] holds x in D2 iff
for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0 implies
x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v = [1,0]
    or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0]);
    thus D1 c= D2
    proof
      let x;
      assume
A16:  x in D1;
      reconsider y=x as finite DecoratedTree of [:NAT,NAT:] by A12,A16;
      for v being Element of dom y holds branchdeg v <= 2 & (branchdeg v
= 0 implies y.v = [0,0] or ex k st y.v = [3,k]) & (branchdeg v = 1 implies y.v
= [1 ,0] or y.v = [1,1]) & (branchdeg v = 2 implies y.v = [2,0]) by A13,A16;
      hence thesis by A15;
    end;
    let x;
    assume
A17: x in D2;
    reconsider y=x as finite DecoratedTree of [:NAT,NAT:] by A14,A17;
    for v being Element of dom y holds branchdeg v <= 2 & (branchdeg v =
0 implies y.v = [0,0] or ex k st y.v = [3,k]) & (branchdeg v = 1 implies y.v =
    [1 ,0] or y.v = [1,1]) & (branchdeg v = 2 implies y.v = [2,0]) by A15,A17;
    hence thesis by A13;
  end;
end;

:: [0,0] = VERUM
:: [1,0] = negation
:: [1,1] = modal operator of necessity
:: [2,0] = &

definition
  mode MP-wff is Element of MP-WFF;
end;

registration
  cluster -> finite for MP-wff;
  coherence by Def5;
end;

reserve A,A1,B,B1,C,C1 for MP-wff;

definition
  let A;
  let a be Element of dom A;
  redefine func A|a -> MP-wff;
  coherence
  proof
    set x = A|a;
A1: dom x = (dom A)|a by TREES_2:def 10;
    then reconsider db = dom x as finite Tree;
    reconsider x as finite DecoratedTree of [: NAT,NAT :] by A1,Lm2;
    now
      thus db is finite;
      let v be Element of db;
      set da = dom A;
      reconsider v9 = v as Element of da|a by TREES_2:def 10;
      v in db;
      then
A2:   v in da|a by TREES_2:def 10;
      then reconsider w = a^v as Element of da by TREES_1:def 6;
      succ v9,succ w are_equipotent & succ v9 = succ v by Th16,TREES_2:def 10;
      then card succ v = card succ w by CARD_1:5;
      then branchdeg v = card succ w by TREES_2:def 12;
      then
A3:   branchdeg v = branchdeg w by TREES_2:def 12;
      hence branchdeg v <= 2 by Def5;
      thus branchdeg v = 0 implies x .v = [0,0] or ex k st x .v = [3,k]
      proof
        assume
A4:     branchdeg v = 0;
        per cases by A3,A4,Def5;
        suppose
          A.w = [0,0];
          hence thesis by A2,TREES_2:def 10;
        end;
        suppose
          ex k st A.w = [3,k];
          then consider k such that
A5:       A.w = [3,k];
          now
            take k;
            thus x .v = [3,k] by A2,A5,TREES_2:def 10;
          end;
          hence thesis;
        end;
      end;
      thus branchdeg v = 1 implies x .v = [1,0] or x .v = [1,1]
      proof
        assume
A6:     branchdeg v = 1;
        per cases by A3,A6,Def5;
        suppose
          A.w = [1,0];
          hence thesis by A2,TREES_2:def 10;
        end;
        suppose
          A.w = [1,1];
          hence thesis by A2,TREES_2:def 10;
        end;
      end;
      thus branchdeg v = 2 implies x .v = [2,0]
      proof
        assume branchdeg v = 2;
        then A.w = [2,0] by A3,Def5;
        hence thesis by A2,TREES_2:def 10;
      end;
    end;
    hence thesis by Def5;
  end;
end;

definition
  let a be Element of MP-conectives;
  func the_arity_of a -> Element of NAT equals
  a`1;
  coherence
  proof
    reconsider X = {0,1,2} as non empty set;
    consider a1 being Element of X,k being Element of NAT such that
A1: a=[a1,k] by DOMAIN_1:1;
    a1 = 0 or a1 = 1 or a1 = 2 by ENUMSET1:def 1;
    hence thesis by A1,MCART_1:7;
  end;
end;

definition
  let D be non empty set, T,T1 be (DecoratedTree of D),
  p be FinSequence of NAT;
  assume
A1: p in dom T;
  func @(T,p,T1) -> DecoratedTree of D equals
  :Def7:
  T with-replacement (p,T1);
  coherence
  proof
    set X = T with-replacement (p,T1);
    rng X c= D
    proof
      let x;
      assume x in rng X;
      then consider z being set such that
A2:   z in dom X and
A3:   x = X.z by FUNCT_1:def 3;
      reconsider z as FinSequence of NAT by A2,TREES_1:19;
A4:   dom X = dom T with-replacement (p,dom T1) by A1,TREES_2:def 11;
      now
        per cases by A1,A2,A4,TREES_2:def 11;
        suppose
A5:       not p is_a_prefix_of z & X.z = T.z;
          then
not ex s being FinSequence of NAT st s in dom T1 & z = p^s by TREES_1:1;
          then reconsider z as Element of dom T by A1,A2,A4,TREES_1:def 9;
          T.z is Element of D;
          hence thesis by A3,A5;
        end;
        suppose
          ex s st s in dom T1 & z = p^s & X.z = T1.s;
          then consider s such that
A6:       s in dom T1 and
          z = p^s and
A7:       X.z = T1.s;
          reconsider s as Element of dom T1 by A6;
          T1.s is Element of D;
          hence thesis by A3,A7;
        end;
      end;
      hence thesis;
    end;
    hence thesis by RELAT_1:def 19;
  end;
end;

theorem Th27:
  ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff
proof
  reconsider d = <*0*> as Element of elementary_tree 1 by TREES_1:28;
  set x = ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A);
  <*0*> in elementary_tree 1 by TREES_1:28;
  then
A1: <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13;
  then
A2: @((elementary_tree 1) --> [1,0],<*0*>, A) = x by Def7;
  dom x = dom((elementary_tree 1) --> [1,0]) with-replacement (<*0*>, dom
  A) by A1,TREES_2:def 11;
  then dom x = elementary_tree 1 with-replacement (d,dom A) by FUNCOP_1:13;
  then reconsider x as finite DecoratedTree of [: NAT,NAT :] by A2,Lm2;
A3: dom x = dom((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,dom A
  ) by A1,TREES_2:def 11;
  for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0
implies x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v =
  [1,0] or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0])
  proof
    set e = (elementary_tree 1) --> [1,0];
    let v be Element of dom x;
    now
      per cases by A1,A3,TREES_2:def 11;
      suppose
A4:     not <*0*> is_a_prefix_of v & x .v = e.v;
A5:     dom e = {{},<*0*>} by FUNCOP_1:13,TREES_1:51;
A6:     not ex s st s in dom A & v = <*0*>^s by A4,TREES_1:1;
        then
A7:     v in dom e by A1,A3,TREES_1:def 9;
        then
A8:     v = {} by A4,A5,TARSKI:def 2;
        reconsider v9=v as Element of dom e by A1,A3,A6,TREES_1:def 9;
        now
          let x;
          thus x in succ v9 implies x in {<*0*>}
          proof
            assume x in succ v9;
            then x in { v9^<*n*> : v9^<*n*> in dom e } by TREES_2:def 5;
            then consider n such that
A9:         x = v9^<*n*> and
A10:        v9^<*n*> in dom e;
            <*n*> in dom e by A8,A10,FINSEQ_1:34;
            then
A11:        <*n*> = {} or <*n*> = <*0*> by A5,TARSKI:def 2;
            x = <*n*> by A8,A9,FINSEQ_1:34;
            hence thesis by A11,TARSKI:def 1;
          end;
          assume x in {<*0*>};
          then
A12:      x = <*0*> by TARSKI:def 1;
          then
A13:      x = v9^<*0*> by A8,FINSEQ_1:34;
          then v9^<*0*> in dom e by A5,A12,TARSKI:def 2;
          then x in { v9^<*n*> : v9^<*n*> in dom e } by A13;
          hence x in succ v9 by TREES_2:def 5;
        end;
        then
A14:    succ v9 = {<*0*>} by TARSKI:1;
        succ v= succ v9 by A1,A3,A8,Lm1,Th13;
        then 1 = card succ v by A14,CARD_1:30;
        then
A15:    branchdeg v = 1 by TREES_2:def 12;
        hence branchdeg v <= 2;
        v in elementary_tree 1 by A7;
        hence thesis by A4,A15,FUNCOP_1:7;
      end;
      suppose
        ex s st s in dom A & v = <*0*>^s & x .v = A.s;
        then consider s such that
A16:    s in dom A and
A17:    v = <*0*>^s and
A18:    x .v = A.s;
        reconsider s as Element of dom A by A16;
        succ v,succ s are_equipotent by A1,A3,A17,TREES_2:37;
        then card succ v = card succ s by CARD_1:5;
        then
A19:    branchdeg v = card succ s by TREES_2:def 12;
A20:    branchdeg s <= 2 by Def5;
        hence branchdeg v <= 2 by A19,TREES_2:def 12;
A21:    branchdeg s = 1 implies A .s = [1,0] or A .s = [1,1] by Def5;
A22:    branchdeg s = 2 implies A .s = [2,0] by Def5;
        branchdeg s = 0 implies A .s = [0,0] or ex m st A .s = [3,m] by Def5;
        hence thesis by A18,A20,A21,A22,A19,TREES_2:def 12;
      end;
    end;
    hence thesis;
  end;
  hence thesis by Def5;
end;

theorem Th28:
  ((elementary_tree 1)-->[1,1]) with-replacement (<*0*>,A) is MP-wff
proof
  reconsider d = <*0*> as Element of elementary_tree 1 by TREES_1:28;
  set x = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*> , A);
  <*0*> in elementary_tree 1 by TREES_1:28;
  then
A1: <*0*> in dom ((elementary_tree 1) --> [1,1]) by FUNCOP_1:13;
  then
  dom x = dom((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,dom A
  ) by TREES_2:def 11;
  then
A2: dom x = elementary_tree 1 with-replacement (d,dom A) by FUNCOP_1:13;
  @((elementary_tree 1) --> [1,1], <*0*> , A) = ((elementary_tree 1) --> [
  1,1]) with-replacement (<*0*> , A) by A1,Def7;
  then reconsider
  x = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*> , A)
  as finite DecoratedTree of [: NAT,NAT :] by A2,Lm2;
A3: dom x = dom((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,dom A
  ) by A1,TREES_2:def 11;
  for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0
implies x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v =
  [1,0] or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0])
  proof
    set e = (elementary_tree 1) --> [1,1];
    let v be Element of dom x;
    now
      per cases by A1,A3,TREES_2:def 11;
      suppose
A4:     not <*0*> is_a_prefix_of v & x .v = e.v;
A5:     dom e = {{},<*0*>} by FUNCOP_1:13,TREES_1:51;
A6:     not ex s st s in dom A & v = <*0*>^s by A4,TREES_1:1;
        then
A7:     v in dom e by A1,A3,TREES_1:def 9;
        then
A8:     v = {} by A4,A5,TARSKI:def 2;
        reconsider v9=v as Element of dom e by A1,A3,A6,TREES_1:def 9;
        now
          let x;
          thus x in succ v9 implies x in {<*0*>}
          proof
            assume x in succ v9;
            then x in { v9^<*n*> : v9^<*n*> in dom e } by TREES_2:def 5;
            then consider n such that
A9:         x = v9^<*n*> and
A10:        v9^<*n*> in dom e;
            <*n*> in dom e by A8,A10,FINSEQ_1:34;
            then
A11:        <*n*> = {} or <*n*> = <*0*> by A5,TARSKI:def 2;
            x = <*n*> by A8,A9,FINSEQ_1:34;
            hence thesis by A11,TARSKI:def 1;
          end;
          assume x in {<*0*>};
          then
A12:      x = <*0*> by TARSKI:def 1;
          then
A13:      x = v9^<*0*> by A8,FINSEQ_1:34;
          then v9^<*0*> in dom e by A5,A12,TARSKI:def 2;
          then x in { v9^<*n*> : v9^<*n*> in dom e } by A13;
          hence x in succ v9 by TREES_2:def 5;
        end;
        then
A14:    succ v9 = {<*0*>} by TARSKI:1;
        succ v= succ v9 by A1,A3,A8,Lm1,Th13;
        then 1 = card succ v by A14,CARD_1:30;
        then
A15:    branchdeg v = 1 by TREES_2:def 12;
        hence branchdeg v <= 2;
        v in elementary_tree 1 by A7;
        hence thesis by A4,A15,FUNCOP_1:7;
      end;
      suppose
        ex s st s in dom A & v = <*0*>^s & x .v = A.s;
        then consider s such that
A16:    s in dom A and
A17:    v = <*0*>^s and
A18:    x .v = A.s;
        reconsider s as Element of dom A by A16;
        succ v,succ s are_equipotent by A1,A3,A17,TREES_2:37;
        then card succ v = card succ s by CARD_1:5;
        then
A19:    branchdeg v = card succ s by TREES_2:def 12;
A20:    branchdeg s <= 2 by Def5;
        hence branchdeg v <= 2 by A19,TREES_2:def 12;
A21:    branchdeg s = 1 implies A .s = [1,0] or A .s = [1,1] by Def5;
A22:    branchdeg s = 2 implies A .s = [2,0] by Def5;
        branchdeg s = 0 implies A .s = [0,0] or ex m st A .s = [3,m] by Def5;
        hence thesis by A18,A20,A21,A22,A19,TREES_2:def 12;
      end;
    end;
    hence thesis;
  end;
  hence thesis by Def5;
end;

theorem Th29:
  (((elementary_tree 2)-->[2,0]) with-replacement (<*0*>,A))
  with-replacement (<*1*>,B) is MP-wff
proof
  reconsider d =<*0*> as Element of elementary_tree 2 by TREES_1:28;
  set y = ((elementary_tree 2)-->[2,0]) with-replacement (<*0*>,A);
  set x = y with-replacement (<*1*>,B);
A1: not <*0*> is_a_proper_prefix_of <*1*>
  proof
    assume not thesis;
    then <*0*> is_a_prefix_of <*1*> by XBOOLE_0:def 8;
    hence contradiction by TREES_1:3;
  end;
  reconsider db = dom B as finite Tree;
  reconsider da = dom A as finite Tree;
  <*0*> in elementary_tree 2 by TREES_1:28;
  then
A2: <*0*> in dom((elementary_tree 2)-->[2,0]) by FUNCOP_1:13;
  then @((elementary_tree 2) --> [2,0],<*0*>,A) = y by Def7;
  then reconsider y as DecoratedTree of [: NAT,NAT :];
A3: dom y = dom((elementary_tree 2)-->[2,0]) with-replacement (<*0*>,dom A)
  by A2,TREES_2:def 11;
  dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 by FUNCOP_1:13;
  then dom y = (elementary_tree 2) with-replacement(d,da) by TREES_2:def 11;
  then reconsider dy = dom y as finite Tree;
  <*1*> in elementary_tree 2 by TREES_1:28;
  then
A4: <*1*> in dom((elementary_tree 2)-->[2,0]) by FUNCOP_1:13;
  then
A5: <*1*> in dom y by A2,A3,A1,TREES_1:def 9;
  reconsider d1 = <*1*> as Element of dy by A2,A3,A4,A1,TREES_1:def 9;
  dom x = dy with-replacement (d1,db) & @(y,<*1*>,B) = x by A5,Def7,
TREES_2:def 11;
  then reconsider x as finite DecoratedTree of [: NAT,NAT :] by Lm2;
A6: dom x = dom y with-replacement (<*1*>,dom B) by A5,TREES_2:def 11;
  for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0
implies x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v =
  [1,0] or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0])
  proof
    set e = (elementary_tree 2)-->[2,0];
    let v be Element of dom x;
    now
      per cases by A5,A6,TREES_2:def 11;
      suppose
A7:     not <*1*> is_a_prefix_of v & x .v = y .v;
        then
A8:     not ex s st s in dom B & v = <*1*>^s by TREES_1:1;
        then
A9:     v in dom e with-replacement (<*0*>,dom A) by A3,A5,A6,TREES_1:def 9;
        now
          per cases by A2,A9,TREES_2:def 11;
          suppose
A10:        not <*0*> is_a_prefix_of v & y.v = e.v;
A11:        dom e = {{},<*0*>,<*1*>} by FUNCOP_1:13,TREES_1:53;
A12:        not ex s st s in dom A & v = <*0*>^s by A10,TREES_1:1;
            then
A13:        v in dom e by A2,A9,TREES_1:def 9;
            then
A14:        v = {} by A7,A10,A11,ENUMSET1:def 1;
            reconsider v9=v as Element of dom e by A2,A9,A12,TREES_1:def 9;
A15:        succ v = succ v9
            proof
              reconsider v99 = v as Element of dom y by A5,A6,A8,TREES_1:def 9
;
              succ v99 = succ v9 by A2,A3,A14,Lm1,Th13;
              hence thesis by A5,A6,A14,Lm1,Th13;
            end;
            now
              let x;
              thus x in succ v9 implies x in {<*0*>,<*1*>}
              proof
                assume x in succ v9;
                then x in { v9^<*n*> : v9^<*n*> in dom e } by TREES_2:def 5;
                then consider n such that
A16:            x = v9^<*n*> and
A17:            v9^<*n*> in dom e;
                <*n*> in dom e by A14,A17,FINSEQ_1:34;
                then
A18:            <*n*> = {} or <*n*> = <*0*> or <*n*> = <*1*> by A11,
ENUMSET1:def 1;
                x = <*n*> by A14,A16,FINSEQ_1:34;
                hence thesis by A18,TARSKI:def 2;
              end;
              assume x in {<*0*>,<*1*>};
              then
A19:          x = <*0*> or x = <*1*> by TARSKI:def 2;
              now
                per cases by A14,A19,FINSEQ_1:34;
                suppose
A20:              x = v9^<*0*>;
                  then v9^<*0*> in dom e by A11,A19,ENUMSET1:def 1;
                  then x in { v9^<*n*> : v9^<*n*> in dom e } by A20;
                  hence x in succ v9 by TREES_2:def 5;
                end;
                suppose
A21:              x = v9^<*1*>;
                  then v9^<*1*> in dom e by A11,A19,ENUMSET1:def 1;
                  then x in { v9^<*n*> : v9^<*n*> in dom e } by A21;
                  hence x in succ v9 by TREES_2:def 5;
                end;
              end;
              hence x in succ v9;
            end;
            then
A22:        succ v9 = {<*0*>,<*1*>} by TARSKI:1;
            <*0*> <> <*1*> by TREES_1:3;
            then
A23:        2 = card succ v by A22,A15,CARD_2:57;
            hence branchdeg v <= 2 by TREES_2:def 12;
            v in elementary_tree 2 by A13;
            hence thesis by A7,A10,A23,FUNCOP_1:7,TREES_2:def 12;
          end;
          suppose
            ex s st s in dom A & v = <*0*>^s & y.v = A.s;
            then consider s such that
A24:        s in dom A and
A25:        v = <*0*>^s and
A26:        y.v = A.s;
            reconsider s as Element of dom A by A24;
            succ v,succ s are_equipotent
            proof
              reconsider v9=v as Element of dom y by A5,A6,A8,TREES_1:def 9;
              succ v9,succ s are_equipotent by A2,A3,A25,TREES_2:37;
              hence thesis by A5,A6,A25,Th1,Th14;
            end;
            then card succ v = card succ s by CARD_1:5;
            then
A27:        branchdeg v = card succ s by TREES_2:def 12;
A28:        branchdeg s <= 2 by Def5;
            hence branchdeg v <= 2 by A27,TREES_2:def 12;
A29:        branchdeg s = 1 implies A .s = [1,0] or A .s = [1,1] by Def5;
A30:        branchdeg s = 2 implies A .s = [2,0] by Def5;
            branchdeg s = 0 implies A .s = [0,0] or ex m st A .s = [3,m]
            by Def5;
            hence thesis by A7,A26,A28,A29,A30,A27,TREES_2:def 12;
          end;
        end;
        hence thesis;
      end;
      suppose
        ex s st s in dom B & v = <*1*>^s & x .v = B.s;
        then consider s such that
A31:    s in dom B and
A32:    v = <*1*>^s and
A33:    x .v = B.s;
        reconsider s as Element of dom B by A31;
        succ v,succ s are_equipotent by A5,A6,A32,TREES_2:37;
        then card succ v = card succ s by CARD_1:5;
        then
A34:    branchdeg v = card succ s by TREES_2:def 12;
A35:    branchdeg s = 2 implies B .s = [2,0] by Def5;
A36:    branchdeg s = 1 implies B .s = [1,0] or B .s = [1,1] by Def5;
A37:    branchdeg s = 0 implies B .s = [0,0] or ex m st B .s = [3,m] by Def5;
        branchdeg s <= 2 by Def5;
        hence thesis by A33,A37,A36,A35,A34,TREES_2:def 12;
      end;
    end;
    hence thesis;
  end;
  hence thesis by Def5;
end;

definition
  let A;
  func 'not' A -> MP-wff equals
  ((elementary_tree 1)-->[1,0]) with-replacement
  (<*0*>,A);
  coherence by Th27;
  func (#) A -> MP-wff equals
  ((elementary_tree 1)-->[1,1]) with-replacement (
  <*0*>,A);
  coherence by Th28;
  let B;
  func A '&' B -> MP-wff equals
  ((((elementary_tree 2)-->[2,0])
  with-replacement (<*0*>,A))) with-replacement (<*1*>,B);
  coherence by Th29;
end;

definition
  let A;
  func ? A -> MP-wff equals
  'not' (#) 'not' A;
  correctness;
  let B;
  func A 'or' B -> MP-wff equals
  'not'('not' A '&' 'not' B);
  correctness;
  func A => B -> MP-wff equals
  'not'(A '&' 'not' B);
  correctness;
end;

theorem Th30:
  (elementary_tree 0) --> [3,n] is MP-wff
proof
  set x = (elementary_tree 0) --> [3,n];
A1: dom x = { {} } by FUNCOP_1:13,TREES_1:29;
  reconsider x as finite DecoratedTree of [: NAT,NAT :];
A2: dom x = elementary_tree 0 by FUNCOP_1:13;
  for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0
implies x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v =
  [1,0] or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0])
  proof
    let v be Element of dom x;
A3: succ v = {}
    proof
      set y = the Element of succ v;
      assume not thesis;
      then y in succ v;
      then y in { v^<*m*> : v^<*m*> in dom x } by TREES_2:def 5;
      then ex m st y = v^<*m*> & v^<*m*> in dom x;
      hence contradiction by A1,TARSKI:def 1;
    end;
    hence branchdeg v <= 2 by CARD_1:27,TREES_2:def 12;
    thus branchdeg v = 0 implies x .v = [0,0] or ex m st x .v =[3,m] by A2,
FUNCOP_1:7;
    thus thesis by A3,CARD_1:27,TREES_2:def 12;
  end;
  hence thesis by Def5;
end;

theorem Th31:
  (elementary_tree 0) --> [0,0] is MP-wff
proof
  set x = (elementary_tree 0) --> [0,0];
  reconsider x as finite DecoratedTree of [: NAT,NAT :];
A1: dom x = { {} } by FUNCOP_1:13,TREES_1:29;
A2: dom x = elementary_tree 0 by FUNCOP_1:13;
  for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0
implies x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v =
  [1,0] or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0])
  proof
    let v be Element of dom x;
A3: succ v = {}
    proof
      set y = the Element of succ v;
      assume not thesis;
      then y in succ v;
      then y in { v^<*m*> : v^<*m*> in dom x } by TREES_2:def 5;
      then ex m st y = v^<*m*> & v^<*m*> in dom x;
      hence contradiction by A1,TARSKI:def 1;
    end;
    hence branchdeg v <= 2 by CARD_1:27,TREES_2:def 12;
    thus thesis by A2,A3,CARD_1:27,FUNCOP_1:7,TREES_2:def 12;
  end;
  hence thesis by Def5;
end;

definition
  let p;
  func @p -> MP-wff equals
  (elementary_tree 0) --> p;
  coherence
  proof
    consider x1,x2 such that
A1: x1 in {3} and
A2: x2 in NAT & p = [x1,x2] by ZFMISC_1:def 2;
    x1 = 3 by A1,TARSKI:def 1;
    hence thesis by A2,Th30;
  end;
end;

theorem Th32:
  @p = @q implies p = q
proof
  assume
A1: @p = @q;
A2: {} in elementary_tree 0 by TREES_1:22;
  then p = @p.{} by FUNCOP_1:7
    .= q by A2,A1,FUNCOP_1:7;
  hence thesis;
end;

Lm3: <*0*> in dom ((elementary_tree 1)-->[n,m])
proof
  <*0*> in elementary_tree 1 by TARSKI:def 2,TREES_1:51;
  hence thesis by FUNCOP_1:13;
end;

theorem Th33:
  'not' A = 'not' B implies A = B
proof
  assume
A1: 'not' A = 'not' B;
  <*0*> in dom((elementary_tree 1)-->[1,0]) by Lm3;
  hence thesis by A1,Th12;
end;

theorem Th34:
  (#)A = (#)B implies A = B
proof
  set AA = (elementary_tree 1)-->[1,1];
  assume
A1: (#)A = (#)B;
  <*0*> in dom AA by Lm3;
  hence thesis by A1,Th12;
end;

theorem Th35:
  (A '&' B) = (A1 '&' B1) implies A = A1 & B = B1
proof
  set e = elementary_tree 2;
  set y = (e-->[2,0]) with-replacement (<*0*>,A);
  set y1 = (e-->[2,0]) with-replacement (<*0*>,A1);
  assume
A1: A '&' B = A1 '&' B1;
A2: <*1*> in e by TREES_1:28;
A3: <*0*> in e & dom (e --> [2,0]) = e by FUNCOP_1:13,TREES_1:28;
  then
A4: dom y1 = dom(e-->[2,0]) with-replacement (<*0*>,dom A1) by TREES_2:def 11;
  not <*1*> is_a_proper_prefix_of <*0*> by TREES_1:52;
  then
A5: <*0*> in dom(e-->[2,0]) with-replacement (<*1*>,dom B) by A2,A3,
TREES_1:def 9;
A6: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:52;
  then
A7: <*1*> in dom y1 by A2,A3,A4,TREES_1:def 9;
A8: dom y = dom(e-->[2,0]) with-replacement (<*0*>,dom A) by A3,TREES_2:def 11;
  then
A9: <*1*> in dom y by A2,A3,A6,TREES_1:def 9;
  then
A10: dom (A '&' B) = dom y with-replacement (<*1*>,dom B) by TREES_2:def 11;
A11: dom (A1 '&' B1) = dom y1 with-replacement (<*1*>,dom B1) by A7,
TREES_2:def 11;
  now
    let s;
    thus s in dom B implies s in dom B1
    proof
      assume s in dom B;
      then
A12:  <*1*>^s in dom(A1 '&' B1) by A1,A9,A10,TREES_1:def 9;
      now
        per cases;
        suppose
          s = {};
          hence thesis by TREES_1:22;
        end;
        suppose
          s <> {};
          then <*1*> is_a_proper_prefix_of <*1*>^s by TREES_1:10;
          then ex w st w in dom B1 & <*1*>^s = <*1*>^w by A7,A11,A12,
TREES_1:def 9;
          hence thesis by FINSEQ_1:33;
        end;
      end;
      hence thesis;
    end;
    assume s in dom B1;
    then
A13: <*1*>^s in dom(A '&' B) by A1,A7,A11,TREES_1:def 9;
    now
      per cases;
      suppose
        s = {};
        hence s in dom B by TREES_1:22;
      end;
      suppose
        s <> {};
        then <*1*> is_a_proper_prefix_of <*1*>^s by TREES_1:10;
        then ex w st w in dom B & <*1*>^s = <*1*>^w by A9,A10,A13,TREES_1:def 9
;
        hence s in dom B by FINSEQ_1:33;
      end;
    end;
    hence s in dom B;
  end;
  then
A14: dom B = dom B1 by TREES_2:def 1;
A15: for s st s in dom B holds B.s = B1.s
  proof
    let s;
    assume s in dom B;
    then
A16: <*1*>^s in dom(A1 '&' B1) by A1,A9,A10,TREES_1:def 9;
A17: <*1*> is_a_prefix_of <*1*>^s by TREES_1:1;
    then consider w such that
    w in dom B1 and
A18: <*1*>^s = <*1*>^w and
A19: (A1 '&' B1).(<*1*>^s) = B1.w by A7,A11,A16,TREES_2:def 11;
A20: ex u st u in dom B & <*1*>^s = <*1*>^u & (A '&' B).(<*1*>^s) = B.u by A1
,A9,A10,A16,A17,TREES_2:def 11;
    s = w by A18,FINSEQ_1:33;
    hence thesis by A1,A19,A20,FINSEQ_1:33;
  end;
  then
A21: B = B1 by A14,TREES_2:31;
A22: not <*0*>,<*1*> are_c=-comparable by TREES_1:5;
  then
A23: dom (A '&' B) = (dom(e-->[2,0]) with-replacement (<*1*>,dom B))
  with-replacement (<*0*>,dom A) by A2,A3,A8,A10,TREES_2:8;
A24: dom (A1 '&' B1) = (dom(e-->[2,0]) with-replacement (<*1*>,dom B))
  with-replacement (<*0*>,dom A1) by A22,A2,A3,A4,A11,A14,TREES_2:8;
  then
A25: dom A = dom A1 by A1,A5,A23,Th11;
  for s st s in dom A holds A.s = A1.s
  proof
    let s;
    assume
A26: s in dom A;
    then
A27: <*0*>^s in dom y by A3,A8,TREES_1:def 9;
A28: <*0*> is_a_prefix_of <*0*>^s by TREES_1:1;
    then
A29: ex w st w in dom A & <*0*>^s = <*0*>^w & y.(<*0*>^s) = A.w by A3,A8,A27,
TREES_2:def 11;
    <*0*>^s in dom y1 by A3,A4,A25,A26,TREES_1:def 9;
    then
A30: ex u st u in dom A1 & <*0*>^s = <*0*>^u & y1.(<*0*>^s) = A1.u by A3,A4,A28
,TREES_2:def 11;
    not <*1*> is_a_proper_prefix_of <*0*>^s by Th3;
    then
A31: <*0*>^s in dom (A '&' B) by A9,A10,A27,TREES_1:def 9;
    now
      given w such that
      w in dom B and
A32:  <*0*>^s = <*1*>^w and
      (A '&' B).(<*0*>^s) = B.w;
      <*0*> is_a_prefix_of <*1*>^w by A32,TREES_1:1;
      hence contradiction by TREES_1:50;
    end;
    then (A '&' B).(<*0*>^s) = y.(<*0*> ^s) by A9,A10,A31,TREES_2:def 11;
    then
A33: A.s = (A1 '&' B).(<*0*>^s) by A1,A21,A29,FINSEQ_1:33;
    now
      given w such that
      w in dom B1 and
A34:  <*0*>^s = <*1*>^w and
      (A1 '&' B1).(<*0*>^s) = B1.w;
      <*0*> is_a_prefix_of <*1*>^w by A34,TREES_1:1;
      hence contradiction by TREES_1:50;
    end;
    then (A1 '&' B1).(<*0*>^s) = y1.(<* 0*>^s) by A1,A7,A11,A31,TREES_2:def 11;
    hence thesis by A21,A33,A30,FINSEQ_1:33;
  end;
  hence thesis by A1,A5,A14,A23,A24,A15,Th11,TREES_2:31;
end;

definition
  func VERUM -> MP-wff equals
  (elementary_tree 0) --> [0,0];
  coherence by Th31;
end;

theorem Th36:
  card dom A = 1 implies A = VERUM or ex p st A = @p
proof
  assume card dom A = 1;
  then consider x such that
A1: dom A = {x} by CARD_2:42;
  reconsider x as Element of dom A by A1,TARSKI:def 1;
A2: {} in dom A by TREES_1:22;
  then
A3: dom A = elementary_tree 0 by A1,TARSKI:def 1,TREES_1:29;
A4: dom A = {{}} by A2,A1,TARSKI:def 1;
  succ x = {}
  proof
    set y = the Element of succ x;
    assume not thesis;
    then
A5: y in succ x;
    succ x = { x^<*n*>: x^<*n*> in dom A } by TREES_2:def 5;
    then ex n st y = x^<*n*> & x^<*n*> in dom A by A5;
    hence contradiction by A4,TARSKI:def 1;
  end;
  then
A6: branchdeg x = 0 by CARD_1:27,TREES_2:def 12;
  now
    per cases by A6,Def5;
    suppose
      A.x = [0,0];
      then for z holds z in dom A implies A.z = [0,0] by A1,TARSKI:def 1;
      hence thesis by A3,FUNCOP_1:11;
    end;
    suppose
      ex n st A.x = [3,n];
      then consider n such that
A7:   A.x = [3,n];
      reconsider p = [3,n] as MP-variable by ZFMISC_1:105;
      for z holds z in dom A implies A.z = [3,n] by A1,A7,TARSKI:def 1;
      then A = @p by A3,FUNCOP_1:11;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem Th37:
  card dom A >= 2 implies (ex B st A = 'not' B or A = (#)B) or ex
  B,C st A = B '&' C
proof
  set b = branchdeg (Root dom A);
  set a = Root dom A;
  assume
A1: card dom A >= 2;
A2: now
    assume b = 0;
    then card dom A = 1 by Th17;
    hence contradiction by A1;
  end;
A3: b <= 2 by Def5;
  now
    per cases by A3,A2,NAT_1:26;
    case
A4:   b = 1;
      then card succ a = 1 by TREES_2:def 12;
      then consider x such that
A5:   succ a = {x} by CARD_2:42;
      x in succ a by A5,TARSKI:def 1;
      then reconsider x9 = x as Element of dom A;
      take B = A|x9;
      now
        per cases by A4,Def5;
        suppose
          A.a = [1,0];
          then Root A = [1,0];
          hence A = 'not' B or A = (#) B by A5,Th23;
        end;
        suppose
          A.a = [1,1];
          then Root A = [1,1];
          hence A = 'not' B or A = (#) B by A5,Th23;
        end;
      end;
      hence thesis;
    end;
    case
A6:   b = 2;
      then
A7:   succ a = { <*0*>,<*1*> } by Th19;
      then <*0*> in succ a & <*1*> in succ a by TARSKI:def 2;
      then reconsider x = <*0*>, y = <*1*> as Element of dom A;
      take B = A|x;
      take C = A|y;
      Root A = [2,0] by A6,Def5;
      then A = B '&' C by A7,Th25;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem Th38:
  card dom A < card dom 'not' A
proof
  set e = elementary_tree 1;
  <*0*> in e by TARSKI:def 2,TREES_1:51;
  then
A1: <*0*> in dom (e --> [1,0]) by FUNCOP_1:13;
  then
A2: dom 'not' A = dom (e --> [1,0]) with-replacement (<*0*>, dom A) by
TREES_2:def 11;
  then reconsider o = <*0*> as Element of dom 'not' A by A1,TREES_1:def 9;
  now
    let s;
    thus s in dom A implies o^s in dom 'not' A by A1,A2,TREES_1:def 9;
    assume
A3: o^s in dom 'not' A;
    now
      per cases;
      suppose
        s = {};
        hence s in dom A by TREES_1:22;
      end;
      suppose
        s <> {};
        then o is_a_proper_prefix_of o^s by TREES_1:10;
        then ex w st w in dom A & o^s = o^w by A1,A2,A3,TREES_1:def 9;
        hence s in dom A by FINSEQ_1:33;
      end;
    end;
    hence s in dom A;
  end;
  then
A4: dom A = (dom 'not' A)|o by TREES_1:def 6;
  o <> Root (dom 'not' A);
  hence thesis by A4,Th21;
end;

theorem Th39:
  card dom A < card dom (#)A
proof
  set e = elementary_tree 1;
  <*0*> in e by TARSKI:def 2,TREES_1:51;
  then
A1: <*0*> in dom (e --> [1,1]) by FUNCOP_1:13;
  then
A2: dom (#)A = dom (e --> [1,1]) with-replacement (<*0*>, dom A) by
TREES_2:def 11;
  then reconsider o = <*0*> as Element of dom (#)A by A1,TREES_1:def 9;
  now
    let s;
    thus s in dom A implies o^s in dom (#)A by A1,A2,TREES_1:def 9;
    assume
A3: o^s in dom (#)A;
    now
      per cases;
      suppose
        s = {};
        hence s in dom A by TREES_1:22;
      end;
      suppose
        s <> {};
        then o is_a_proper_prefix_of o^s by TREES_1:10;
        then ex w st w in dom A & o^s = o^w by A1,A2,A3,TREES_1:def 9;
        hence s in dom A by FINSEQ_1:33;
      end;
    end;
    hence s in dom A;
  end;
  then
A4: dom A = (dom (#)A)|o by TREES_1:def 6;
  o <> Root (dom (#)A);
  hence thesis by A4,Th21;
end;

theorem Th40:
  card dom A < card dom(A '&' B) & card dom B < card dom (A '&' B)
proof
  set e = elementary_tree 2;
  set y = (e-->[2,0]) with-replacement(<*0*>,A);
A1: not <*1*> is_a_proper_prefix_of <*0*> by TREES_1:52;
A2: <*0*> in e & dom (e --> [2,0]) = e by FUNCOP_1:13,TREES_1:28;
  then
A3: dom y = dom(e-->[2,0]) with-replacement (<*0*>,dom A) by TREES_2:def 11;
  <*1*> in e & not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:28,52;
  then
A4: <*1*> in dom y by A2,A3,TREES_1:def 9;
  then
A5: dom (A '&' B) = dom y with-replacement (<*1*>,dom B) by TREES_2:def 11;
  then reconsider u = <*1*> as Element of dom(A '&' B) by A4,TREES_1:def 9;
  <*0*> in dom y by A2,A3,TREES_1:def 9;
  then reconsider o = <*0*> as Element of dom(A '&' B) by A4,A5,A1,
TREES_1:def 9;
  now
    let s;
    thus s in dom A implies o^s in dom(A '&' B)
    proof
      assume s in dom A;
      then
A6:   o^s in dom y by A2,A3,TREES_1:def 9;
      not <*1*> is_a_proper_prefix_of o^s by Th3;
      hence thesis by A4,A5,A6,TREES_1:def 9;
    end;
    assume
A7: o^s in dom(A '&' B);
    now
      per cases;
      suppose
        s = {};
        hence s in dom A by TREES_1:22;
      end;
      suppose
A8:     s <> {};
        now
          given w such that
          w in dom B and
A9:       o^s = <*1*>^w;
          o is_a_prefix_of <*1*>^w by A9,TREES_1:1;
          hence contradiction by TREES_1:50;
        end;
        then
A10:    o^s in dom y by A4,A5,A7,TREES_1:def 9;
        o is_a_proper_prefix_of o^s by A8,TREES_1:10;
        then ex w st w in dom A & o^s = o^w by A2,A3,A10,TREES_1:def 9;
        hence s in dom A by FINSEQ_1:33;
      end;
    end;
    hence s in dom A;
  end;
  then
A11: dom A = (dom(A '&' B))|o by TREES_1:def 6;
  now
    let s;
    thus s in dom B implies u^s in dom(A '&' B) by A4,A5,TREES_1:def 9;
    assume
A12: u^s in dom(A '&' B);
    now
      per cases;
      suppose
        s = {};
        hence s in dom B by TREES_1:22;
      end;
      suppose
        s <> {};
        then <*1*> is_a_proper_prefix_of u^s by TREES_1:10;
        then ex w st w in dom B & u^s = <*1*>^w by A4,A5,A12,TREES_1:def 9;
        hence s in dom B by FINSEQ_1:33;
      end;
    end;
    hence s in dom B;
  end;
  then
A13: dom B = (dom(A '&' B))|u by TREES_1:def 6;
  o <> Root (dom(A '&' B));
  hence card dom A < card dom(A '&' B) by A11,Th21;
  u <> Root (dom(A '&' B));
  hence thesis by A13,Th21;
end;

definition
  let IT be MP-wff;
  attr IT is atomic means
  :Def16:
  ex p st IT = @p;
  attr IT is negative means
  :Def17:
  ex A st IT = 'not' A;
  attr IT is necessitive means
  :Def18:
  ex A st IT = (#) A;
  attr IT is conjunctive means
  :Def19:
  ex A,B st IT = A '&' B;
end;

registration
  cluster atomic for MP-wff;
  existence
  proof
    reconsider p = [3,0] as MP-variable by ZFMISC_1:105;
    take @p;
    take p;
    thus thesis;
  end;
  cluster negative for MP-wff;
  existence
  proof
    set A = VERUM;
    take 'not' A;
    take A;
    thus thesis;
  end;
  cluster necessitive for MP-wff;
  existence
  proof
    set A = VERUM;
    take (#)A;
    take A;
    thus thesis;
  end;
  cluster conjunctive for MP-wff;
  existence
  proof
    set B = VERUM;
    set A = VERUM;
    take A '&' B;
    take B;
    take A;
    thus thesis;
  end;
end;

scheme
  MPInd { Prop[Element of MP-WFF] }: for A being Element of MP-WFF holds Prop[
  A]
provided
A1: Prop[VERUM] and
A2: for p being MP-variable holds Prop[@p] and
A3: for A being Element of MP-WFF st Prop[A] holds Prop['not' A] and
A4: for A being Element of MP-WFF st Prop[A] holds Prop[(#) A] and
A5: for A, B being Element of MP-WFF st Prop[A] & Prop[B] holds Prop[A '&' B]
proof
  defpred P[Element of NAT] means for A st card dom A <= $1 holds Prop[A];
A6: for k st P[k] holds P[k+1]
  proof
    let k such that
A7: for A st card dom A <= k holds Prop[A];
    let A such that
A8: card dom A <= k + 1;
    set a = Root dom A;
    set b = branchdeg a;
A9: b <= 2 by Def5;
    now
      per cases by A9,NAT_1:26;
      suppose
        b = 0;
        then
A10:    card dom A = 1 by Th17;
        now
          per cases by A10,Th36;
          suppose
            A = VERUM;
            hence thesis by A1;
          end;
          suppose
            ex p st A = @p;
            hence thesis by A2;
          end;
        end;
        hence thesis;
      end;
      suppose
A11:    b = 1;
        then
A12:    succ a ={<*0*>} by Th18;
        then <*0*> in succ a by TARSKI:def 1;
        then reconsider o = <*0*> as Element of dom A;
A13:    A = ((elementary_tree 1) --> Root A) with-replacement (<*0*>, A|o
        ) by A12,Th23;
        now
          per cases by A11,Def5;
          suppose
A14:        A.a = [1,0];
            dom (A|o) = (dom A)|o & o <> Root dom A by TREES_2:def 10;
            then card dom (A|o) < k + 1 by A8,Th21,XXREAL_0:2;
            then
A15:        card dom (A|o) <= k by NAT_1:13;
            A = 'not'(A|o) by A13,A14;
            hence thesis by A3,A7,A15;
          end;
          suppose
A16:        A.a = [1,1];
            dom (A|o) = (dom A)|o & o <> Root dom A by TREES_2:def 10;
            then card dom (A|o) < k + 1 by A8,Th21,XXREAL_0:2;
            then
A17:        card dom (A|o) <= k by NAT_1:13;
            A = (#)(A|o) by A13,A16;
            hence thesis by A4,A7,A17;
          end;
        end;
        hence thesis;
      end;
      suppose
A18:    b = 2;
        then
A19:    succ a ={<*0*>,<*1*>} by Th19;
        then <*0*> in succ a & <*1*> in succ a by TARSKI:def 2;
        then reconsider o1 = <*0*>, o2 = <*1*> as Element of dom A;
        dom (A|o1) = (dom A)|o1 & o1 <> Root dom A by TREES_2:def 10;
        then card dom (A|o1) < k + 1 by A8,Th21,XXREAL_0:2;
        then card dom (A|o1) <= k by NAT_1:13;
        then
A20:    Prop[A|o1] by A7;
        dom (A|o2) = (dom A)|o2 & o2 <> Root dom A by TREES_2:def 10;
        then card dom (A|o2) < k + 1 by A8,Th21,XXREAL_0:2;
        then card dom (A|o2) <= k by NAT_1:13;
        then
A21:    Prop[A|o2] by A7;
        A = ((elementary_tree 2) --> Root A) with-replacement (<*0*>, A|
        o1) with-replacement (<*1*>,A|o2) by A19,Th25;
        then A = (A|o1) '&' (A|o2) by A18,Def5;
        hence thesis by A5,A20,A21;
      end;
    end;
    hence thesis;
  end;
  let A;
A22: card dom A <= card dom A;
A23: P[0] by NAT_1:2;
  for n holds P[n] from NAT_1:sch 1(A23,A6);
  hence thesis by A22;
end;

theorem
  for A being Element of MP-WFF holds A = VERUM or A is atomic MP-wff or
  A is negative MP-wff or A is necessitive MP-wff or A is conjunctive MP-wff
proof
  defpred Prop[Element of MP-WFF] means $1 = VERUM or $1 is atomic MP-wff or
$1 is negative MP-wff or $1 is necessitive MP-wff or $1 is conjunctive MP-wff;
A1: Prop[VERUM];
A2: for A being Element of MP-WFF st Prop[A] holds Prop['not' A] by Def17;
A3: for A,B being Element of MP-WFF st Prop[A] & Prop[B] holds Prop[A '&' B]
  by Def19;
A4: for A being Element of MP-WFF st Prop[A] holds Prop[(#) A] by Def18;
A5: for p being MP-variable holds Prop[@p] by Def16;
  thus for A be Element of MP-WFF holds Prop[A] from MPInd(A1,A5, A2,A4,A3);
end;

theorem Th42:
  A = VERUM or (ex p st A = @p) or (ex B st A = 'not' B) or (ex B
  st A = (#) B) or ex B,C st A = B '&' C
proof
  now
    per cases by NAT_1:26;
    suppose
      card dom A = 1;
      hence thesis by Th36;
    end;
    suppose
      card dom A >= 2;
      hence thesis by Th37;
    end;
  end;
  hence thesis;
end;

theorem Th43:
  @p <> 'not' A & @p <> (#)A & @p <> A '&' B
proof
  set e2 = elementary_tree 2;
  set e1 = elementary_tree 1;
  set e0 = elementary_tree 0;
A1: dom @p = e0 by FUNCOP_1:13;
A2: <*0*> in e1 by TARSKI:def 2,TREES_1:51;
  dom (e1 --> [1,0]) = e1 by FUNCOP_1:13;
  then dom ('not' A) = e1 with-replacement (<*0*>,dom A) by A2,TREES_2:def 11;
  then <*0*> in dom ('not' A) by A2,TREES_1:def 9;
  hence @p <> 'not' A by A1,TARSKI:def 1,TREES_1:29;
  dom (e1 --> [1,1]) = e1 by FUNCOP_1:13;
  then dom ((#)A) = e1 with-replacement (<*0*>,dom A) by A2,TREES_2:def 11;
  then <*0*> in dom ((#)A) by A2,TREES_1:def 9;
  hence @p <> (#)A by A1,TARSKI:def 1,TREES_1:29;
  set y = (e2-->[2,0]) with-replacement (<*0*>,A);
A3: <*1*> in e2 & not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:28,52;
A4: <*0*> in e2 & dom (e2 --> [2,0]) = e2 by FUNCOP_1:13,TREES_1:28;
  then dom y = dom(e2-->[2,0]) with-replacement (<*0*>,dom A) by TREES_2:def 11
;
  then
A5: <*1*> in dom y by A4,A3,TREES_1:def 9;
  then dom (A '&' B) = dom y with-replacement (<*1*>,dom B) by TREES_2:def 11;
  then <*1*> in dom (A '&' B) by A5,TREES_1:def 9;
  hence thesis by A1,TARSKI:def 1,TREES_1:29;
end;

theorem Th44:
  'not' A <> (#)B & 'not' A <> B '&' C
proof
  set e2 = elementary_tree 2;
  set e1 = elementary_tree 1;
  set E = e1 --> [1,0];
  set F = e1 --> [1,1];
  reconsider e = {} as Element of dom 'not' A by TREES_1:22;
A1: {} in dom (#)B & not ex u st u in dom B & e = <*0*>^u & ((#)B).e = B.u
  by TREES_1:22;
A2: <*0*> in e1 by TARSKI:def 2,TREES_1:51;
  then
A3: <*0*> in dom E by FUNCOP_1:13;
  then
A4: dom 'not' A = dom E with-replacement (<*0*>,dom A) by TREES_2:def 11;
A5: <*0*> in dom F by A2,FUNCOP_1:13;
  then dom (#)B = dom F with-replacement (<*0*>,dom B) by TREES_2:def 11;
  then
A6: ((#) B).e = F.e by A5,A1,TREES_2:def 11;
  e in e1 by TREES_1:22;
  then
A7: E.e = [1,0] & F.e = [1,1] by FUNCOP_1:7;
  ( not ex u st u in dom A & e = <*0*>^u & ('not' A).e = A.u)& [1,0] <> [
  1,1] by XTUPLE_0:1;
  hence 'not' A <> (#)B by A3,A4,A6,A7,TREES_2:def 11;
  set y = (e2-->[2,0]) with-replacement (<*0*>,B);
A8: <*1*> in e2 & not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:28,52;
A9: <*0*> in e2 & dom (e2 --> [2,0]) = e2 by FUNCOP_1:13,TREES_1:28;
  then dom y = dom(e2-->[2,0]) with-replacement (<*0*>,dom B) by TREES_2:def 11
;
  then
A10: <*1*> in dom y by A9,A8,TREES_1:def 9;
  then dom (B '&' C) = dom y with-replacement (<*1*>,dom C) by TREES_2:def 11;
  then
A11: <*1*> in dom (B '&' C) by A10,TREES_1:def 9;
A12: now
    assume <*1*> in dom E;
    then <*1*> = {} or <*1*> = <*0*> by TARSKI:def 2,TREES_1:51;
    hence contradiction by TREES_1:3;
  end;
  assume not thesis;
  then ex s st s in dom A & <*1*> = <*0*>^s by A3,A4,A11,A12,TREES_1:def 9;
  then <*0*> is_a_prefix_of <*1*> by TREES_1:1;
  hence contradiction by TREES_1:3;
end;

theorem Th45:
  (#)A <> B '&' C
proof
  set e2 = elementary_tree 2;
  set e1 = elementary_tree 1;
  set F = e1 --> [1,1];
  set y = (e2-->[2,0]) with-replacement (<*0*>,B);
A1: <*1*> in e2 & not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:28,52;
A2: <*0*> in e2 & dom (e2 --> [2,0]) = e2 by FUNCOP_1:13,TREES_1:28;
  then dom y = dom(e2-->[2,0]) with-replacement (<*0*>,dom B) by TREES_2:def 11
;
  then
A3: <*1*> in dom y by A2,A1,TREES_1:def 9;
  then dom (B '&' C) = dom y with-replacement (<*1*>,dom C) by TREES_2:def 11;
  then
A4: <*1*> in dom (B '&' C) by A3,TREES_1:def 9;
  assume
A5: not thesis;
A6: now
    assume <*1*> in dom F;
    then <*1*> = {} or <*1*> = <*0*> by TARSKI:def 2,TREES_1:51;
    hence contradiction by TREES_1:3;
  end;
  <*0*> in e1 by TARSKI:def 2,TREES_1:51;
  then
A7: <*0*> in dom F by FUNCOP_1:13;
  then dom (#)A = dom F with-replacement (<*0*>,dom A) by TREES_2:def 11;
  then ex s st s in dom A & <*1*> = <*0*>^s by A7,A4,A6,A5,TREES_1:def 9;
  then <*0*> is_a_prefix_of <*1*> by TREES_1:1;
  hence contradiction by TREES_1:3;
end;

Lm4: VERUM <> 'not' A & VERUM <> (#)A & VERUM <> A '&' B
proof
  set e2 = elementary_tree 2;
  set e1 = elementary_tree 1;
A1: dom VERUM = elementary_tree 0 by FUNCOP_1:13;
  set F = e1 --> [1,1];
  set E = e1 --> [1,0];
A2: <*0*> in e1 by TARSKI:def 2,TREES_1:51;
  then <*0*> in dom E by FUNCOP_1:13;
  then dom E = e1 & dom 'not' A = dom E with-replacement (<*0*>,dom A) by
FUNCOP_1:13,TREES_2:def 11;
  then <*0*> in dom ('not' A) by A2,TREES_1:def 9;
  hence VERUM <> 'not' A by A1,TARSKI:def 1,TREES_1:29;
  <*0*> in dom F by A2,FUNCOP_1:13;
  then dom F = e1 & dom (#)A = dom F with-replacement (<*0*>,dom A) by
FUNCOP_1:13,TREES_2:def 11;
  then <*0*> in dom ((#)A) by A2,TREES_1:def 9;
  hence VERUM <> (#)A by A1,TARSKI:def 1,TREES_1:29;
  set y = (e2-->[2,0]) with-replacement (<*0*>,A);
A3: <*1*> in e2 & not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:28,52;
A4: <*0*> in e2 & dom (e2 --> [2,0]) = e2 by FUNCOP_1:13,TREES_1:28;
  then dom y = dom( e2-->[2,0]) with-replacement (<*0*>,dom A) by
TREES_2:def 11;
  then
A5: <*1*> in dom y by A4,A3,TREES_1:def 9;
  then dom (A '&' B) = dom y with-replacement (<*1*>,dom B) by TREES_2:def 11;
  then
A6: <*1*> in dom (A '&' B) by A5,TREES_1:def 9;
  assume not thesis;
  hence contradiction by A1,A6,TARSKI:def 1,TREES_1:29;
end;

Lm5: [0,0] is MP-conective
proof
  0 in {0,1,2} by ENUMSET1:def 1;
  hence thesis by ZFMISC_1:87;
end;

Lm6: VERUM <> @p
proof
  assume
A1: not thesis;
  rng @p = {p} & rng VERUM = {[0,0]} by FUNCOP_1:8;
  then [0,0] in {p} by A1,TARSKI:def 1;
  hence contradiction by Lm5,Th26,XBOOLE_0:3;
end;

theorem
  VERUM <> @p & VERUM <> 'not' A & VERUM <> (#)A & VERUM <> A '&' B by Lm4,Lm6;

scheme
  MPFuncEx{ D() -> non empty set, d() -> Element of D(), F(Element of
  MP-variables) -> Element of D(), N,H(Element of D()) -> Element of D(), C((
  Element of D()),Element of D()) -> Element of D() }: ex f being Function of
MP-WFF, D() st f.VERUM = d() & (for p being MP-variable holds f.@p = F(p)) & (
  for A being Element of MP-WFF holds f.('not' A) = N(f.A)) & (for A being
  Element of MP-WFF holds f.((#)A) = H(f.A)) & for A,B being Element of MP-WFF
  holds f.(A '&' B) = C(f.A,f.B) proof
  defpred Pfn[(Function of MP-WFF, D()), Element of NAT] means for A st card
dom A <= $2 holds (A = VERUM implies $1.A = d()) & (for p st A = @p holds $1.A
  = F(p)) & (for B st A = 'not' B holds $1.A = N($1.B)) & (for B st A = (#)B
  holds $1.A = H($1.B)) & (for B,C st A = B '&' C holds $1.A = C($1.B,$1.C));
  defpred Pfgp[(Element of D()),(Function of MP-WFF,D()),Element of MP-WFF]
means ($3 = VERUM implies $1 = d()) & (for p st $3 = @p holds $1 = F(p)) & (for
A st $3 = 'not' A holds $1 = N($2.A)) & (for A st $3 = (#)A holds $1 = H($2.A))
  & (for A,B st $3 = A '&' B holds $1 = C($2.A,$2.B));
  defpred P[Element of NAT] means ex F be Function of MP-WFF,D() st Pfn[F,$1];
  defpred Qfn[set, set] means ex A being Element of MP-WFF st A = $1 & for g
  being Function of MP-WFF, D() st Pfn[g, card dom A] holds $2 = g.A;
A1: for k st P[k] holds P[k+1]
  proof
    let k;
    given F be Function of MP-WFF,D() such that
A2: Pfn[F,k];
    defpred Q[Element of MP-WFF,Element of D()] means (card dom $1 <> k+1
    implies $2 = F.$1) & (card dom $1 = k+1 implies Pfgp[$2, F, $1]);
A3: for x being Element of MP-WFF ex y being Element of D() st Q[x,y]
    proof
      let A be Element of MP-WFF;
      now
        per cases by Th42;
        case
          card dom A <> k+1;
          take y=F.A;
        end;
        case
A4:       card dom A = k+1 & A = VERUM;
          take y = d();
          thus Pfgp[y,F,A] by A4,Lm4,Lm6;
        end;
        case
          card dom A = k + 1 & ex p st A = @p;
          then consider p such that
A5:       A = @p;
          take y = F(p);
          thus Pfgp[y,F,A] by A5,Lm6,Th32,Th43;
        end;
        case
          card dom A = k + 1 & ex B st A = 'not' B;
          then consider B such that
A6:       A = 'not' B;
          take y = N(F.B);
          thus Pfgp[y,F,A] by A6,Lm4,Th33,Th43,Th44;
        end;
        case
          card dom A = k + 1 & ex B st A = (#)B;
          then consider B such that
A7:       A = (#)B;
          take y = H(F.B);
          thus Pfgp[y,F,A] by A7,Lm4,Th34,Th43,Th44,Th45;
        end;
        case
          card dom A = k + 1 & ex B,C st A = B '&' C;
          then consider B,C such that
A8:       A = B '&' C;
          take y = C(F.B,F.C);
          now
            let B1,C1;
            assume
A9:         A = B1 '&' C1;
            then B=B1 by A8,Th35;
            hence y=C(F.B1,F.C1) by A8,A9,Th35;
          end;
          hence Pfgp[y,F,A] by A8,Lm4,Th43,Th44,Th45;
        end;
      end;
      hence thesis;
    end;
    consider G being Function of MP-WFF, D() such that
A10: for p being Element of MP-WFF holds Q[p,G.p] from FUNCT_2:sch 3(
    A3);
    take H = G;
    thus Pfn[H, k+1]
    proof
      let A be Element of MP-WFF;
      set p = card dom A;
      assume
A11:  p <= k+1;
      thus A = VERUM implies H.A = d()
      proof
        per cases;
        suppose
          p <> k+1;
          then p <= k & H.A = F.A by A10,A11,NAT_1:8;
          hence thesis by A2;
        end;
        suppose
          p = k+1;
          hence thesis by A10;
        end;
      end;
      thus for p st A = @p holds H.A = F(p)
      proof
        let q such that
A12:    A = @q;
        per cases;
        suppose
          p <> k+1;
          then p <= k & H.A = F.A by A10,A11,NAT_1:8;
          hence thesis by A2,A12;
        end;
        suppose
          p = k+1;
          hence thesis by A10,A12;
        end;
      end;
      thus for B st A = 'not' B holds H.A = N(H.B)
      proof
        let B;
        assume
A13:    A = 'not' B;
        then card dom B <> k+1 by A11,Th38;
        then
A14:    H.B = F.B by A10;
        per cases;
        suppose
          p <> k+1;
          then p <= k & H.A = F.A by A10,A11,NAT_1:8;
          hence thesis by A2,A13,A14;
        end;
        suppose
          p = k+1;
          hence thesis by A10,A13,A14;
        end;
      end;
      thus for B st A = (#)B holds H.A = H(H.B)
      proof
        let B;
        assume
A15:    A = (#)B;
        then card dom B <> k+1 by A11,Th39;
        then
A16:    H.B = F.B by A10;
        per cases;
        suppose
          p <> k+1;
          then p <= k & H.A = F.A by A10,A11,NAT_1:8;
          hence thesis by A2,A15,A16;
        end;
        suppose
          p = k+1;
          hence thesis by A10,A15,A16;
        end;
      end;
      thus for B,C st A = B '&' C holds H.A = C(H.B,H.C)
      proof
        let B,C;
        assume
A17:    A = B '&' C;
        then (card dom B) <> k+1 by A11,Th40;
        then
A18:    H.B = F.B by A10;
        (card dom C) <> k+1 by A11,A17,Th40;
        then
A19:    H.C = F.C by A10;
        per cases;
        suppose
          p <> k+1;
          then p <= k & H.A = F.A by A10,A11,NAT_1:8;
          hence thesis by A2,A17,A18,A19;
        end;
        suppose
          p = k+1;
          hence thesis by A10,A17,A18,A19;
        end;
      end;
    end;
  end;
A20: P[0]
  proof
    set F = the Function of MP-WFF,D();
    take F;
    let A;
    assume card dom A <= 0;
    hence thesis by NAT_1:2;
  end;
A21: for n holds P[n] from NAT_1:sch 1(A20,A1);
A22: for x st x in MP-WFF ex y st Qfn[x, y]
  proof
    let x;
    assume x in MP-WFF;
    then reconsider x9 = x as Element of MP-WFF;
    consider F being Function of MP-WFF, D() such that
A23: Pfn[F, card dom x9] by A21;
    take F.x, x9;
    thus x = x9;
    let G be Function of MP-WFF, D();
    defpred Prop[Element of MP-WFF] means card dom $1 <= card dom x9 implies F
    .$1 = G.$1;
    assume
A24: Pfn[G, card dom x9];
A25: for p holds Prop[@p]
    proof
      let p;
      assume
A26:  card dom @p <= card dom x9;
      hence F.@p = F(p) by A23
        .= G.@p by A24,A26;
    end;
A27: for A,B be Element of MP-WFF st Prop[A] & Prop[B] holds Prop[A '&' B]
    proof
      let A,B;
      assume that
A28:  ( Prop[A])& Prop[B] and
A29:  card dom(A '&' B) <= card dom x9;
      card dom A < card dom(A '&' B) & card dom B < card dom(A '&' B) by Th40;
      hence F.(A '&' B) = C(G.A, G.B) by A23,A28,A29,XXREAL_0:2
        .= G.(A '&' B) by A24,A29;
    end;
A30: for A be Element of MP-WFF st Prop[A] holds Prop[(#) A]
    proof
      let A such that
A31:  Prop[A];
      assume
A32:  card dom (#)A <= card dom x9;
      card dom A < card dom (#)A by Th39;
      hence F.((#)A) = H(G.A) by A23,A31,A32,XXREAL_0:2
        .= G.((#)A) by A24,A32;
    end;
A33: for A be Element of MP-WFF st Prop[A] holds Prop['not' A]
    proof
      let A such that
A34:  Prop[A];
      assume
A35:  card dom 'not' A <= card dom x9;
      card dom A < card dom 'not' A by Th38;
      hence F.('not' A) = N(G.A) by A23,A34,A35,XXREAL_0:2
        .= G.('not' A) by A24,A35;
    end;
A36: Prop[VERUM]
    proof
      assume
A37:  card dom VERUM <= card dom x9;
      hence F.VERUM = d() by A23
        .= G.VERUM by A24,A37;
    end;
    for p be Element of MP-WFF holds Prop[p] from MPInd(A36,A25, A33,A30,
    A27);
    hence thesis;
  end;
  consider F being Function such that
A38: dom F = MP-WFF and
A39: for x st x in MP-WFF holds Qfn[x, F.x] from CLASSES1:sch 1(A22);
  rng F c= D()
  proof
    let y;
    assume y in rng F;
    then consider x being set such that
A40: x in MP-WFF & y = F.x by A38,FUNCT_1:def 3;
    consider p being Element of MP-WFF such that
    p = x and
A41: for g being Function of MP-WFF, D() st Pfn[g, card dom p] holds y
    = g.p by A39,A40;
    consider G being Function of MP-WFF, D() such that
A42: Pfn[G, card dom p] by A21;
    y = G.p by A41,A42;
    hence thesis;
  end;
  then reconsider F as Function of MP-WFF, D() by A38,FUNCT_2:def 1,RELSET_1:4
;
  consider A such that
A43: A = VERUM and
A44: for g being Function of MP-WFF,D() st Pfn[g,card dom A] holds F.
  VERUM = g.A by A39;
  take F;
  consider G being Function of MP-WFF,D() such that
A45: Pfn[G,card dom A] by A21;
  F.VERUM = G.VERUM by A43,A44,A45;
  hence F.VERUM = d() by A43,A45;
  thus for p being MP-variable holds F.@p = F(p)
  proof
    let p be MP-variable;
    consider A such that
A46: A = @p and
A47: for g being Function of MP-WFF,D() st Pfn[g,card dom A] holds F.@
    p = g.A by A39;
    consider G being Function of MP-WFF,D() such that
A48: Pfn[G,card dom A] by A21;
    F.@p = G.@p by A46,A47,A48;
    hence thesis by A46,A48;
  end;
  thus for A being Element of MP-WFF holds F.('not' A) = N(F.A)
  proof
    let A be Element of MP-WFF;
    consider A1 such that
A49: A1 = 'not' A and
A50: for g being Function of MP-WFF,D() st Pfn[g,card dom A1] holds F.
    'not' A = g.A1 by A39;
    consider G being Function of MP-WFF,D() such that
A51: Pfn[G,card dom A1] by A21;
A52: for k st k < card dom 'not' A holds Pfn[G,k]
    proof
      let k;
      assume
A53:  k < card dom 'not' A;
      let a be Element of MP-WFF;
      assume card dom a <= k;
      then card dom a <= card dom 'not' A by A53,XXREAL_0:2;
      hence thesis by A49,A51;
    end;
A54: ex B st B = A & for g be Function of MP-WFF,D() st Pfn[g,card dom B]
    holds F.A = g.B by A39;
    set k = card dom A;
    k < card dom 'not' A by Th38;
    then Pfn[G,k] by A52;
    then
A55: F.A = G.A by A54;
    F.'not' A = G.'not' A by A49,A50,A51;
    hence thesis by A49,A51,A55;
  end;
  thus for A being Element of MP-WFF holds F.((#)A) = H(F.A)
  proof
    let A be Element of MP-WFF;
    consider A1 such that
A56: A1 = (#)A and
A57: for g being Function of MP-WFF,D() st Pfn[g,card dom A1] holds F
    .( (#)A) = g.A1 by A39;
    consider G being Function of MP-WFF,D() such that
A58: Pfn[G,card dom A1] by A21;
A59: for k st k < card dom (#)A holds Pfn[G,k]
    proof
      let k;
      assume
A60:  k < card dom (#)A;
      let a be Element of MP-WFF;
      assume card dom a <= k;
      then card dom a <= card dom (#)A by A60,XXREAL_0:2;
      hence thesis by A56,A58;
    end;
A61: ex B st B = A & for g be Function of MP-WFF,D() st Pfn[g,card dom B]
    holds F.A = g.B by A39;
    set k = card dom A;
    k < card dom (#)A by Th39;
    then Pfn[G,k] by A59;
    then
A62: F.A = G.A by A61;
    F.((#)A) = G.((#)A) by A56,A57,A58;
    hence thesis by A56,A58,A62;
  end;
  thus for A,B being Element of MP-WFF holds F.(A '&' B) = C(F.A,F.B)
  proof
    let A,B be Element of MP-WFF;
    set k1 = card dom A;
    set k2 = card dom B;
    consider A1 such that
A63: A1 = A '&' B and
A64: for g being Function of MP-WFF,D() st Pfn[g,card dom A1] holds F
    .( A '&' B) = g.A1 by A39;
    consider G being Function of MP-WFF,D() such that
A65: Pfn[G,card dom A1] by A21;
A66: for k st k < card dom(A '&' B) holds Pfn[G,k]
    proof
      let k;
      assume
A67:  k < card dom(A '&' B);
      let a be Element of MP-WFF;
      assume card dom a <= k;
      then card dom a <= card dom(A '&' B) by A67,XXREAL_0:2;
      hence thesis by A63,A65;
    end;
A68: ex B1 st B1 = A & for g be Function of MP-WFF,D() st Pfn[g,card dom
    B1] holds F.A = g.B1 by A39;
    k1 < card dom(A '&' B) by Th40;
    then Pfn[G,k1] by A66;
    then
A69: F.A = G.A by A68;
A70: ex C st C = B & for g be Function of MP-WFF,D() st Pfn[g,card dom C]
    holds F.B = g.C by A39;
    k2 < card dom(A '&' B) by Th40;
    then Pfn[G,k2] by A66;
    then
A71: F.B = G.B by A70;
    F.(A '&' B) = G.(A '&' B) by A63,A64,A65;
    hence thesis by A63,A65,A69,A71;
  end;
end;