:: Defining by structural induction in the positive propositional language
:: by Andrzej Trybulec
::
:: Received April 23, 1999
:: Copyright (c) 1999-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, PBOOLE, FUNCT_1, CARD_3, RELAT_1, TARSKI, FINSEQ_1,
ORDINAL4, XBOOLE_0, SUBSET_1, HILBERT1, TREES_1, TREES_A, CARD_1,
ARYTM_3, TREES_2, TREES_4, TREES_3, TREES_9, FUNCT_6, QC_LANG1, XBOOLEAN,
ZF_LANG, GLIB_000, XXREAL_0, NAT_1, ORDINAL1, ZFMISC_1, PARTFUN1,
FUNCT_4, FUNCOP_1, HILBERT2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_3,
RELAT_1, FUNCT_1, PARTFUN1, XCMPLX_0, NAT_1, FINSEQ_1, FUNCOP_1, FUNCT_4,
FUNCT_6, PBOOLE, TREES_1, TREES_2, TREES_3, TREES_4, TREES_9, HILBERT1,
XXREAL_0;
constructors FUNCT_4, XREAL_0, NAT_1, CARD_3, TREES_4, HILBERT1, RELSET_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
XREAL_0, NAT_1, FINSEQ_1, TREES_2, TREES_3, HILBERT1, TREES_4;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, HILBERT1, PARTFUN1;
equalities HILBERT1, FUNCOP_1;
expansions TARSKI, FUNCT_1, HILBERT1;
theorems PBOOLE, ZFMISC_1, FUNCT_1, HILBERT1, ORDERS_1, SUBSET_1, TARSKI,
FUNCT_4, FUNCOP_1, WELLFND1, CARD_3, GRFUNC_1, NAT_1, FINSEQ_1, TREES_1,
TREES_4, TREES_2, TREES_9, FINSEQ_2, TREES_3, RELAT_1, ORDINAL1,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, CARD_1, PARTFUN1, EQREL_1;
schemes PBOOLE, NAT_1, FINSEQ_1;
begin :: Preliminaries
reserve X,x for set;
theorem Th1:
for Z being set, M being ManySortedSet of Z st for x being set st
x in Z holds M.x is ManySortedSet of x for f being Function st f = Union M
holds dom f = union Z
proof
let Z be set, M be ManySortedSet of Z such that
A1: for x being set st x in Z holds M.x is ManySortedSet of x;
let f be Function;
assume f = Union M;
then
A2: f = union rng M by CARD_3:def 4;
for x being object holds x in dom f iff ex Y being set st x in Y & Y in Z
proof
let x be object;
thus x in dom f implies ex Y being set st x in Y & Y in Z
proof
assume x in dom f;
then [x,f.x] in f by FUNCT_1:def 2;
then consider g being set such that
A3: [x,f.x] in g and
A4: g in rng M by A2,TARSKI:def 4;
consider a being object such that
A5: a in dom M and
A6: g = M.a by A4,FUNCT_1:def 3;
reconsider a as set by TARSKI:1;
A7: a in Z by A5,PARTFUN1:def 2;
then reconsider g as ManySortedSet of a by A1,A6;
take dom g;
thus x in dom g by A3,FUNCT_1:1;
thus thesis by A7,PARTFUN1:def 2;
end;
given Y being set such that
A8: x in Y and
A9: Y in Z;
reconsider g = M.Y as ManySortedSet of Y by A1,A9;
Y = dom g by PARTFUN1:def 2;
then
A10: [x,g.x] in g by A8,FUNCT_1:1;
Z = dom M by PARTFUN1:def 2;
then g in rng M by A9,FUNCT_1:def 3;
then [x,g.x] in f by A2,A10,TARSKI:def 4;
hence thesis by FUNCT_1:1;
end;
hence thesis by TARSKI:def 4;
end;
theorem Th2:
for x,y being set, f,g being FinSequence st <*x*>^f = <*y*>^g holds f = g
proof
let x,y be set, f,g be FinSequence;
assume
A1: <*x*>^f = <*y*>^g;
then x = (<*y*>^g).1 by FINSEQ_1:41
.= y by FINSEQ_1:41;
hence thesis by A1,FINSEQ_1:33;
end;
theorem Th3:
for x being object holds <*x*> is FinSequence of X implies x in X
proof let x be object;
A1: rng<*x*> = {x} by FINSEQ_1:38;
assume <*x*> is FinSequence of X;
then {x} c= X by A1,FINSEQ_1:def 4;
hence thesis by ZFMISC_1:31;
end;
theorem Th4:
for X for f being FinSequence of X st f <> {} ex g being
FinSequence of X, d being Element of X st f = g^<*d*>
proof
let X be set, f be FinSequence of X;
assume f <> {};
then consider q being FinSequence, x being object such that
A1: f = q^<*x*> by FINSEQ_1:46;
reconsider q as FinSequence of X by A1,FINSEQ_1:36;
take q;
<*x*> is FinSequence of X by A1,FINSEQ_1:36;
then reconsider x as Element of X by Th3;
take x;
thus thesis by A1;
end;
reserve k,m,n for Element of NAT,
p,q,r,s,r9,s9 for Element of HP-WFF,
T1,T2 for Tree;
theorem Th5:
<*x*> in tree(T1,T2) iff x=0 or x=1
proof
A1: len<*T1,T2*> = 2 & tree(T1,T2) = tree<*T1,T2*> by FINSEQ_1:44
,TREES_3:def 17;
thus <*x*> in tree(T1,T2) implies x=0 or x=1
proof
assume <*x*> in tree(T1,T2);
then consider n being Nat, q being FinSequence such that
A2: n < 2 and
q in <*T1,T2*>.(n+1) and
A3: <*x*> = <*n*>^q by A1,TREES_3:def 15;
x = <*x*>.1
.= n by A3,FINSEQ_1:41;
hence thesis by A2,NAT_1:23;
end;
assume
A4: x=0 or x=1;
then reconsider n = x as Element of NAT;
<*T1,T2*>.(n+1) = T1 or <*T1,T2*>.(n+1) = T2 by A4;
then
A5: {} in <*T1,T2*>.(n+1) by TREES_1:22;
<*n*> = <*n*>^{} by FINSEQ_1:34;
hence thesis by A1,A4,A5,TREES_3:def 15;
end;
scheme
InTreeInd{T() -> Tree, P[set] }: for f being Element of T() holds P[f]
provided
A1: P[<*>NAT] and
A2: for f being Element of T() st P[f] for n st f^<*n*> in T() holds P[f
^<*n*>]
proof
defpred Q[FinSequence] means $1 in T() implies P[$1];
A3: for p being FinSequence, x being object st Q[p] holds Q[p^<*x*>]
proof
let p be FinSequence, x be object such that
A4: Q[p];
assume
A5: p^<*x*> in T();
then reconsider h = p^<*x*> as FinSequence of NAT by TREES_1:19;
consider g being FinSequence of NAT, n such that
A6: h = g^<*n*> by Th4;
A7: g = p by A6,FINSEQ_2:17;
reconsider g as Element of T() by A5,A6,TREES_1:21;
P[g] by A4,A7;
hence thesis by A2,A5,A6;
end;
A8: Q[ {} ] by A1;
for p being FinSequence holds Q[p] from FINSEQ_1:sch 3(A8,A3);
hence thesis;
end;
reserve T1,T2 for DecoratedTree;
theorem Th6:
for x being set, T1, T2 holds (x-tree (T1,T2)).{} = x
proof
let x be set, T1, T2;
x-tree (T1,T2) = x-tree<*T1,T2*> by TREES_4:def 6;
hence thesis by TREES_4:def 4;
end;
theorem Th7:
x-tree(T1,T2).<*0*> = T1.{} & x-tree(T1,T2).<*1*> = T2.{}
proof
A1: len<*T1,T2*> = 2 by FINSEQ_1:44;
reconsider w = {} as Node of T1 by TREES_1:22;
A2: <*T1,T2*>.(0+1) = T1;
thus x-tree(T1,T2).<*0*> = (x-tree<*T1,T2*>).<*0*> by TREES_4:def 6
.= (x-tree<*T1,T2*>).(<*0*>^w) by FINSEQ_1:34
.= T1.{} by A1,A2,TREES_4:12;
reconsider w = {} as Node of T2 by TREES_1:22;
A3: <*T1,T2*>.(1+1) = T2;
thus x-tree(T1,T2).<*1*> = (x-tree<*T1,T2*>).<*1*> by TREES_4:def 6
.= (x-tree<*T1,T2*>).(<*1*>^w) by FINSEQ_1:34
.= T2.{} by A1,A3,TREES_4:12;
end;
theorem Th8:
x-tree(T1,T2)|<*0*> = T1 & x-tree(T1,T2)|<*1*> = T2
proof
A1: len<*T1,T2*> = 2 by FINSEQ_1:44;
thus x-tree(T1,T2)|<*0*> = (x-tree<*T1,T2*>)|<*0*> by TREES_4:def 6
.= <*T1,T2*>.(0+1) by A1,TREES_4:def 4
.= T1;
thus x-tree(T1,T2)|<*1*> = (x-tree<*T1,T2*>)|<*1*> by TREES_4:def 6
.= <*T1,T2*>.(1+1) by A1,TREES_4:def 4
.= T2;
end;
registration
let x;
let p be DTree-yielding non empty FinSequence;
cluster x-tree p -> non root;
coherence
proof
assume x-tree p is root;
then
A1: dom(x-tree p) = tree{} by TREES_3:52,TREES_9:def 1;
ex q being DTree-yielding FinSequence st p = q & dom(x-tree p) = tree
doms q by TREES_4:def 4;
then dom p <> {} & doms p = {} by A1,TREES_3:50;
hence contradiction by TREES_3:37;
end;
end;
registration
let x;
let T1 be DecoratedTree;
cluster x-tree T1 -> non root;
coherence
proof
x-tree T1 = x-tree <*T1*> by TREES_4:def 5;
hence thesis;
end;
let T2 be DecoratedTree;
cluster x-tree (T1,T2) -> non root;
coherence
proof
x-tree (T1,T2) = x-tree <*T1,T2*> by TREES_4:def 6;
hence thesis;
end;
end;
begin :: About the language
definition
let n;
func prop n -> Element of HP-WFF equals
<*3+n*>;
coherence by HILBERT1:def 4;
end;
definition
let D be set;
redefine attr D is with_VERUM means :: redefines with_VERUM (HILBERT1, definition)
VERUM in D;
compatibility;
redefine attr D is with_propositional_variables means :: redefines with_propositional_variables (HILBERT1, definition)
for n holds prop n in D;
compatibility
proof
thus D is with_propositional_variables implies for n holds prop n in D;
assume
A1: for n holds prop n in D;
let n;
prop n = <*3+n*>;
hence thesis by A1;
end;
end;
definition
let D be Subset of HP-WFF;
redefine attr D is with_implication means :: redefines with_implication (HILBERT1, definition)
for p, q st p in D & q in D holds p => q in D;
compatibility
proof
thus D is with_implication implies for p, q st p in D & q in D holds p =>
q in D;
assume
A1: for p, q st p in D & q in D holds p => q in D;
let p, q be FinSequence;
assume
A2: p in D & q in D;
then reconsider p9 = p, q9 = q as Element of HP-WFF;
p9 => q9 in D by A1,A2;
hence thesis;
end;
redefine attr D is with_conjunction means :: redefines with_conjunction (HILBERT1, definition)
for p, q st p in D & q in D holds p '&' q in D;
compatibility
proof
thus D is with_conjunction implies for p, q st p in D & q in D holds p '&'
q in D;
assume
A3: for p, q st p in D & q in D holds p '&' q in D;
let p, q be FinSequence;
assume
A4: p in D & q in D;
then reconsider p9 = p, q9 = q as Element of HP-WFF;
p9 '&' q9 in D by A3,A4;
hence thesis;
end;
end;
reserve t,t1 for FinSequence;
definition
let p;
attr p is conjunctive means
:Def6:
ex r,s st p = r '&' s;
attr p is conditional means
:Def7:
ex r,s st p = r => s;
attr p is simple means
:Def8:
ex n st p = prop n;
end;
scheme
HPInd { P[set] }: for r holds P[r]
provided
A1: P[VERUM] and
A2: for n holds P[prop n] and
A3: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
set X = { p where p is Element of HP-WFF: P[p]};
X c= HP-WFF
proof
let x be object;
assume x in X;
then ex p being Element of HP-WFF st x = p & P[p];
hence thesis;
end;
then reconsider X as Subset of HP-WFF;
let r;
A4: X is with_propositional_variables
proof
let n;
P[prop n] by A2;
hence thesis;
end;
A5: X is with_implication
proof
let p, q;
assume p in X;
then
A6: ex x being Element of HP-WFF st p = x & P[x];
assume q in X;
then ex x being Element of HP-WFF st q = x & P[x];
then P[p => q] by A3,A6;
hence thesis;
end;
A7: HP-WFF c= NAT* by HILBERT1:def 5;
A8: X c= NAT*
by A7;
A9: X is with_conjunction
proof
let p, q;
assume p in X;
then
A10: ex x being Element of HP-WFF st p = x & P[x];
assume q in X;
then ex x being Element of HP-WFF st q = x & P[x];
then P[p '&' q] by A3,A10;
hence thesis;
end;
VERUM in X by A1;
then X is with_VERUM;
then HP-WFF c= X by A8,A5,A9,A4,HILBERT1:def 6;
then r in X;
then ex p being Element of HP-WFF st r = p & P[p];
hence thesis;
end;
theorem Th9:
p is conjunctive or p is conditional or p is simple or p = VERUM
proof
defpred P[Element of HP-WFF] means $1 is conjunctive or $1 is conditional or
$1 is simple or $1 = VERUM;
A1: P[VERUM];
A2: for n holds P[prop n] by Def8;
A3: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s] by Def6,Def7;
for p holds P[p] from HPInd(A1,A2,A3);
hence thesis;
end;
theorem Th10:
len p >= 1
proof
per cases by Th9;
suppose
p is conjunctive;
then consider r,s such that
A1: p = r '&' s;
len p = len(<*2*>^(r^s)) by A1,FINSEQ_1:32
.= len<*2*> + len(r^s) by FINSEQ_1:22
.= 1 + len(r^s) by FINSEQ_1:39;
hence thesis by NAT_1:11;
end;
suppose
p is conditional;
then consider r,s such that
A2: p = r => s;
len p = len(<*1*>^(r^s)) by A2,FINSEQ_1:32
.= len<*1*> + len(r^s) by FINSEQ_1:22
.= 1 + len(r^s) by FINSEQ_1:39;
hence thesis by NAT_1:11;
end;
suppose
p is simple;
then ex n st p = prop n;
hence thesis by FINSEQ_1:39;
end;
suppose
p = VERUM;
hence thesis by FINSEQ_1:39;
end;
end;
theorem Th11:
p.1 = 1 implies p is conditional
proof
assume
A1: p.1 = 1;
per cases by Th9;
suppose
p is conjunctive;
then consider r,s such that
A2: p = r '&' s;
p = <*2*>^(r^s) by A2,FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
suppose
p is conditional;
hence thesis;
end;
suppose
p is simple;
then consider n such that
A3: p = prop n;
1+0 = 1+(2+n) by A1,A3;
hence thesis;
end;
suppose
p = VERUM;
hence thesis by A1;
end;
end;
theorem Th12:
p.1 = 2 implies p is conjunctive
proof
assume
A1: p.1 = 2;
per cases by Th9;
suppose
p is conjunctive;
hence thesis;
end;
suppose
p is conditional;
then consider r,s such that
A2: p = r => s;
p = <*1*>^(r^s) by A2,FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
suppose
p is simple;
then consider n such that
A3: p = prop n;
2+0 = 2+(1+n) by A1,A3;
hence thesis;
end;
suppose
p = VERUM;
hence thesis by A1;
end;
end;
theorem
p.1 = 3+n implies p is simple
proof
assume
A1: p.1 = 3+n;
per cases by Th9;
suppose
p is conjunctive;
then consider r,s such that
A2: p = r '&' s;
p = <*2*>^(r^s) by A2,FINSEQ_1:32;
then 2+0 = 2+(1+n) by A1,FINSEQ_1:41;
hence thesis;
end;
suppose
p is conditional;
then consider r,s such that
A3: p = r => s;
p = <*1*>^(r^s) by A3,FINSEQ_1:32;
then 1+0 = 1+(2+n) by A1,FINSEQ_1:41;
hence thesis;
end;
suppose
p is simple;
hence thesis;
end;
suppose
p = VERUM;
hence thesis by A1;
end;
end;
theorem
p.1 = 0 implies p = VERUM
proof
assume
A1: p.1 = 0;
per cases by Th9;
suppose
p is conjunctive;
then consider r,s such that
A2: p = r '&' s;
p = <*2*>^(r^s) by A2,FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
suppose
p is conditional;
then consider r,s such that
A3: p = r => s;
p = <*1*>^(r^s) by A3,FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
suppose
p is simple;
then ex n st p = prop n;
hence thesis by A1;
end;
suppose
p = VERUM;
hence thesis;
end;
end;
theorem Th15:
len p < len(p '&' q) & len q < len(p '&' q)
proof
len(p '&' q) = len(<*2*>^p) + len q by FINSEQ_1:22
.= len<*2*> + len p + len q by FINSEQ_1:22
.= 1 + len p + len q by FINSEQ_1:39
.= 1 + (len p + len q);
then
A1: len p + len q < len(p '&' q) by XREAL_1:29;
len p <= len p + len q & len q <= len p + len q by NAT_1:11;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th16:
len p < len(p => q) & len q < len(p => q)
proof
len(p => q) = len(<*1*>^p) + len q by FINSEQ_1:22
.= len<*1*> + len p + len q by FINSEQ_1:22
.= 1 + len p + len q by FINSEQ_1:39
.= 1 + (len p + len q);
then
A1: len p + len q < len(p => q) by XREAL_1:29;
len p <= len p + len q & len q <= len p + len q by NAT_1:11;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th17:
p = q^t implies p = q
proof
defpred P[Nat] means for p,q,t st len p = $1 & p = q^t holds p = q;
A1: for n be Nat st for k being Nat st k < n holds P[k] holds P[n]
proof
let n be Nat such that
A2: for k being Nat st k < n holds for p,q,t st len p = k & p = q^t
holds p = q;
let p,q,t such that
A3: len p = n and
A4: p = q^t;
len q >= 1 by Th10;
then
A5: p.1 = q.1 by A4,FINSEQ_1:64;
per cases by Th9;
suppose
p is conjunctive;
then consider r,s such that
A6: p = r '&' s;
q.1 = (<*2*>^(r^s)).1 by A5,A6,FINSEQ_1:32
.= 2 by FINSEQ_1:41;
then q is conjunctive by Th12;
then consider r9,s9 such that
A7: q = r9 '&' s9;
<*2*>^(r9^s9^t) = <*2*>^(r9^s9)^t by FINSEQ_1:32
.= <*2*>^r^s by A4,A6,A7,FINSEQ_1:32
.= <*2*>^(r^s) by FINSEQ_1:32;
then r9^s9^t = r^s by Th2;
then
A8: r9^(s9^t) = r^s by FINSEQ_1:32;
now
per cases;
suppose
A9: len r <= len r9;
n = len q + len t by A3,A4,FINSEQ_1:22;
then len q <= n by NAT_1:11;
then
A10: len r9 < n by A7,Th15,XXREAL_0:2;
ex t1 st r^t1 = r9 by A8,A9,FINSEQ_1:47;
then r = r9 by A2,A10;
then
A11: s9^t = s by A8,FINSEQ_1:33;
len s < n by A3,A6,Th15;
then s9 = s by A2,A11;
then t = {} by A11,FINSEQ_1:87;
hence thesis by A4,FINSEQ_1:34;
end;
suppose
len r >= len r9;
then
A12: ex t1 st r9^t1 = r by A8,FINSEQ_1:47;
len r < n by A3,A6,Th15;
then r = r9 by A2,A12;
then
A13: s9^t = s by A8,FINSEQ_1:33;
len s < n by A3,A6,Th15;
then s9 = s by A2,A13;
then t = {} by A13,FINSEQ_1:87;
hence thesis by A4,FINSEQ_1:34;
end;
end;
hence thesis;
end;
suppose
p is conditional;
then consider r,s such that
A14: p = r => s;
q.1 = (<*1*>^(r^s)).1 by A5,A14,FINSEQ_1:32
.= 1 by FINSEQ_1:41;
then q is conditional by Th11;
then consider r9,s9 such that
A15: q = r9 => s9;
<*1*>^(r9^s9^t) = <*1*>^(r9^s9)^t by FINSEQ_1:32
.= <*1*>^r^s by A4,A14,A15,FINSEQ_1:32
.= <*1*>^(r^s) by FINSEQ_1:32;
then r9^s9^t = r^s by Th2;
then
A16: r9^(s9^t) = r^s by FINSEQ_1:32;
now
per cases;
suppose
A17: len r <= len r9;
n = len q + len t by A3,A4,FINSEQ_1:22;
then len q <= n by NAT_1:11;
then
A18: len r9 < n by A15,Th16,XXREAL_0:2;
ex t1 st r^t1 = r9 by A16,A17,FINSEQ_1:47;
then r = r9 by A2,A18;
then
A19: s9^t = s by A16,FINSEQ_1:33;
len s < n by A3,A14,Th16;
then s9 = s by A2,A19;
then t = {} by A19,FINSEQ_1:87;
hence thesis by A4,FINSEQ_1:34;
end;
suppose
len r >= len r9;
then
A20: ex t1 st r9^t1 = r by A16,FINSEQ_1:47;
len r < n by A3,A14,Th16;
then r = r9 by A2,A20;
then
A21: s9^t = s by A16,FINSEQ_1:33;
len s < n by A3,A14,Th16;
then s9 = s by A2,A21;
then t = {} by A21,FINSEQ_1:87;
hence thesis by A4,FINSEQ_1:34;
end;
end;
hence thesis;
end;
suppose
A22: p is simple;
A23: q <> {} by Th10,CARD_1:27;
ex n st p = prop n by A22;
hence thesis by A4,A23,FINSEQ_1:88;
end;
suppose
A24: p = VERUM;
q <> {} by Th10,CARD_1:27;
hence thesis by A4,A24,FINSEQ_1:88;
end;
end;
A25: for n being Nat holds P[n] from NAT_1:sch 4(A1);
len p = len p;
hence thesis by A25;
end;
theorem Th18:
p^q = r^s implies p = r & q = s
proof
assume
A1: p^q = r^s;
per cases;
suppose
len p <= len r;
then ex t st p^t = r by A1,FINSEQ_1:47;
hence p = r by Th17;
hence thesis by A1,FINSEQ_1:33;
end;
suppose
len p >= len r;
then ex t st r^t = p by A1,FINSEQ_1:47;
hence p = r by Th17;
hence thesis by A1,FINSEQ_1:33;
end;
end;
theorem Th19:
p '&' q = r '&' s implies p = r & s = q
proof
assume p '&' q = r '&' s;
then <*2*>^(p^q) = r '&' s by FINSEQ_1:32
.= <*2*>^(r^s) by FINSEQ_1:32;
then p^q = r^s by Th2;
hence thesis by Th18;
end;
theorem Th20:
p => q = r => s implies p = r & s = q
proof
assume p => q = r => s;
then <*1*>^(p^q) = r => s by FINSEQ_1:32
.= <*1*>^(r^s) by FINSEQ_1:32;
then p^q = r^s by Th2;
hence thesis by Th18;
end;
theorem Th21:
prop n = prop m implies n = m
proof
assume prop n = prop m;
then 3+n = 3+m by FINSEQ_1:76;
hence thesis;
end;
theorem Th22:
p '&' q <> r => s
proof
p '&' q = <*2*>^(p^q) by FINSEQ_1:32;
then r => s = <*1*>^(r^s) & (p '&' q).1 = 2 by FINSEQ_1:32,41;
hence thesis by FINSEQ_1:41;
end;
theorem Th23:
p '&' q <> VERUM
proof
p '&' q = <*2*>^(p^q) by FINSEQ_1:32;
then (p '&' q).1 = 2 by FINSEQ_1:41;
hence thesis;
end;
theorem Th24:
p '&' q <> prop n
proof
A1: now
assume 2 = 2+1+n;
then 2+0 = 2+(1+n);
hence contradiction;
end;
p '&' q = <*2*>^(p^q) by FINSEQ_1:32;
then (p '&' q).1 = 2 by FINSEQ_1:41;
hence thesis by A1;
end;
theorem Th25:
p => q <> VERUM
proof
p => q = <*1*>^(p^q) by FINSEQ_1:32;
then (p => q).1 = 1 by FINSEQ_1:41;
hence thesis;
end;
theorem Th26:
p => q <> prop n
proof
A1: now
assume 1 = 1+2+n;
then 1+0 = 1+(2+n);
hence contradiction;
end;
p => q = <*1*>^(p^q) by FINSEQ_1:32;
then (p => q).1 = 1 by FINSEQ_1:41;
hence thesis by A1;
end;
theorem Th27:
p '&' q <> p & p '&' q <> q
proof
len p < len(p '&' q) by Th15;
hence thesis by Th15;
end;
theorem Th28:
p => q <> p & p => q <> q
proof
len p < len(p => q) by Th16;
hence thesis by Th16;
end;
theorem Th29:
VERUM <> prop n
proof
assume
A1: not thesis;
VERUM.1 = 0;
hence contradiction by A1,FINSEQ_1:40;
end;
begin :: Defining by structural induction
scheme
HPMSSExL{V()->set,P(Element of NAT)->set, C,I[Element of HP-WFF,Element of
HP-WFF,set,set,set]}: ex M being ManySortedSet of HP-WFF st M.VERUM = V() & (
for n holds M.prop n = P(n)) & for p,q holds C[p,q,M.p,M.q,M.(p '&' q)] & I[p,q
,M.p,M.q,M.(p => q)]
provided
A1: for p,q for a,b being set ex c being set st C[p,q,a,b,c] and
A2: for p,q for a,b being set ex d being set st I[p,q,a,b,d] and
A3: for p,q for a,b,c,d being set st C[p,q,a,b,c] & C[p,q,a,b,d] holds c
= d and
A4: for p,q for a,b,c,d being set st I[p,q,a,b,c] & I[p,q,a,b,d] holds c = d
proof
defpred P[object,object] means
($1 = VERUM implies $2 = V()) & for n st $1 = prop
n holds $2 = P(n);
set Pn = the set of all prop n;
set X = { Y where Y is Subset of HP-WFF: VERUM in Y & (for n holds prop n in
Y) & (for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y) & ex M
being ManySortedSet of Y st M.VERUM = V() & (for n holds M.prop n = P(n)) & (
for p,q st p '&' q in Y for a,b,c being set st a = M.p & b = M.q & c = M.(p '&'
q) holds C[p,q,a,b,c] ) & for p,q st p => q in Y for a,b,c being set st a = M.p
& b = M.q & c = M.(p => q) holds I[p,q,a,b,c] };
A5: Pn c= HP-WFF
proof
let x be object;
assume x in Pn;
then ex n st x = prop n;
hence thesis;
end;
{VERUM} c= HP-WFF by ZFMISC_1:31;
then reconsider Y0 = Pn \/ {VERUM} as Subset of HP-WFF by A5,XBOOLE_1:8;
A6: for x being object st x in Y0 ex y being object st P[x,y]
proof
let x be object;
assume
A7: x in Y0;
per cases by A7,XBOOLE_0:def 3;
suppose
x in Pn;
then consider n such that
A8: x = prop n;
take P(n);
thus x = VERUM implies P(n) = V() by A8,Th29;
let k;
assume x = prop k;
hence thesis by A8,Th21;
end;
suppose
A9: x in { VERUM };
take V();
x = VERUM by A9,TARSKI:def 1;
hence thesis by Th29;
end;
end;
consider M0 being ManySortedSet of Y0 such that
A10: for x being object st x in Y0 holds P[x,M0.x] from PBOOLE:sch 3(A6);
A11: for p,q holds not p '&' q in Y0 & not p => q in Y0
proof
let p,q;
assume
A12: not thesis;
per cases by A12,XBOOLE_0:def 3;
suppose
p '&' q in {VERUM} or p => q in {VERUM};
then p '&' q = VERUM or p => q = VERUM by TARSKI:def 1;
hence contradiction by Th23,Th25;
end;
suppose
p '&' q in Pn;
then ex n st p '&' q = prop n;
hence contradiction by Th24;
end;
suppose
p => q in Pn;
then ex n st p => q = prop n;
hence contradiction by Th26;
end;
end;
then
A13: ( for p,q st p '&' q in Y0 or p => q in Y0 holds p in Y0 & q in Y0)&
for p,q st p '&' q in Y0 for x,y,z being set st x = M0.p & y = M0.q & z = M0.(p
'&' q) holds C[p,q,x,y,z];
A14: for n holds prop n in Y0
proof
let k;
prop k in Pn;
hence thesis by XBOOLE_0:def 3;
end;
A15: for n holds M0.prop n = P(n)
proof
let n;
prop n in Y0 by A14;
hence thesis by A10;
end;
VERUM in {VERUM} by TARSKI:def 1;
then
A16: VERUM in Y0 by XBOOLE_0:def 3;
A17: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds union Z in X
proof
defpred P[object,object] means
ex D1 being set, M being ManySortedSet of D1 st D1=$1 & M = $2 & M.
VERUM = V() & (for n holds M.prop n = P(n)) & (for p,q st p '&' q in D1 for x,y
,z being set st x = M.p & y = M.q & z = M.(p '&' q) holds C[p,q,x,y,z]) & for p
,q st p => q in D1 for x,y,z being set st x = M.p & y = M.q & z = M.(p => q)
holds I[p,q,x,y,z];
let Z be set such that
A18: Z <> {} and
A19: Z c= X and
A20: Z is c=-linear;
A21: X c= bool HP-WFF
proof
let x be object;
assume x in X;
then ex Y being Subset of HP-WFF st x = Y & VERUM in Y & (for n holds
prop n in Y) & (for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y) &
ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M.prop n = P(n))
& (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y = M.q & z = M.(p
'&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z being set st x =
M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z];
hence thesis;
end;
then reconsider uZ = union Z as Subset of HP-WFF by A19,EQREL_1:61;
consider Z0 being object such that
A22: Z0 in Z by A18,XBOOLE_0:def 1;
reconsider Z0 as set by TARSKI:1;
A23: for x being object st x in Z ex y being object st P[x,y]
proof
let x be object;
assume x in Z;
then x in X by A19;
then consider Y being Subset of HP-WFF such that
A24: Y = x and
VERUM in Y and
for n holds prop n in Y and
for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y and
A25: ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M
.prop n = P(n)) & (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y =
M.q & z = M.(p '&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z
being set st x = M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z];
consider M being ManySortedSet of Y such that
A26: ( M.VERUM = V() & for n holds M.prop n = P(n) )&( ( for p,q st
p '&' q in Y for x,y,z being set st x = M.p & y = M.q & z = M.(p '&' q) holds C
[p,q,x,y,z])& for p,q st p => q in Y for x,y,z being set st x = M.p & y = M.q &
z = M.(p => q ) holds I[p,q,x,y,z] ) by A25;
take M;
thus thesis by A24,A26;
end;
consider MM being ManySortedSet of Z such that
A27: for x being object st x in Z holds P[x,MM.x] from PBOOLE:sch 3(A23);
rng MM is functional
proof
let y be object;
assume y in rng MM;
then consider x being object such that
A28: x in dom MM and
A29: y = MM.x by FUNCT_1:def 3;
x in Z by A28,PARTFUN1:def 2;
then P[x,y] by A27,A29;
hence thesis;
end;
then reconsider rr = rng MM as functional set;
A30: for f, g being Function st f in rr & g in rr & dom f c= dom g holds f
tolerates g
proof
let f, g be Function;
assume f in rr;
then consider x1 being object such that
A31: x1 in dom MM and
A32: f = MM.x1 by FUNCT_1:def 3;
reconsider x1 as set by TARSKI:1;
A33: x1 in Z by A31,PARTFUN1:def 2;
then P[x1,MM.x1] by A27;
then
A34: ex M being ManySortedSet of x1
st M = f & M.VERUM = V() & (for n
holds M.prop n = P(n)) & (for p,q st p '&' q in x1 for x,y,z being set st x = M
.p & y = M.q & z = M.(p '&' q) holds C[p,q,x,y,z]) & for p,q st p => q in x1
for x,y,z being set st x = M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z]
by A32;
then
A35: x1 = dom f by PARTFUN1:def 2;
assume g in rr;
then consider x2 being object such that
A36: x2 in dom MM and
A37: g = MM.x2 by FUNCT_1:def 3;
reconsider x2 as set by TARSKI:1;
defpred P[Element of HP-WFF] means $1 in x1 implies f.$1 = g.$1;
assume
A38: dom f c= dom g;
x2 in Z by A36,PARTFUN1:def 2;
then P[x2,MM.x2] by A27;
then
A39: ex M being ManySortedSet of x2 st M = g & M.VERUM = V() & (for n
holds M.prop n = P(n)) & (for p,q st p '&' q in x2 for x,y,z being set st x = M
.p & y = M.q & z = M.(p '&' q) holds C[p,q,x,y,z]) & for p,q st p => q in x2
for x,y,z being set st x = M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z]
by A37;
A40: for n holds P[prop n]
proof
let n such that
prop n in x1;
thus f.prop n = P(n) by A34
.= g.prop n by A39;
end;
A41: x1 in X by A19,A33;
A42: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
A43: (ex Y being Subset of HP-WFF st Y = x1 & VERUM in Y &( for n
holds prop n in Y) &( for p,q st p '&' q in Y or p => q in Y holds p in Y & q
in Y)& ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M. prop n
= P(n)) & (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y = M.q & z
= M.(p '&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z being set
st x = M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z])& x1 c= x2 by A39,A38
,A35,A41,PARTFUN1:def 2;
let r,s such that
A44: ( r in x1 implies f.r = g.r)&( s in x1 implies f.s = g.s);
thus r '&' s in x1 implies f.(r '&' s) = g.(r '&' s)
proof
assume r '&' s in x1;
then ( C[r,s,g.r,g.s,f.(r '&' s)])& C[r,s,g.r,g.s,g.(r '&' s)] by A34
,A39,A44,A43;
hence thesis by A3;
end;
thus r => s in x1 implies f.(r => s) = g.(r => s)
proof
assume r => s in x1;
then ( I[r,s,g.r,g.s,f.(r => s)])& I[r,s,g.r,g.s,g.(r => s)] by A34
,A39,A44,A43;
hence thesis by A4;
end;
end;
let x be object;
assume x in dom f /\ dom g;
then
A45: x in x1 by A38,A35,XBOOLE_1:28;
A46: P[VERUM] by A34,A39;
for p holds P[p] from HPInd(A46,A40,A42);
hence thesis by A21,A45,A41;
end;
for f, g being Function st f in rr & g in rr holds f tolerates g
proof
let f, g be Function;
assume
A47: f in rr;
then consider x1 being object such that
A48: x1 in dom MM and
A49: f = MM.x1 by FUNCT_1:def 3;
reconsider x1 as set by TARSKI:1;
A50: x1 in Z by A48,PARTFUN1:def 2;
then P[x1,MM.x1] by A27;
then ex M being ManySortedSet of x1 st M = f & M.VERUM = V() & (for n
holds M.prop n = P(n)) & (for p,q st p '&' q in x1 for x,y,z being set st x = M
.p & y = M.q & z = M.(p '&' q) holds C[p,q,x,y,z]) & for p,q st p => q in x1
for x,y,z being set st x = M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z]
by A49;
then
A51: x1 = dom f by PARTFUN1:def 2;
assume
A52: g in rr;
then consider x2 being object such that
A53: x2 in dom MM and
A54: g = MM.x2 by FUNCT_1:def 3;
reconsider x2 as set by TARSKI:1;
A55: x2 in Z by A53,PARTFUN1:def 2;
then x1,x2 are_c=-comparable by A20,A50,ORDINAL1:def 8;
then
A56: x1 c= x2 or x2 c= x1 by XBOOLE_0:def 9;
P[x2,MM.x2] by A27,A55;
then ex M being ManySortedSet of x2 st M = g & M.VERUM = V() & (for n
holds M.prop n = P(n)) & (for p,q st p '&' q in x2 for x,y,z being set st x = M
.p & y = M.q & z = M.(p '&' q) holds C[p,q,x,y,z]) & for p,q st p => q in x2
for x,y,z being set st x = M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z]
by A54;
then x2 = dom g by PARTFUN1:def 2;
hence thesis by A30,A47,A52,A51,A56;
end;
then union rr is Function by WELLFND1:1;
then reconsider M = Union MM as Function by CARD_3:def 4;
for x being set st x in Z holds MM.x is ManySortedSet of x
proof
let x be set;
assume x in Z;
then P[x,MM.x] by A27;
hence thesis;
end;
then dom M = uZ by Th1;
then reconsider M as ManySortedSet of uZ by PARTFUN1:def 2,RELAT_1:def 18;
A57: M = union rr by CARD_3:def 4;
A58: for p,q st p '&' q in uZ for x,y,z being set st x = M.p & y = M.q &
z = M.(p '&' q) holds C[p,q,x,y,z]
proof
let p,q;
assume p '&' q in uZ;
then consider Z1 being set such that
A59: p '&' q in Z1 and
A60: Z1 in Z by TARSKI:def 4;
Z1 in dom MM by A60,PARTFUN1:def 2;
then MM.Z1 in rr by FUNCT_1:def 3;
then
A61: MM.Z1 c= M by A57,ZFMISC_1:74;
let x,y,z be set;
assume that
A62: x = M.p and
A63: y = M.q and
A64: z = M.(p '&' q);
P[Z1,MM.Z1] by A27,A60;
then consider MZ1 being ManySortedSet of Z1 such that
A65: MZ1 = MM.Z1 and
MZ1.VERUM = V() and
for n holds MZ1.prop n = P(n) and
A66: for p,q st p '&' q in Z1 for x,y,z being set st x = MZ1.p & y
= MZ1.q & z = MZ1.(p '&' q) holds C[p,q,x,y,z] and
for p,q st p => q in Z1 for x,y,z being set st x = MZ1.p & y = MZ1.q
& z = MZ1.(p => q) holds I[p,q,x,y,z];
p '&' q in dom MZ1 by A59,PARTFUN1:def 2;
then
A67: z = MZ1.(p '&' q) by A65,A61,A64,GRFUNC_1:2;
Z1 in X by A19,A60;
then
A68: ex Y being Subset of HP-WFF st Z1 = Y & VERUM in Y & (for n holds
prop n in Y) & (for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y) &
ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M.prop n = P(n))
& (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y = M.q & z = M.(p
'&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z being set st x =
M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z];
then q in Z1 by A59;
then q in dom MZ1 by PARTFUN1:def 2;
then
A69: y = MZ1.q by A65,A61,A63,GRFUNC_1:2;
p in Z1 by A59,A68;
then p in dom MZ1 by PARTFUN1:def 2;
then x = MZ1.p by A65,A61,A62,GRFUNC_1:2;
hence thesis by A59,A66,A69,A67;
end;
Z0 in dom MM by A22,PARTFUN1:def 2;
then MM.Z0 in rr by FUNCT_1:def 3;
then
A70: MM.Z0 c= M by A57,ZFMISC_1:74;
P[Z0,MM.Z0] by A27,A22;
then consider MZ0 being ManySortedSet of Z0 such that
A71: MZ0 = MM.Z0 and
A72: MZ0.VERUM = V() and
A73: for n holds MZ0.prop n = P(n) and
for p,q st p '&' q in Z0 for x,y,z being set st x = MZ0.p & y = MZ0.q
& z = MZ0.(p '&' q) holds C[p,q,x,y,z] and
for p,q st p => q in Z0 for x,y,z being set st x = MZ0.p & y = MZ0 .q
& z = MZ0.(p => q) holds I[p,q,x,y,z];
A74: Y0 c= Z0
proof
let x be object;
Z0 in X by A19,A22;
then
A75: ex Y being Subset of HP-WFF st Y = Z0 & VERUM in Y &( for n holds
prop n in Y)&( for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y)&
ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M. prop n = P(n))
& (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y = M.q & z = M.(p
'&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z being set st x =
M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z];
assume
A76: x in Y0;
per cases by A76,XBOOLE_0:def 3;
suppose
x in {VERUM};
hence thesis by A75,TARSKI:def 1;
end;
suppose
x in Pn;
then ex n st x = prop n;
hence thesis by A75;
end;
end;
then
A77: Y0 c= dom MZ0 by PARTFUN1:def 2;
A78: for n holds M.prop n = P(n)
proof
let n;
prop n in Y0 by A14;
hence M.prop n = MZ0.prop n by A70,A71,A77,GRFUNC_1:2
.= P(n) by A73;
end;
A79: for p,q st p => q in uZ for x,y,z being set st x = M.p & y = M.q & z
= M.(p => q) holds I[p,q,x,y,z]
proof
let p,q;
assume p => q in uZ;
then consider Z1 being set such that
A80: p => q in Z1 and
A81: Z1 in Z by TARSKI:def 4;
Z1 in dom MM by A81,PARTFUN1:def 2;
then MM.Z1 in rr by FUNCT_1:def 3;
then
A82: MM.Z1 c= M by A57,ZFMISC_1:74;
let x,y,z be set;
assume that
A83: x = M.p and
A84: y = M.q and
A85: z = M.(p => q);
P[Z1,MM.Z1] by A27,A81;
then consider MZ1 being ManySortedSet of Z1 such that
A86: MZ1 = MM.Z1 and
MZ1.VERUM = V() and
for n holds MZ1.prop n = P(n) and
for p,q st p '&' q in Z1 for x,y,z being set st x = MZ1.p & y = MZ1.
q & z = MZ1.(p '&' q) holds C[p,q,x,y,z] and
A87: for p,q st p => q in Z1 for x,y,z being set st x = MZ1.p & y =
MZ1.q & z = MZ1.(p => q) holds I[p,q,x,y,z];
p => q in dom MZ1 by A80,PARTFUN1:def 2;
then
A88: z = MZ1.(p => q) by A86,A82,A85,GRFUNC_1:2;
Z1 in X by A19,A81;
then
A89: ex Y being Subset of HP-WFF st Z1 = Y & VERUM in Y & (for n holds
prop n in Y) & (for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y) &
ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M.prop n = P(n))
& (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y = M.q & z = M.(p
'&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z being set st x =
M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z];
then q in Z1 by A80;
then q in dom MZ1 by PARTFUN1:def 2;
then
A90: y = MZ1.q by A86,A82,A84,GRFUNC_1:2;
p in Z1 by A80,A89;
then p in dom MZ1 by PARTFUN1:def 2;
then x = MZ1.p by A86,A82,A83,GRFUNC_1:2;
hence thesis by A80,A87,A90,A88;
end;
A91: for p,q st p '&' q in uZ or p => q in uZ holds p in uZ & q in uZ
proof
let p,q;
assume
A92: p '&' q in uZ or p => q in uZ;
per cases by A92;
suppose
p '&' q in uZ;
then consider Z0 being set such that
A93: p '&' q in Z0 and
A94: Z0 in Z by TARSKI:def 4;
Z0 in X by A19,A94;
then
ex Y being Subset of HP-WFF st Z0 = Y & VERUM in Y & (for n holds
prop n in Y) & (for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y) &
ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M.prop n = P(n))
& (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y = M.q & z = M.(p
'&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z being set st x =
M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z];
then p in Z0 & q in Z0 by A93;
hence thesis by A94,TARSKI:def 4;
end;
suppose
p => q in uZ;
then consider Z0 being set such that
A95: p => q in Z0 and
A96: Z0 in Z by TARSKI:def 4;
Z0 in X by A19,A96;
then
ex Y being Subset of HP-WFF st Z0 = Y & VERUM in Y & (for n holds
prop n in Y) & (for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y) &
ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M.prop n = P(n))
& (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y = M.q & z = M.(p
'&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z being set st x =
M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z];
then p in Z0 & q in Z0 by A95;
hence thesis by A96,TARSKI:def 4;
end;
end;
Z0 c= uZ by A22,ZFMISC_1:74;
then
A97: Y0 c= uZ by A74;
A98: for n holds prop n in uZ
by A14,A97;
M.VERUM = V() by A16,A70,A71,A72,A77,GRFUNC_1:2;
hence thesis by A16,A97,A98,A91,A78,A58,A79;
end;
A99: for p,q st p => q in Y0 for x,y,z being set st x = M0.p & y = M0.q & z
= M0.(p => q) holds I[p,q,x,y,z] by A11;
M0.VERUM = V() by A10,A16;
then Y0 in X by A16,A14,A15,A13,A99;
then consider H being set such that
A100: H in X and
A101: for Z being set st Z in X & Z <> H holds not H c= Z by A17,ORDERS_1:67;
consider Y being Subset of HP-WFF such that
A102: Y = H and
A103: VERUM in Y and
A104: for n holds prop n in Y and
A105: for p,q st p '&' q in Y or p => q in Y holds p in Y & q in Y and
A106: ex M being ManySortedSet of Y st M.VERUM = V() & (for n holds M.
prop n = P(n)) & (for p,q st p '&' q in Y for x,y,z being set st x = M.p & y =
M.q & z = M.(p '&' q) holds C[p,q,x,y,z]) & for p,q st p => q in Y for x,y,z
being set st x = M.p & y = M.q & z = M.(p => q) holds I[p,q,x,y,z] by A100;
consider M being ManySortedSet of Y such that
A107: M.VERUM = V() and
A108: for n holds M.prop n = P(n) and
A109: for p,q st p '&' q in Y for x,y,z being set st x = M.p & y = M.q &
z = M.(p '&' q) holds C[p,q,x,y,z] and
A110: for p,q st p => q in Y for x,y,z being set st x = M.p & y = M.q &
z = M.(p => q) holds I[p,q,x,y,z] by A106;
A111: Y = HP-WFF
proof
defpred P[Element of HP-WFF] means $1 in Y;
A112: for n holds P[prop n] by A104;
A113: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s such that
A114: r in Y & s in Y;
assume
A115: not thesis;
per cases by A115;
suppose
A116: not r '&' s in Y;
{r '&' s} c= HP-WFF by ZFMISC_1:31;
then reconsider Y9 = Y \/ {r '&' s} as Subset of HP-WFF by XBOOLE_1:8;
consider CMrMs being set such that
A117: C[r,s,M.r,M.s,CMrMs] by A1;
set N = M +* (r '&' s .--> CMrMs);
A118: dom(r '&' s .--> CMrMs) = {r '&' s};
dom M = Y by PARTFUN1:def 2;
then dom N = Y9 by A118,FUNCT_4:def 1;
then reconsider N as ManySortedSet of Y9 by PARTFUN1:def 2
,RELAT_1:def 18;
r '&' s in {r '&' s} by TARSKI:def 1;
then
A119: r '&' s in Y9 by XBOOLE_0:def 3;
A120: for p,q st p => q in Y9 for x,y,z being set st x = N.p & y = N.q
& z = N.(p => q) holds I[p,q,x,y,z]
proof
let p,q such that
A121: p => q in Y9;
p => q <> r '&' s by Th22;
then
A122: not p => q in {r '&' s} by TARSKI:def 1;
then
A123: p => q in Y by A121,XBOOLE_0:def 3;
then p in Y by A105;
then not p in {r '&' s} by A116,TARSKI:def 1;
then
A124: N.p = M.p by A118,FUNCT_4:11;
q in Y by A105,A123;
then not q in {r '&' s} by A116,TARSKI:def 1;
then
A125: N.q = M.q by A118,FUNCT_4:11;
A126: N.(p => q) = M.(p => q) by A118,A122,FUNCT_4:11;
let x,y,z be set;
assume x = N.p & y = N.q & z = N.(p => q);
hence thesis by A110,A123,A124,A125,A126;
end;
A127: for n holds N.prop n = P(n)
proof
let n;
prop n <> r '&' s by Th24;
then not prop n in {r '&' s} by TARSKI:def 1;
hence N.prop n = M.prop n by A118,FUNCT_4:11
.= P(n) by A108;
end;
A128: for p,q st p '&' q in Y9 for x,y,z being set st x = N.p & y = N.
q & z = N.(p '&' q) holds C[p,q,x,y,z]
proof
let p,q such that
A129: p '&' q in Y9;
let x,y,z be set such that
A130: x = N.p & y = N.q & z = N.(p '&' q);
per cases;
suppose
A131: p '&' q = r '&' s;
q <> p '&' q by Th27;
then not q in {r '&' s} by A131,TARSKI:def 1;
then
A132: N.q = M.q by A118,FUNCT_4:11;
p <> p '&' q by Th27;
then not p in {r '&' s} by A131,TARSKI:def 1;
then
A133: N.p = M.p by A118,FUNCT_4:11;
p '&' q in {r '&' s} by A131,TARSKI:def 1;
then
A134: N.(p '&' q) = (r '&' s .--> CMrMs).(p '&' q) by A118,FUNCT_4:13;
p = r & q = s by A131,Th19;
hence thesis by A117,A130,A133,A132,A134,FUNCOP_1:72;
end;
suppose
p '&' q <> r '&' s;
then
A135: not p '&' q in {r '&' s} by TARSKI:def 1;
then
A136: p '&' q in Y by A129,XBOOLE_0:def 3;
then p in Y by A105;
then not p in {r '&' s} by A116,TARSKI:def 1;
then
A137: N.p = M.p by A118,FUNCT_4:11;
q in Y by A105,A136;
then not q in {r '&' s} by A116,TARSKI:def 1;
then
A138: N.q = M.q by A118,FUNCT_4:11;
N.(p '&' q) = M.(p '&' q) by A118,A135,FUNCT_4:11;
hence thesis by A109,A130,A136,A137,A138;
end;
end;
A139: Y c= Y9 by XBOOLE_1:7;
then
A140: for n holds prop n in Y9 by A104;
A141: for p,q st p '&' q in Y9 or p => q in Y9 holds p in Y9 & q in Y9
proof
let p,q such that
A142: p '&' q in Y9 or p => q in Y9;
per cases by A142;
suppose
p '&' q = r '&' s;
then p = r & q = s by Th19;
hence thesis by A114,A139;
end;
suppose that
A143: p '&' q in Y9 and
A144: p '&' q <> r '&' s;
not p '&' q in {r '&' s} by A144,TARSKI:def 1;
then p '&' q in Y by A143,XBOOLE_0:def 3;
then p in Y & q in Y by A105;
hence thesis by A139;
end;
suppose
A145: p => q in Y9;
p => q <> r '&' s by Th22;
then not p => q in {r '&' s} by TARSKI:def 1;
then p => q in Y by A145,XBOOLE_0:def 3;
then p in Y & q in Y by A105;
hence thesis by A139;
end;
end;
VERUM <> r '&' s by Th23;
then not VERUM in {r '&' s} by TARSKI:def 1;
then N.VERUM = V() by A107,A118,FUNCT_4:11;
then Y9 in X by A103,A139,A140,A141,A127,A128,A120;
hence contradiction by A101,A102,A116,A119,XBOOLE_1:7;
end;
suppose
A146: not r => s in Y;
{r => s} c= HP-WFF by ZFMISC_1:31;
then reconsider Y9 = Y \/ {r => s} as Subset of HP-WFF by XBOOLE_1:8;
consider IMrMs being set such that
A147: I[r,s,M.r,M.s,IMrMs] by A2;
set N = M +* (r => s .--> IMrMs);
A148: dom(r => s .--> IMrMs) = {r => s};
dom M = Y by PARTFUN1:def 2;
then dom N = Y9 by A148,FUNCT_4:def 1;
then reconsider N as ManySortedSet of Y9 by PARTFUN1:def 2
,RELAT_1:def 18;
r => s in {r => s} by TARSKI:def 1;
then
A149: r => s in Y9 by XBOOLE_0:def 3;
A150: for p,q st p '&' q in Y9 for x,y,z being set st x = N.p & y = N.
q & z = N.(p '&' q) holds C[p,q,x,y,z]
proof
let p,q such that
A151: p '&' q in Y9;
p '&' q <> r => s by Th22;
then
A152: not p '&' q in {r => s} by TARSKI:def 1;
then
A153: p '&' q in Y by A151,XBOOLE_0:def 3;
then p in Y by A105;
then not p in {r => s} by A146,TARSKI:def 1;
then
A154: N.p = M.p by A148,FUNCT_4:11;
q in Y by A105,A153;
then not q in {r => s} by A146,TARSKI:def 1;
then
A155: N.q = M.q by A148,FUNCT_4:11;
A156: N.(p '&' q) = M.(p '&' q) by A148,A152,FUNCT_4:11;
let x,y,z be set;
assume x = N.p & y = N.q & z = N.(p '&' q);
hence thesis by A109,A153,A154,A155,A156;
end;
A157: for n holds N.prop n = P(n)
proof
let n;
prop n <> r => s by Th26;
then not prop n in {r => s} by TARSKI:def 1;
hence N.prop n = M.prop n by A148,FUNCT_4:11
.= P(n) by A108;
end;
A158: for p,q st p => q in Y9 for x,y,z being set st x = N.p & y = N.q
& z = N.(p => q) holds I[p,q,x,y,z]
proof
let p,q such that
A159: p => q in Y9;
let x,y,z be set such that
A160: x = N.p & y = N.q & z = N.(p => q);
per cases;
suppose
A161: p => q = r => s;
q <> p => q by Th28;
then not q in {r => s} by A161,TARSKI:def 1;
then
A162: N.q = M.q by A148,FUNCT_4:11;
p <> p => q by Th28;
then not p in {r => s} by A161,TARSKI:def 1;
then
A163: N.p = M.p by A148,FUNCT_4:11;
p => q in {r => s} by A161,TARSKI:def 1;
then
A164: N.(p => q) = (r => s .--> IMrMs).(p => q) by A148,FUNCT_4:13;
p = r & q = s by A161,Th20;
hence thesis by A147,A160,A163,A162,A164,FUNCOP_1:72;
end;
suppose
p => q <> r => s;
then
A165: not p => q in {r => s} by TARSKI:def 1;
then
A166: p => q in Y by A159,XBOOLE_0:def 3;
then p in Y by A105;
then not p in {r => s} by A146,TARSKI:def 1;
then
A167: N.p = M.p by A148,FUNCT_4:11;
q in Y by A105,A166;
then not q in {r => s} by A146,TARSKI:def 1;
then
A168: N.q = M.q by A148,FUNCT_4:11;
N.(p => q) = M.(p => q) by A148,A165,FUNCT_4:11;
hence thesis by A110,A160,A166,A167,A168;
end;
end;
A169: Y c= Y9 by XBOOLE_1:7;
then
A170: for n holds prop n in Y9 by A104;
A171: for p,q st p '&' q in Y9 or p => q in Y9 holds p in Y9 & q in Y9
proof
let p,q such that
A172: p '&' q in Y9 or p => q in Y9;
per cases by A172;
suppose
p => q = r => s;
then p = r & q = s by Th20;
hence thesis by A114,A169;
end;
suppose that
A173: p => q in Y9 and
A174: p => q <> r => s;
not p => q in {r => s} by A174,TARSKI:def 1;
then p => q in Y by A173,XBOOLE_0:def 3;
then p in Y & q in Y by A105;
hence thesis by A169;
end;
suppose
A175: p '&' q in Y9;
p '&' q <> r => s by Th22;
then not p '&' q in {r => s} by TARSKI:def 1;
then p '&' q in Y by A175,XBOOLE_0:def 3;
then p in Y & q in Y by A105;
hence thesis by A169;
end;
end;
VERUM <> r => s by Th25;
then not VERUM in {r => s} by TARSKI:def 1;
then N.VERUM = V() by A107,A148,FUNCT_4:11;
then Y9 in X by A103,A169,A170,A171,A157,A158,A150;
hence contradiction by A101,A102,A146,A149,XBOOLE_1:7;
end;
end;
A176: P[VERUM] by A103;
for s holds P[s] from HPInd(A176,A112,A113);
hence thesis by SUBSET_1:28;
end;
then reconsider M as ManySortedSet of HP-WFF;
take M;
thus thesis by A107,A108,A109,A110,A111;
end;
scheme
HPMSSLambda{V()->set,P(Element of NAT)->set,C,I(set,set)->set}: ex M being
ManySortedSet of HP-WFF st M.VERUM = V() & (for n holds M.prop n = P(n)) & for
p,q holds M.(p '&' q) = C(M.p,M.q) & M.(p => q) = I(M.p,M.q) proof
defpred I[Element of HP-WFF,Element of HP-WFF,set,set,set] means $5 = I($3,
$4);
defpred C[Element of HP-WFF,Element of HP-WFF,set,set,set] means $5 = C($3,
$4);
A1: for p,q for a,b being set ex d being set st I[p,q,a,b,d];
A2: for p,q for a,b,c,d being set st C[p,q,a,b,c] & C[p,q,a,b,d] holds c = d;
A3: for p,q for a,b,c,d being set st I[p,q,a,b,c] & I[p,q,a,b,d] holds c = d;
A4: for p,q for a,b being set ex c being set st C[p,q,a,b,c];
consider M being ManySortedSet of HP-WFF such that
A5: M.VERUM = V() and
A6: for n holds M.prop n = P(n) and
A7: for p,q holds C[p,q,M.p,M.q,M.(p '&' q)] & I[p,q,M.p,M.q,M.(p => q)]
from HPMSSExL(A4,A1,A2,A3);
take M;
thus M.VERUM = V() by A5;
thus for n holds M.prop n = P(n) by A6;
let p,q;
set x = M.p, y = M.q;
thus M.(p '&' q) = C(x,y) by A7;
thus thesis by A7;
end;
begin :: The tree of the subformulae
definition
func HP-Subformulae -> ManySortedSet of HP-WFF means
:Def9:
it.VERUM =
root-tree VERUM & (for n holds it.prop n = root-tree prop n) & for p,q ex p9,q9
being DecoratedTree of HP-WFF st p9 = it.p & q9 = it.q & it.(p '&' q) = (p '&'
q)-tree(p9,q9) & it.(p => q) = (p => q)-tree(p9,q9);
existence
proof
deffunc P(Element of NAT)=root-tree prop $1;
defpred I[Element of HP-WFF,Element of HP-WFF,set,set,set] means ($3 is
DecoratedTree of HP-WFF & $4 is DecoratedTree of HP-WFF implies ex p9,q9 being
DecoratedTree of HP-WFF st p9 = $3 & q9 = $4 & $5 = ($1 => $2)-tree(p9,q9)) & (
$3 is not DecoratedTree of HP-WFF or $4 is not DecoratedTree of HP-WFF implies
$5 = {});
defpred C[Element of HP-WFF,Element of HP-WFF,set,set,set] means ($3 is
DecoratedTree of HP-WFF & $4 is DecoratedTree of HP-WFF implies ex p9,q9 being
DecoratedTree of HP-WFF st p9 = $3 & q9 = $4 & $5 = ($1 '&' $2)-tree(p9,q9)) &
($3 is not DecoratedTree of HP-WFF or $4 is not DecoratedTree of HP-WFF implies
$5 = {});
A1: for p,q for a,b being set ex c being set st C[p,q,a,b,c]
proof
let p,q;
let a,b be set;
per cases;
suppose that
A2: a is DecoratedTree of HP-WFF and
A3: b is DecoratedTree of HP-WFF;
reconsider q9 = b as DecoratedTree of HP-WFF by A3;
reconsider p9 = a as DecoratedTree of HP-WFF by A2;
take (p '&' q)-tree(p9,q9);
thus thesis;
end;
suppose
a is not DecoratedTree of HP-WFF or b is not DecoratedTree of HP-WFF;
hence thesis;
end;
end;
A4: for p,q for a,b being set ex d being set st I[p,q,a,b,d]
proof
let p,q;
let a,b be set;
per cases;
suppose that
A5: a is DecoratedTree of HP-WFF and
A6: b is DecoratedTree of HP-WFF;
reconsider q9 = b as DecoratedTree of HP-WFF by A6;
reconsider p9 = a as DecoratedTree of HP-WFF by A5;
take (p => q)-tree(p9,q9);
thus thesis;
end;
suppose
a is not DecoratedTree of HP-WFF or b is not DecoratedTree of HP-WFF;
hence thesis;
end;
end;
A7: for p,q for a,b,c,d being set st I[p,q,a,b,c] & I[p,q,a,b,d] holds c = d;
A8: for p,q for a,b,c,d being set st C[p,q,a,b,c] & C[p,q,a,b,d] holds c = d;
consider M being ManySortedSet of HP-WFF such that
A9: M.VERUM = root-tree VERUM and
A10: for n holds M.prop n = P(n) and
A11: for p,q holds C[p,q,M.p,M.q,M.(p '&' q)] & I[p,q,M.p,M.q,M.(p =>
q)] from HPMSSExL(A1,A4,A8,A7);
take M;
thus M.VERUM = root-tree VERUM by A9;
thus for n holds M.prop n = root-tree prop n by A10;
let p,q;
A12: ( C[p,q,M.p,M.q,M.(p '&' q)])& I[p,q,M.p,M.q,M.(p => q)] by A11;
defpred P[Element of HP-WFF] means M.$1 is DecoratedTree of HP-WFF;
A13: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s such that
A14: M.r is DecoratedTree of HP-WFF & M.s is DecoratedTree of HP-WFF;
C[r,s,M.r,M.s,M.(r '&' s)] by A11;
hence M.(r '&' s) is DecoratedTree of HP-WFF by A14;
I[r,s,M.r,M.s,M.(r => s)] by A11;
hence thesis by A14;
end;
A15: for n holds P[prop n]
proof
let n;
M.prop n = root-tree prop n by A10;
hence thesis;
end;
A16: P[VERUM] by A9;
for p holds P[p] from HPInd(A16,A15,A13);
hence thesis by A12;
end;
uniqueness
proof
let M1,M2 be ManySortedSet of HP-WFF such that
A17: M1.VERUM = root-tree VERUM and
A18: for n holds M1.prop n = root-tree prop n and
A19: for p,q ex p9,q9 being DecoratedTree of HP-WFF st p9 = M1.p & q9
= M1.q & M1.(p '&' q) = (p '&' q)-tree(p9,q9) & M1.(p => q) = (p => q)-tree(p9,
q9) and
A20: M2.VERUM = root-tree VERUM and
A21: for n holds M2.prop n = root-tree prop n and
A22: for p,q ex p9,q9 being DecoratedTree of HP-WFF st p9 = M2.p & q9
= M2.q & M2.(p '&' q) = (p '&' q)-tree(p9,q9) & M2.(p => q) = (p => q)-tree(p9,
q9);
defpred P[Element of HP-WFF] means M1.$1=M2.$1;
A23: for n holds P[prop n]
proof
let n;
thus M1.prop n = root-tree prop n by A18
.= M2.prop n by A21;
end;
A24: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s such that
A25: M1.r=M2.r & M1.s=M2.s;
A26: (ex p9,q9 being DecoratedTree of HP-WFF st p9 = M1.r & q9 = M1.s &
M1.(r '&' s) = (r '&' s)-tree(p9,q9) & M1.(r => s) = (r => s)-tree( p9,q9) )&
ex p9, q9 being DecoratedTree of HP-WFF st p9 = M2.r & q9 = M2.s & M2.(r '&' s)
= (r '&' s)-tree(p9,q9) & M2.(r => s) = (r => s)-tree( p9,q9) by A19,A22;
hence M1.(r '&' s) = M2.(r '&' s) by A25;
thus thesis by A25,A26;
end;
A27: P[VERUM] by A17,A20;
for r holds P[r] from HPInd(A27,A23,A24);
then for r being object st r in HP-WFF holds M1.r=M2.r;
hence M1 = M2 by PBOOLE:3;
end;
end;
definition
let p;
func Subformulae p -> DecoratedTree of HP-WFF equals
HP-Subformulae.p;
correctness
proof
defpred P[Element of HP-WFF] means HP-Subformulae.$1 is DecoratedTree of
HP-WFF;
A1: for n holds P[prop n]
proof
let n;
HP-Subformulae.prop n = root-tree prop n by Def9;
hence thesis;
end;
A2: for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s]
proof
let r,s;
ex p9,q9 being DecoratedTree of HP-WFF st p9 = HP-Subformulae.r & q9
= HP-Subformulae.s & HP-Subformulae.(r '&' s) = (r '&' s)-tree(p9,q9) &
HP-Subformulae.(r => s) = (r => s)-tree(p9,q9) by Def9;
hence thesis;
end;
A3: P[VERUM] by Def9;
for p holds P[p] from HPInd(A3,A1,A2);
hence thesis;
end;
end;
theorem Th30:
Subformulae VERUM = root-tree VERUM by Def9;
theorem
Subformulae prop n = root-tree prop n by Def9;
theorem Th32:
Subformulae(p '&' q) = (p '&' q)-tree(Subformulae p,Subformulae q)
proof
ex p9,q9 being DecoratedTree of HP-WFF st p9 = HP-Subformulae.p & q9 =
HP-Subformulae.q & HP-Subformulae.(p '&' q) = (p '&' q)-tree(p9,q9) &
HP-Subformulae.(p => q) = (p => q)-tree(p9,q9) by Def9;
hence thesis;
end;
theorem Th33:
Subformulae(p => q) = (p => q)-tree(Subformulae p,Subformulae q)
proof
ex p9,q9 being DecoratedTree of HP-WFF st p9 = HP-Subformulae.p & q9 =
HP-Subformulae.q & HP-Subformulae.(p '&' q) = (p '&' q)-tree(p9,q9) &
HP-Subformulae.(p => q) = (p => q)-tree(p9,q9) by Def9;
hence thesis;
end;
theorem Th34:
(Subformulae p).{} = p
proof
per cases by Th9;
suppose
p is conjunctive;
then consider r,s such that
A1: p = r '&' s;
Subformulae p = p-tree(Subformulae r,Subformulae s) by A1,Th32;
hence thesis by Th6;
end;
suppose
p is conditional;
then consider r,s such that
A2: p = r => s;
Subformulae p = p-tree(Subformulae r,Subformulae s) by A2,Th33;
hence thesis by Th6;
end;
suppose
p is simple;
then ex n st p = prop n;
then Subformulae p = root-tree p by Def9;
hence thesis by TREES_4:3;
end;
suppose
p = VERUM;
hence thesis by Th30,TREES_4:3;
end;
end;
theorem Th35:
for f being Element of dom Subformulae p holds (Subformulae p)|f
= Subformulae((Subformulae p).f)
proof
let f be Element of dom Subformulae p;
defpred P[FinSequence of NAT] means ex q being Element of HP-WFF st q = (
Subformulae p).$1 & (Subformulae p)|$1 = Subformulae q;
A1: for f being Element of dom Subformulae p st P[f qua FinSequence of NAT]
for n st f^<*n*> in dom Subformulae p holds P[f^<*n*>qua FinSequence of NAT]
proof
let f be Element of dom Subformulae p;
given q being Element of HP-WFF such that
q = (Subformulae p).f and
A2: (Subformulae p)|f = Subformulae q;
let n such that
A3: f^<*n*> in dom Subformulae p;
A4: (Subformulae p)|(f^<*n*>) = (Subformulae q)|<*n*> by A2,A3,TREES_9:3;
A5: (dom Subformulae p)|f = dom Subformulae q by A2,TREES_2:def 10;
then
A6: <*n*> in dom Subformulae q by A3,TREES_1:def 6;
then
A7: (Subformulae p).(f^<*n*>) = (Subformulae q).<*n*> by A2,A5,TREES_2:def 10;
per cases by Th9;
suppose
q is conjunctive;
then consider r,s such that
A8: q = r '&' s;
A9: Subformulae q = (r '&' s)-tree(Subformulae r,Subformulae s) by A8,Th32;
then
A10: dom Subformulae q = tree(dom Subformulae r, dom Subformulae s) by
TREES_4:14;
now
per cases by A6,A10,Th5;
suppose
A11: n= 0;
take r;
thus r = (Subformulae r).{} by Th34
.= (Subformulae p).(f^<*n*>) by A7,A9,A11,Th7;
thus (Subformulae p)|(f^<*n*>) = Subformulae r by A4,A9,A11,Th8;
end;
suppose
A12: n= 1;
take s;
thus s = (Subformulae s).{} by Th34
.= (Subformulae p).(f^<*n*>) by A7,A9,A12,Th7;
thus (Subformulae p)|(f^<*n*>) = Subformulae s by A4,A9,A12,Th8;
end;
end;
hence thesis;
end;
suppose
q is conditional;
then consider r,s such that
A13: q = r => s;
A14: Subformulae q = (r => s)-tree(Subformulae r,Subformulae s) by A13,Th33;
then
A15: dom Subformulae q = tree(dom Subformulae r, dom Subformulae s) by
TREES_4:14;
now
per cases by A6,A15,Th5;
suppose
A16: n= 0;
take r;
thus r = (Subformulae r).{} by Th34
.= (Subformulae p).(f^<*n*>) by A7,A14,A16,Th7;
thus (Subformulae p)|(f^<*n*>) = Subformulae r by A4,A14,A16,Th8;
end;
suppose
A17: n= 1;
take s;
thus s = (Subformulae s).{} by Th34
.= (Subformulae p).(f^<*n*>) by A7,A14,A17,Th7;
thus (Subformulae p)|(f^<*n*>) = Subformulae s by A4,A14,A17,Th8;
end;
end;
hence thesis;
end;
suppose
q is simple;
then consider k such that
A18: q = prop k;
Subformulae q = root-tree prop k by A18,Def9;
then dom Subformulae q = { {} } by TREES_1:29,TREES_4:3;
hence thesis by A6,TARSKI:def 1;
end;
suppose
q = VERUM;
then dom Subformulae q = { {} } by Th30,TREES_1:29,TREES_4:3;
hence thesis by A6,TARSKI:def 1;
end;
end;
(Subformulae p).{} = p by Th34;
then
A19: P[(<*>NAT) qua FinSequence of NAT] by TREES_9:1;
for f being Element of dom Subformulae p holds P[f qua FinSequence of
NAT] from InTreeInd(A19,A1);
then P[f qua FinSequence of NAT];
hence thesis;
end;
theorem
p in Leaves Subformulae q implies p = VERUM or p is simple
proof
assume p in Leaves Subformulae q;
then p in (Subformulae q).:Leaves dom Subformulae q by TREES_2:def 9;
then consider x being object such that
A1: x in dom Subformulae q and
A2: x in Leaves dom Subformulae q and
A3: p = (Subformulae q).x by FUNCT_1:def 6;
reconsider f = x as Element of dom Subformulae q by A1;
A4: (Subformulae q)|f = Subformulae p by A3,Th35;
A5: p is not conditional
proof
assume not thesis;
then consider r,s such that
A6: p = r => s;
Subformulae p = p-tree(Subformulae r,Subformulae s) by A6,Th33;
hence contradiction by A2,A4,TREES_9:6;
end;
p is not conjunctive
proof
assume not thesis;
then consider r,s such that
A7: p = r '&' s;
Subformulae p = p-tree(Subformulae r,Subformulae s) by A7,Th32;
hence contradiction by A2,A4,TREES_9:6;
end;
hence thesis by A5,Th9;
end;