:: Introduction to Modal Propositional Logic
:: by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, 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,
ORDINAL1, NUMBERS, WELLORD2, XCMPLX_0, 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, NUMBERS;
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;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, NAT_1, ENUMSET1, TREES_1, TREES_2, FUNCOP_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, ORDINAL1;
schemes TREES_2, CLASSES1, NAT_1, FUNCT_2, XBOOLE_0;
begin
reserve x,y,x1,x2,z for set,
n,m,k for 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*>
by XBOOLE_1:2;
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;
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
.= (<*m*>^(s^a)).1 by FINSEQ_1:32
.= m by FINSEQ_1:41;
hence contradiction by A1;
end;
end;
::$CT
theorem Th2:
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;
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;
::$CT 4
theorem Th3:
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 Th5:
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 Th6:
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 Th7:
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,Th6,TREES_2:31;
end;
theorem Th8:
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;
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 be object;
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 n as Element of NAT by ORDINAL1:def 12;
x = v^<*n*> by A8;
then reconsider x9 = x as FinSequence of NAT;
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;
reconsider n as Element of NAT by ORDINAL1:def 12;
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:2;
end;
theorem Th9:
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;
now
let x be object;
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 n as Element of NAT by ORDINAL1:def 12;
x = v^<*n*> by A5;
then reconsider x9 = x as FinSequence of NAT;
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;
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;
reconsider n as Element of NAT by ORDINAL1:def 12;
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:2;
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 Th11:
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;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A4: t^<*nn*> = p^(t2^<*nn*>) 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[object,object] means
for n st $1 = t^<*n*> holds $2 = t2^<*n*>;
A5: for x being object st x in succ t ex y being object st P[x,y]
proof
let x be object;
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 being object st x in succ t holds P[x,f.x] from CLASSES1:
sch 1 (A5);
now
let x be object;
thus x in rng f implies x in succ t2
proof
assume x in rng f;
then consider y being object 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:2;
now
let x1,x2 be object;
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 Th12:
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 be object;
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:2;
hence thesis by CARD_2:42;
end;
theorem Th13:
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 being object 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 Th3,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 Th14:
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 being object 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 k <> 0 & ... & k <> 1 by A1,A5,A8,A9;
then 1 < k by NAT_1:25;
then 1+1 <= k by NAT_1:13;
then <*1*> in Z by A8,Th3,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,Th3,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 1 < m by A12,NAT_1:25;
then 1+1 <= m by NAT_1:13;
then <*1 *> in Z by A5,Th3,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 Th15:
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[object,object] means for s st $1 = s holds $2 = o^s;
A2: for x being object st x in Z|o ex y being object st P[x,y]
proof
let x be object;
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 being object 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 being object st x in Z|o for s st x = s holds f.x = o^s;
now
let x be object;
thus x in rng f implies x in A
proof
assume x in rng f;
then consider x1 being object 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:2;
now
let x1,x2 be object;
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 Th16:
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,Th15;
then reconsider A as finite set by CARD_1:38;
reconsider B = A \/ {Root Z} as finite set;
now
let x be object 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;
card B = card A + 1 by A1,Th15,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 Th17:
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,Th13;
then z in { <*0*> } by TARSKI:def 1;
then
A4: z = <*0*> by TARSKI:def 1;
then
A5: <*0*> in Z;
now
let x be object;
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:2;
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 Th18:
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,Th13;
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,Th17;
hence thesis by A7,TREES_2:31;
end;
theorem Th19:
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: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,Th2,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: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:3;
<*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 Th20:
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,Th19;
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 Th21:
MP-conectives misses MP-variables
proof
assume not thesis;
then consider x being object such that
A1: x in [:{0,1,2},NAT:] and
A2: x in [:{3},NAT:] by XBOOLE_0:3;
consider x1,x2 being object 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 -> Nat; :: redefines branchdeg (TREES_2, definition)
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[object] 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 being object 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 Th5;
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 be object;
assume x in rng T;
then consider z being object 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 Th5;
then reconsider Y as non empty set by A1,A8;
for x being object 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 be object;
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 be object;
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; :: redefines | (TREES_2, definition)
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 Th11,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];
x .v = [3,k] by A2,A5,TREES_2:def 10;
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 -> 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;
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 be object;
assume x in rng X;
then consider z being object 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 Th22:
((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 be object;
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:2;
succ v= succ v9 by A1,A3,A8,Lm1,Th8;
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 Th23:
((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 be object;
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:2;
succ v= succ v9 by A1,A3,A8,Lm1,Th8;
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 Th24:
(((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*>
by TREES_1:3;
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,Th8;
hence thesis by A5,A6,A14,Lm1,Th8;
end;
now
let x be object;
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:2;
<*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,Th9;
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 Th22;
func (#) A -> MP-wff equals
((elementary_tree 1)-->[1,1]) with-replacement (
<*0*>,A);
coherence by Th23;
let B;
func A '&' B -> MP-wff equals
((((elementary_tree 2)-->[2,0])
with-replacement (<*0*>,A))) with-replacement (<*1*>,B);
coherence by Th24;
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 Th25:
(elementary_tree 0) --> [3,n] is MP-wff
proof
3 in NAT & n in NAT by ORDINAL1:def 12;
then reconsider 3n = [3,n] as Element of [:NAT,NAT:] by ZFMISC_1:87;
set x = (elementary_tree 0) --> 3n;
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 Th26:
(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 being object 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,Th25;
end;
end;
theorem Th27:
@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 Th28:
'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,Th7;
end;
theorem Th29:
(#)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,Th7;
end;
theorem Th30:
(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,Th6;
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 Th2;
then
A31: <*0*>^s in dom (A '&' B) by A9,A10,A27,TREES_1:def 9;
not ex w st w in dom B & <*0*>^s = <*1*>^w & (A '&' B).(<*0*>^s) = B.w
by TREES_1:1,50;
then (A '&' B).(<*0*>^s) = y.(<*0*> ^s) by A9,A10,A31,TREES_2:def 11;
then
A32: A.s = (A1 '&' B).(<*0*>^s) by A1,A21,A29,FINSEQ_1:33;
not ex w st w in dom B1 & <*0*>^s = <*1*>^w & (A1 '&' B1).(<*0*>^s) = B1.w
by TREES_1:1,50;
then (A1 '&' B1).(<*0*>^s) = y1.(<* 0*>^s) by A1,A7,A11,A31,TREES_2:def 11;
hence thesis by A21,A32,A30,FINSEQ_1:33;
end;
hence thesis by A1,A5,A14,A23,A24,A15,Th6,TREES_2:31;
end;
definition
func VERUM -> MP-wff equals
(elementary_tree 0) --> [0,0];
coherence by Th26;
end;
theorem Th31:
card dom A = 1 implies A = VERUM or ex p st A = @p
proof
assume card dom A = 1;
then consider x being object 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 being object 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];
3 in NAT & n in NAT by ORDINAL1:def 12;
then reconsider p = [3,n] as MP-variable by ZFMISC_1:105;
for z being object 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 Th32:
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 Th12;
hence contradiction by A1;
end;
A3: b <= 2 by Def5;
now
b = 0 or ... or b = 2 by A3,NAT_1:60;
then per cases by A2;
case
A4: b = 1;
then card succ a = 1 by TREES_2:def 12;
then consider x being object 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,Th18;
end;
suppose
A.a = [1,1];
then Root A = [1,1];
hence A = 'not' B or A = (#) B by A5,Th18;
end;
end;
hence thesis;
end;
case
A6: b = 2;
then
A7: succ a = { <*0*>,<*1*> } by Th14;
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,Th20;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th33:
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,Th16;
end;
theorem Th34:
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,Th16;
end;
theorem Th35:
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 Th2;
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 <> {};
not ex w st w in dom B & o^s = <*1*>^w by TREES_1:1,50;
then
A9: 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,A9,TREES_1:def 9;
hence s in dom A by FINSEQ_1:33;
end;
end;
hence s in dom A;
end;
then
A10: 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
A11: 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,A11,TREES_1:def 9;
hence s in dom B by FINSEQ_1:33;
end;
end;
hence s in dom B;
end;
then
A12: 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 A10,Th16;
u <> Root (dom(A '&' B));
hence thesis by A12,Th16;
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[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
b = 0 or ... or b = 2 by A9,NAT_1:60;
then per cases;
suppose
b = 0;
then
A10: card dom A = 1 by Th12;
now
per cases by A10,Th31;
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 Th13;
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,Th18;
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,Th16,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,Th16,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 Th14;
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,Th16,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,Th16,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,Th20;
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 2(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 Th37:
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:25;
suppose
card dom A = 1;
hence thesis by Th31;
end;
suppose
card dom A > 1;
then card dom A >= 1+1 by NAT_1:13;
hence thesis by Th32;
end;
end;
hence thesis;
end;
theorem Th38:
@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 Th39:
'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 Th40:
(#)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,Th21,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()), 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[Nat] means ex F be Function of MP-WFF,D() st Pfn[F,$1];
defpred Qfn[object, object] 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 Th37;
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,Th27,Th38;
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,Th28,Th38,Th39;
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,Th29,Th38,Th39,Th40;
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,Th30;
hence y=C(F.B1,F.C1) by A8,A9,Th30;
end;
hence Pfgp[y,F,A] by A8,Lm4,Th38,Th39,Th40;
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,Th33;
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,Th34;
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,Th35;
then
A18: H.B = F.B by A10;
(card dom C) <> k+1 by A11,A17,Th35;
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 2(A20,A1);
A22: for x being object st x in MP-WFF ex y being object st Qfn[x, y]
proof
let x be object;
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 Th35;
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 Th34;
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 Th33;
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 being object st x in MP-WFF 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
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 Th33;
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 Th34;
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 Th35;
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 Th35;
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;