:: MODAL_1 semantic presentation
begin
Lm1: for m being Element of NAT holds {} is_a_proper_prefix_of <*m*>
proof
let m be Element of NAT ; ::_thesis: {} is_a_proper_prefix_of <*m*>
{} is_a_prefix_of <*m*> by XBOOLE_1:2;
hence {} is_a_proper_prefix_of <*m*> by XBOOLE_0:def_8; ::_thesis: verum
end;
definition
let Z be Tree;
func Root Z -> Element of Z equals :: MODAL_1:def 1
{} ;
coherence
{} is Element of Z by TREES_1:22;
end;
:: deftheorem defines Root MODAL_1:def_1_:_
for Z being Tree holds Root Z = {} ;
definition
let D be non empty set ;
let T be DecoratedTree of D;
func Root T -> Element of D equals :: MODAL_1:def 2
T . (Root (dom T));
coherence
T . (Root (dom T)) is Element of D ;
end;
:: deftheorem defines Root MODAL_1:def_2_:_
for D being non empty set
for T being DecoratedTree of D holds Root T = T . (Root (dom T));
theorem Th1: :: MODAL_1:1
for n, m being Element of NAT
for s being FinSequence of NAT st n <> m holds
not <*n*>,<*m*> ^ s are_c=-comparable
proof
let n, m be Element of NAT ; ::_thesis: for s being FinSequence of NAT st n <> m holds
not <*n*>,<*m*> ^ s are_c=-comparable
let s be FinSequence of NAT ; ::_thesis: ( n <> m implies not <*n*>,<*m*> ^ s are_c=-comparable )
assume A1: n <> m ; ::_thesis: not <*n*>,<*m*> ^ s are_c=-comparable
assume A2: <*n*>,<*m*> ^ s are_c=-comparable ; ::_thesis: contradiction
percases ( <*n*> is_a_prefix_of <*m*> ^ s or <*m*> ^ s is_a_prefix_of <*n*> ) by A2, XBOOLE_0:def_9;
suppose <*n*> is_a_prefix_of <*m*> ^ s ; ::_thesis: contradiction
then A3: ex a being 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; ::_thesis: verum
end;
suppose <*m*> ^ s is_a_prefix_of <*n*> ; ::_thesis: contradiction
then consider a being FinSequence such that
A4: <*n*> = (<*m*> ^ s) ^ a by TREES_1:1;
n = ((<*m*> ^ s) ^ a) . 1 by A4, FINSEQ_1:40
.= (<*m*> ^ (s ^ a)) . 1 by FINSEQ_1:32
.= m by FINSEQ_1:41 ;
hence contradiction by A1; ::_thesis: verum
end;
end;
end;
theorem :: MODAL_1:2
for s being FinSequence of NAT st s <> {} holds
ex w being FinSequence of NAT ex n being Element of NAT st s = <*n*> ^ w by FINSEQ_2:130;
theorem Th3: :: MODAL_1:3
for n, m being Element of NAT
for s being FinSequence of NAT st n <> m holds
not <*n*> is_a_proper_prefix_of <*m*> ^ s
proof
let n, m be Element of NAT ; ::_thesis: for s being FinSequence of NAT st n <> m holds
not <*n*> is_a_proper_prefix_of <*m*> ^ s
let s be FinSequence of NAT ; ::_thesis: ( n <> m implies not <*n*> is_a_proper_prefix_of <*m*> ^ s )
assume A1: n <> m ; ::_thesis: not <*n*> is_a_proper_prefix_of <*m*> ^ s
assume <*n*> is_a_proper_prefix_of <*m*> ^ s ; ::_thesis: contradiction
then <*n*> is_a_prefix_of <*m*> ^ s by XBOOLE_0:def_8;
then A2: ex a being 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; ::_thesis: verum
end;
theorem :: MODAL_1:4
for n, m being Element of NAT
for s being FinSequence of NAT st n <> m holds
not <*n*> is_a_prefix_of <*m*> ^ s by TREES_1:50;
theorem :: MODAL_1:5
for n, m being Element of NAT holds not <*n*> is_a_proper_prefix_of <*m*> by TREES_1:52;
theorem :: MODAL_1:6
elementary_tree 1 = {{},<*0*>} by TREES_1:51;
theorem :: MODAL_1:7
elementary_tree 2 = {{},<*0*>,<*1*>} by TREES_1:53;
theorem Th8: :: MODAL_1:8
for Z being Tree
for n, m being Element of NAT 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; ::_thesis: for n, m being Element of NAT st n <= m & <*m*> in Z holds
<*n*> in Z
let n, m be Element of NAT ; ::_thesis: ( n <= m & <*m*> in Z implies <*n*> in Z )
assume that
A1: n <= m and
A2: <*m*> in Z ; ::_thesis: <*n*> in Z
{} ^ <*m*> in Z by A2, FINSEQ_1:34;
then s ^ <*n*> in Z by A1, TREES_1:def_3;
hence <*n*> in Z by FINSEQ_1:34; ::_thesis: verum
end;
theorem :: MODAL_1:9
for w, t, s being FinSequence of NAT st w ^ t is_a_proper_prefix_of w ^ s holds
t is_a_proper_prefix_of s by TREES_1:49;
theorem Th10: :: MODAL_1:10
for t1 being DecoratedTree of [:NAT,NAT:] holds t1 in PFuncs ((NAT *),[:NAT,NAT:])
proof
let t1 be DecoratedTree of [:NAT,NAT:]; ::_thesis: t1 in PFuncs ((NAT *),[:NAT,NAT:])
( rng t1 c= [:NAT,NAT:] & dom t1 c= NAT * ) by TREES_1:def_3;
hence t1 in PFuncs ((NAT *),[:NAT,NAT:]) by PARTFUN1:def_3; ::_thesis: verum
end;
theorem Th11: :: MODAL_1:11
for Z, Z1, Z2 being Tree
for 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; ::_thesis: for z being Element of Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds
Z1 = Z2
let z be Element of Z; ::_thesis: ( Z with-replacement (z,Z1) = Z with-replacement (z,Z2) implies Z1 = Z2 )
assume A1: Z with-replacement (z,Z1) = Z with-replacement (z,Z2) ; ::_thesis: Z1 = Z2
now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_
(_(_s_in_Z1_implies_s_in_Z2_)_&_(_s_in_Z2_implies_s_in_Z1_)_)
let s be FinSequence of NAT ; ::_thesis: ( ( s in Z1 implies s in Z2 ) & ( s in Z2 implies b1 in Z1 ) )
thus ( s in Z1 implies s in Z2 ) ::_thesis: ( s in Z2 implies b1 in Z1 )
proof
assume A2: s in Z1 ; ::_thesis: s in Z2
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: s in Z2
hence s in Z2 by TREES_1:22; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: s in Z2
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 being FinSequence of NAT st
( w in Z2 & z ^ s = z ^ w ) by A3, TREES_1:def_9;
hence s in Z2 by FINSEQ_1:33; ::_thesis: verum
end;
end;
end;
assume A4: s in Z2 ; ::_thesis: b1 in Z1
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: b1 in Z1
hence s in Z1 by TREES_1:22; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: b1 in Z1
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 being FinSequence of NAT st
( w in Z1 & z ^ s = z ^ w ) by A5, TREES_1:def_9;
hence s in Z1 by FINSEQ_1:33; ::_thesis: verum
end;
end;
end;
hence Z1 = Z2 by TREES_2:def_1; ::_thesis: verum
end;
theorem Th12: :: MODAL_1:12
for D being non empty set
for Z, Z1, Z2 being DecoratedTree of D
for z being Element of dom Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds
Z1 = Z2
proof
let D be non empty set ; ::_thesis: for Z, Z1, Z2 being DecoratedTree of D
for z being Element of dom Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds
Z1 = Z2
let Z, Z1, Z2 be DecoratedTree of D; ::_thesis: for z being Element of dom Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds
Z1 = Z2
let z be Element of dom Z; ::_thesis: ( Z with-replacement (z,Z1) = Z with-replacement (z,Z2) implies Z1 = Z2 )
assume A1: Z with-replacement (z,Z1) = Z with-replacement (z,Z2) ; ::_thesis: Z1 = Z2
set T2 = Z with-replacement (z,Z2);
set T1 = Z with-replacement (z,Z1);
A2: dom (Z with-replacement (z,Z1)) = (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 being FinSequence of NAT st s in dom Z1 holds
Z1 . s = Z2 . s
proof
let s be FinSequence of NAT ; ::_thesis: ( s in dom Z1 implies Z1 . s = Z2 . s )
A5: z is_a_prefix_of z ^ s by TREES_1:1;
assume A6: s in dom Z1 ; ::_thesis: Z1 . s = Z2 . s
then z ^ s in (dom Z) with-replacement (z,(dom Z1)) by TREES_1:def_9;
then A7: ex u being FinSequence of NAT st
( u in dom Z1 & z ^ s = z ^ u & (Z with-replacement (z,Z1)) . (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 being FinSequence of NAT such that
w in dom Z2 and
A8: z ^ s = z ^ w and
A9: (Z with-replacement (z,Z2)) . (z ^ s) = Z2 . w by A5, TREES_2:def_11;
s = w by A8, FINSEQ_1:33;
hence Z1 . s = Z2 . s by A1, A9, A7, FINSEQ_1:33; ::_thesis: verum
end;
dom (Z with-replacement (z,Z2)) = (dom Z) with-replacement (z,(dom Z2)) by TREES_2:def_11;
hence Z1 = Z2 by A1, A2, A4, Th11, TREES_2:31; ::_thesis: verum
end;
theorem Th13: :: MODAL_1:13
for Z1, Z2 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for 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; ::_thesis: for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds
succ v = succ w
let p be FinSequence of NAT ; ::_thesis: ( p in Z1 implies for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds
succ v = succ w )
assume A1: p in Z1 ; ::_thesis: for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds
succ v = succ w
set Z = Z1 with-replacement (p,Z2);
let v be Element of Z1 with-replacement (p,Z2); ::_thesis: for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds
succ v = succ w
let w be Element of Z1; ::_thesis: ( v = w & w is_a_proper_prefix_of p implies succ v = succ w )
assume that
A2: v = w and
A3: w is_a_proper_prefix_of p ; ::_thesis: succ v = succ w
w is_a_prefix_of p by A3, XBOOLE_0:def_8;
then consider r being FinSequence such that
A4: p = w ^ r by TREES_1:1;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_r_holds_
r_._n_in_NAT
let n be Nat; ::_thesis: ( n in dom r implies r . n in NAT )
assume A5: n in dom r ; ::_thesis: r . n in NAT
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; ::_thesis: verum
end;
then reconsider r = r as FinSequence of NAT by FINSEQ_2:12;
A7: r <> {} by A3, A4, FINSEQ_1:34;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_succ_v_implies_x_in_succ_w_)_&_(_x_in_succ_w_implies_x_in_succ_v_)_)
let x be set ; ::_thesis: ( ( x in succ v implies x in succ w ) & ( x in succ w implies x in succ v ) )
thus ( x in succ v implies x in succ w ) ::_thesis: ( x in succ w implies x in succ v )
proof
assume x in succ v ; ::_thesis: x in succ w
then x in { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in Z1 with-replacement (p,Z2) } by TREES_2:def_5;
then consider n being Element of NAT such that
A8: x = v ^ <*n*> and
A9: v ^ <*n*> in Z1 with-replacement (p,Z2) ;
reconsider x9 = x as FinSequence of NAT by A8;
now__::_thesis:_x_in_succ_w
percases ( ( x9 in Z1 & not p is_a_proper_prefix_of x9 ) or ex r being FinSequence of NAT st
( r in Z2 & x9 = p ^ r ) ) by A1, A8, A9, TREES_1:def_9;
suppose ( x9 in Z1 & not p is_a_proper_prefix_of x9 ) ; ::_thesis: x in succ w
then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A2, A8;
hence x in succ w by TREES_2:def_5; ::_thesis: verum
end;
suppose ex r being FinSequence of NAT st
( r in Z2 & x9 = p ^ r ) ; ::_thesis: x in succ w
then consider s being FinSequence of NAT 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 s = {} ; ::_thesis: contradiction
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 ; ::_thesis: verum
end;
then <*n*> = r by A11, FINSEQ_1:34;
then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A1, A2, A4, A8;
hence x in succ w by TREES_2:def_5; ::_thesis: verum
end;
end;
end;
hence x in succ w ; ::_thesis: verum
end;
assume x in succ w ; ::_thesis: x in succ v
then x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in Z1 } by TREES_2:def_5;
then consider n being Element of NAT such that
A13: x = w ^ <*n*> and
A14: w ^ <*n*> in Z1 ;
now__::_thesis:_v_^_<*n*>_in_Z1_with-replacement_(p,Z2)
assume A15: not v ^ <*n*> in Z1 with-replacement (p,Z2) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( not v ^ <*n*> in Z1 or p is_a_proper_prefix_of v ^ <*n*> ) by A1, A15, TREES_1:def_9;
suppose not v ^ <*n*> in Z1 ; ::_thesis: contradiction
hence contradiction by A2, A14; ::_thesis: verum
end;
suppose p is_a_proper_prefix_of v ^ <*n*> ; ::_thesis: contradiction
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; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
then x in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in Z1 with-replacement (p,Z2) } by A2, A13;
hence x in succ v by TREES_2:def_5; ::_thesis: verum
end;
hence succ v = succ w by TARSKI:1; ::_thesis: verum
end;
theorem Th14: :: MODAL_1:14
for Z1, Z2 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for 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; ::_thesis: for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w
let p be FinSequence of NAT ; ::_thesis: ( p in Z1 implies for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w )
assume A1: p in Z1 ; ::_thesis: for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w
set Z = Z1 with-replacement (p,Z2);
let v be Element of Z1 with-replacement (p,Z2); ::_thesis: for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w
let w be Element of Z1; ::_thesis: ( v = w & not p,w are_c=-comparable implies succ v = succ w )
assume that
A2: v = w and
A3: not p,w are_c=-comparable ; ::_thesis: succ v = succ w
A4: not p is_a_prefix_of w by A3, XBOOLE_0:def_9;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_succ_v_implies_x_in_succ_w_)_&_(_x_in_succ_w_implies_x_in_succ_v_)_)
let x be set ; ::_thesis: ( ( x in succ v implies x in succ w ) & ( x in succ w implies x in succ v ) )
thus ( x in succ v implies x in succ w ) ::_thesis: ( x in succ w implies x in succ v )
proof
assume x in succ v ; ::_thesis: x in succ w
then x in { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in Z1 with-replacement (p,Z2) } by TREES_2:def_5;
then consider n being Element of NAT such that
A5: x = v ^ <*n*> and
A6: v ^ <*n*> in Z1 with-replacement (p,Z2) ;
reconsider x9 = x as FinSequence of NAT by A5;
v ^ <*n*> in Z1
proof
assume A7: not v ^ <*n*> in Z1 ; ::_thesis: contradiction
then ex t being FinSequence of NAT 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;
percases ( p is_a_proper_prefix_of v ^ <*n*> or p = v ^ <*n*> ) by A8, XBOOLE_0:def_8;
suppose p is_a_proper_prefix_of v ^ <*n*> ; ::_thesis: contradiction
hence contradiction by A2, A4, TREES_1:9; ::_thesis: verum
end;
suppose p = v ^ <*n*> ; ::_thesis: contradiction
hence contradiction by A1, A7; ::_thesis: verum
end;
end;
end;
then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A2, A5;
hence x in succ w by TREES_2:def_5; ::_thesis: verum
end;
assume x in succ w ; ::_thesis: x in succ v
then x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in Z1 } by TREES_2:def_5;
then consider n being Element of NAT such that
A9: x = w ^ <*n*> and
A10: w ^ <*n*> in Z1 ;
not p is_a_proper_prefix_of w ^ <*n*> by A4, TREES_1:9;
then v ^ <*n*> in Z1 with-replacement (p,Z2) by A1, A2, A10, TREES_1:def_9;
then x in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in Z1 with-replacement (p,Z2) } by A2, A9;
hence x in succ v by TREES_2:def_5; ::_thesis: verum
end;
hence succ v = succ w by TARSKI:1; ::_thesis: verum
end;
theorem :: MODAL_1:15
for Z1, Z2 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z2 st v = p ^ w holds
succ v, succ w are_equipotent by TREES_2:37;
theorem Th16: :: MODAL_1:16
for Z1 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1
for w being Element of Z1 | p st v = p ^ w holds
succ v, succ w are_equipotent
proof
let Z1 be Tree; ::_thesis: for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1
for w being Element of Z1 | p st v = p ^ w holds
succ v, succ w are_equipotent
let p be FinSequence of NAT ; ::_thesis: ( p in Z1 implies for v being Element of Z1
for w being Element of Z1 | p st v = p ^ w holds
succ v, succ w are_equipotent )
assume A1: p in Z1 ; ::_thesis: for v being Element of Z1
for w being Element of Z1 | p st v = p ^ w holds
succ v, succ w are_equipotent
set T = Z1 | p;
let t be Element of Z1; ::_thesis: for w being Element of Z1 | p st t = p ^ w holds
succ t, succ w are_equipotent
let t2 be Element of Z1 | p; ::_thesis: ( t = p ^ t2 implies succ t, succ t2 are_equipotent )
assume A2: t = p ^ t2 ; ::_thesis: succ t, succ t2 are_equipotent
A3: for n being Element of NAT holds
( t ^ <*n*> in Z1 iff t2 ^ <*n*> in Z1 | p )
proof
let n be Element of NAT ; ::_thesis: ( t ^ <*n*> in Z1 iff t2 ^ <*n*> in Z1 | p )
A4: t ^ <*n*> = p ^ (t2 ^ <*n*>) by A2, FINSEQ_1:32;
hence ( t ^ <*n*> in Z1 implies t2 ^ <*n*> in Z1 | p ) by A1, TREES_1:def_6; ::_thesis: ( t2 ^ <*n*> in Z1 | p implies t ^ <*n*> in Z1 )
assume t2 ^ <*n*> in Z1 | p ; ::_thesis: t ^ <*n*> in Z1
hence t ^ <*n*> in Z1 by A1, A4, TREES_1:def_6; ::_thesis: verum
end;
defpred S1[ set , set ] means for n being Element of NAT st $1 = t ^ <*n*> holds
$2 = t2 ^ <*n*>;
A5: for x being set st x in succ t holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in succ t implies ex y being set st S1[x,y] )
assume x in succ t ; ::_thesis: ex y being set st S1[x,y]
then x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by TREES_2:def_5;
then consider n being Element of NAT such that
A6: x = t ^ <*n*> and
t ^ <*n*> in Z1 ;
take t2 ^ <*n*> ; ::_thesis: S1[x,t2 ^ <*n*>]
let m be Element of NAT ; ::_thesis: ( x = t ^ <*m*> implies t2 ^ <*n*> = t2 ^ <*m*> )
assume x = t ^ <*m*> ; ::_thesis: t2 ^ <*n*> = t2 ^ <*m*>
hence t2 ^ <*n*> = t2 ^ <*m*> by A6, FINSEQ_1:33; ::_thesis: verum
end;
consider f being Function such that
A7: ( dom f = succ t & ( for x being set st x in succ t holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A5);
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_rng_f_implies_x_in_succ_t2_)_&_(_x_in_succ_t2_implies_x_in_rng_f_)_)
let x be set ; ::_thesis: ( ( x in rng f implies x in succ t2 ) & ( x in succ t2 implies x in rng f ) )
thus ( x in rng f implies x in succ t2 ) ::_thesis: ( x in succ t2 implies x in rng f )
proof
assume x in rng f ; ::_thesis: x in succ t2
then consider y being set such that
A8: y in dom f and
A9: x = f . y by FUNCT_1:def_3;
y in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A7, A8, TREES_2:def_5;
then consider n being Element of NAT such that
A10: y = t ^ <*n*> and
A11: t ^ <*n*> in Z1 ;
A12: t2 ^ <*n*> in Z1 | p by A3, A11;
x = t2 ^ <*n*> by A7, A8, A9, A10;
then x in { (t2 ^ <*m*>) where m is Element of NAT : t2 ^ <*m*> in Z1 | p } by A12;
hence x in succ t2 by TREES_2:def_5; ::_thesis: verum
end;
assume x in succ t2 ; ::_thesis: x in rng f
then x in { (t2 ^ <*n*>) where n is Element of NAT : t2 ^ <*n*> in Z1 | p } by TREES_2:def_5;
then consider n being Element of NAT such that
A13: x = t2 ^ <*n*> and
A14: t2 ^ <*n*> in Z1 | p ;
t ^ <*n*> in Z1 by A3, A14;
then t ^ <*n*> in { (t ^ <*m*>) where m is Element of NAT : 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; ::_thesis: verum
end;
then A16: rng f = succ t2 by TARSKI:1;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A17: x1 in dom f and
A18: x2 in dom f and
A19: f . x1 = f . x2 ; ::_thesis: x1 = x2
x2 in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A7, A18, TREES_2:def_5;
then consider k being Element of NAT such that
A20: x2 = t ^ <*k*> and
t ^ <*k*> in Z1 ;
x1 in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A7, A17, TREES_2:def_5;
then consider m being Element of NAT 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; ::_thesis: verum
end;
then f is one-to-one by FUNCT_1:def_4;
hence succ t, succ t2 are_equipotent by A7, A16, WELLORD2:def_4; ::_thesis: verum
end;
theorem Th17: :: MODAL_1:17
for Z being finite Tree st branchdeg (Root Z) = 0 holds
( card Z = 1 & Z = {{}} )
proof
let Z be finite Tree; ::_thesis: ( branchdeg (Root Z) = 0 implies ( card Z = 1 & Z = {{}} ) )
assume branchdeg (Root Z) = 0 ; ::_thesis: ( card Z = 1 & Z = {{}} )
then 0 = card (succ (Root Z)) by TREES_2:def_12;
then A1: succ (Root Z) = {} ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Z_implies_x_in_{(Root_Z)}_)_&_(_x_in_{(Root_Z)}_implies_x_in_Z_)_)
let x be set ; ::_thesis: ( ( x in Z implies x in {(Root Z)} ) & ( x in {(Root Z)} implies x in Z ) )
thus ( x in Z implies x in {(Root Z)} ) ::_thesis: ( x in {(Root Z)} implies x in Z )
proof
assume x in Z ; ::_thesis: x in {(Root Z)}
then reconsider z = x as Element of Z ;
assume not x in {(Root Z)} ; ::_thesis: contradiction
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; ::_thesis: verum
end;
assume x in {(Root Z)} ; ::_thesis: x in Z
then reconsider x9 = x as Element of Z ;
x9 in Z ;
hence x in Z ; ::_thesis: verum
end;
then Z = {(Root Z)} by TARSKI:1;
hence ( card Z = 1 & Z = {{}} ) by CARD_2:42; ::_thesis: verum
end;
theorem Th18: :: MODAL_1:18
for Z being finite Tree st branchdeg (Root Z) = 1 holds
succ (Root Z) = {<*0*>}
proof
let Z be finite Tree; ::_thesis: ( branchdeg (Root Z) = 1 implies succ (Root Z) = {<*0*>} )
assume branchdeg (Root Z) = 1 ; ::_thesis: succ (Root Z) = {<*0*>}
then card (succ (Root Z)) = 1 by TREES_2:def_12;
then consider x being set 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*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A2, TREES_2:def_5;
then consider m being Element of NAT such that
A3: x9 = (Root Z) ^ <*m*> and
A4: (Root Z) ^ <*m*> in Z ;
A5: x9 = <*m*> by A3, FINSEQ_1:34;
now__::_thesis:_not_m_<>_0
A6: <*0*> = (Root Z) ^ <*0*> by FINSEQ_1:34;
<*m*> in Z by A4, FINSEQ_1:34;
then <*0*> in Z by Th8, NAT_1:2;
then (Root Z) ^ <*0*> in succ (Root Z) by A6, TREES_2:12;
then A7: <*0*> = x by A1, A6, TARSKI:def_1;
assume m <> 0 ; ::_thesis: contradiction
hence contradiction by A5, A7, TREES_1:3; ::_thesis: verum
end;
hence succ (Root Z) = {<*0*>} by A1, A3, FINSEQ_1:34; ::_thesis: verum
end;
theorem Th19: :: MODAL_1:19
for Z being finite Tree st branchdeg (Root Z) = 2 holds
succ (Root Z) = {<*0*>,<*1*>}
proof
let Z be finite Tree; ::_thesis: ( branchdeg (Root Z) = 2 implies succ (Root Z) = {<*0*>,<*1*>} )
assume branchdeg (Root Z) = 2 ; ::_thesis: succ (Root Z) = {<*0*>,<*1*>}
then card (succ (Root Z)) = 2 by TREES_2:def_12;
then consider x, y being set 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*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A3, TREES_2:def_5;
then consider m being Element of NAT 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*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A6, TREES_2:def_5;
then consider k being Element of NAT such that
A7: y9 = (Root Z) ^ <*k*> and
(Root Z) ^ <*k*> in Z ;
A8: y9 = <*k*> by A7, FINSEQ_1:34;
percases ( m = 0 or m <> 0 ) ;
supposeA9: m = 0 ; ::_thesis: succ (Root Z) = {<*0*>,<*1*>}
now__::_thesis:_not_k_<>_1
A10: <*1*> = (Root Z) ^ <*1*> by FINSEQ_1:34;
assume A11: k <> 1 ; ::_thesis: contradiction
then 2 <= k by A1, A5, A8, A9, NAT_1:26;
then <*1*> in Z by A8, Th8, XXREAL_0:2;
then <*1*> in succ (Root Z) by A10, TREES_2:12;
then ( <*1*> = <*0*> or <*1*> = <*k*> ) by A2, A5, A8, A9, TARSKI:def_2;
hence contradiction by A11, TREES_1:3; ::_thesis: verum
end;
hence succ (Root Z) = {<*0*>,<*1*>} by A2, A4, A8, A9, FINSEQ_1:34; ::_thesis: verum
end;
supposeA12: m <> 0 ; ::_thesis: succ (Root Z) = {<*0*>,<*1*>}
( <*0*> in Z & <*0*> = (Root Z) ^ <*0*> ) by A5, Th8, FINSEQ_1:34, NAT_1:2;
then <*0*> in succ (Root Z) by TREES_2:12;
then A13: ( <*0*> = <*m*> or <*0*> = <*k*> ) by A2, A5, A8, TARSKI:def_2;
now__::_thesis:_not_m_<>_1
A14: <*1*> = (Root Z) ^ <*1*> by FINSEQ_1:34;
assume A15: m <> 1 ; ::_thesis: contradiction
then 2 <= m by A12, NAT_1:26;
then <*1*> in Z by A5, Th8, XXREAL_0:2;
then <*1*> in succ (Root Z) by A14, TREES_2:12;
then ( <*1*> = <*0*> or <*1*> = <*m*> ) by A2, A5, A8, A12, A13, TARSKI:def_2, TREES_1:3;
hence contradiction by A15, TREES_1:3; ::_thesis: verum
end;
hence succ (Root Z) = {<*0*>,<*1*>} by A2, A4, A8, A13, FINSEQ_1:34, TREES_1:3; ::_thesis: verum
end;
end;
end;
theorem Th20: :: MODAL_1:20
for Z being Tree
for o being Element of Z st o <> Root Z holds
( Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent & not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } )
proof
let Z be Tree; ::_thesis: for o being Element of Z st o <> Root Z holds
( Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent & not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } )
let o be Element of Z; ::_thesis: ( o <> Root Z implies ( Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent & not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } ) )
assume A1: o <> Root Z ; ::_thesis: ( Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent & not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } )
set A = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ;
thus Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent ::_thesis: not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z }
proof
defpred S1[ set , set ] means for s being FinSequence of NAT st $1 = s holds
$2 = o ^ s;
A2: for x being set st x in Z | o holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in Z | o implies ex y being set st S1[x,y] )
assume x in Z | o ; ::_thesis: ex y being set st S1[x,y]
then reconsider s = x as FinSequence of NAT by TREES_1:19;
take o ^ s ; ::_thesis: S1[x,o ^ s]
let w be FinSequence of NAT ; ::_thesis: ( x = w implies o ^ s = o ^ w )
assume x = w ; ::_thesis: o ^ s = o ^ w
hence o ^ s = o ^ w ; ::_thesis: verum
end;
ex f being Function st
( dom f = Z | o & ( for x being set st x in Z | o holds
S1[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 set st x in Z | o holds
for s being FinSequence of NAT st x = s holds
f . x = o ^ s ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_rng_f_implies_x_in__{__(o_^_s9)_where_s9_is_Element_of_NAT_*_:_o_^_s9_in_Z__}__)_&_(_x_in__{__(o_^_s9)_where_s9_is_Element_of_NAT_*_:_o_^_s9_in_Z__}__implies_x_in_rng_f_)_)
let x be set ; ::_thesis: ( ( x in rng f implies x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ) & ( x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } implies x in rng f ) )
thus ( x in rng f implies x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ) ::_thesis: ( x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } implies x in rng f )
proof
assume x in rng f ; ::_thesis: x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z }
then consider x1 being set such that
A5: x1 in dom f and
A6: x = f . x1 by FUNCT_1:def_3;
reconsider x1 = x1 as FinSequence of NAT by A3, A5, TREES_1:19;
reconsider x1 = 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 x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; ::_thesis: verum
end;
assume x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; ::_thesis: x in rng f
then consider v9 being Element of NAT * 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; ::_thesis: verum
end;
then A10: rng f = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } by TARSKI:1;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A11: x1 in dom f and
A12: x2 in dom f and
A13: f . x1 = f . x2 ; ::_thesis: x1 = 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; ::_thesis: verum
end;
then f is one-to-one by FUNCT_1:def_4;
hence Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent by A3, A10, WELLORD2:def_4; ::_thesis: verum
end;
assume Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } ; ::_thesis: contradiction
then ex v9 being Element of NAT * st
( Root Z = o ^ v9 & o ^ v9 in Z ) ;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th21: :: MODAL_1:21
for Z being finite Tree
for o being Element of Z st o <> Root Z holds
card (Z | o) < card Z
proof
let Z be finite Tree; ::_thesis: for o being Element of Z st o <> Root Z holds
card (Z | o) < card Z
let o be Element of Z; ::_thesis: ( o <> Root Z implies card (Z | o) < card Z )
assume A1: o <> Root Z ; ::_thesis: card (Z | o) < card Z
set A = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ;
A2: Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent by A1, Th20;
then reconsider A = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } as finite set by CARD_1:38;
reconsider B = A \/ {(Root Z)} as finite set ;
now__::_thesis:_for_x_being_set_st_x_in_B_holds_
x_in_Z
let x be set ; ::_thesis: ( x in B implies x in Z )
assume A3: x in B ; ::_thesis: x in Z
now__::_thesis:_x_in_Z
percases ( x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } or x in {(Root Z)} ) by A3, XBOOLE_0:def_3;
suppose x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; ::_thesis: x in Z
then ex v9 being Element of NAT * st
( x = o ^ v9 & o ^ v9 in Z ) ;
hence x in Z ; ::_thesis: verum
end;
suppose x in {(Root Z)} ; ::_thesis: x in Z
hence x in Z ; ::_thesis: verum
end;
end;
end;
hence x in Z ; ::_thesis: verum
end;
then A4: B c= Z by TARSKI:def_3;
card B = (card A) + 1 by A1, Th20, CARD_2:41
.= (card (Z | o)) + 1 by A2, CARD_1:5 ;
then (card (Z | o)) + 1 <= card Z by A4, NAT_1:43;
hence card (Z | o) < card Z by NAT_1:13; ::_thesis: verum
end;
theorem Th22: :: MODAL_1:22
for Z being finite Tree
for 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; ::_thesis: for z being Element of Z st succ (Root Z) = {z} holds
Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z))
let z be Element of Z; ::_thesis: ( succ (Root Z) = {z} implies Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) )
set e = elementary_tree 1;
A1: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
A2: {} in Z by TREES_1:22;
assume A3: succ (Root Z) = {z} ; ::_thesis: Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z))
then card (succ (Root Z)) = 1 by CARD_1:30;
then branchdeg (Root Z) = 1 by TREES_2:def_12;
then {z} = {<*0*>} by A3, Th18;
then z in {<*0*>} by TARSKI:def_1;
then A4: z = <*0*> by TARSKI:def_1;
then A5: <*0*> in Z ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Z_implies_x_in_(elementary_tree_1)_with-replacement_(<*0*>,(Z_|_z))_)_&_(_x_in_(elementary_tree_1)_with-replacement_(<*0*>,(Z_|_z))_implies_x_in_Z_)_)
let x be set ; ::_thesis: ( ( x in Z implies x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) & ( x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) implies b1 in Z ) )
thus ( x in Z implies x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) ::_thesis: ( x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) implies b1 in Z )
proof
assume x in Z ; ::_thesis: x in (elementary_tree 1) with-replacement (<*0*>,(Z | z))
then reconsider x9 = x as Element of Z ;
percases ( x9 = {} or x9 <> {} ) ;
suppose x9 = {} ; ::_thesis: x in (elementary_tree 1) with-replacement (<*0*>,(Z | z))
hence x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by TREES_1:22; ::_thesis: verum
end;
suppose x9 <> {} ; ::_thesis: x in (elementary_tree 1) with-replacement (<*0*>,(Z | z))
then consider w being 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 x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by A1, A6, A9, TREES_1:def_9; ::_thesis: verum
end;
end;
end;
assume x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ; ::_thesis: b1 in Z
then reconsider x9 = x as Element of (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ;
percases ( ( x9 in elementary_tree 1 & not <*0*> is_a_proper_prefix_of x9 ) or ex s being FinSequence of NAT st
( s in Z | z & x9 = <*0*> ^ s ) ) by A1, TREES_1:def_9;
suppose ( x9 in elementary_tree 1 & not <*0*> is_a_proper_prefix_of x9 ) ; ::_thesis: b1 in Z
hence x in Z by A5, A2, TARSKI:def_2, TREES_1:51; ::_thesis: verum
end;
suppose ex s being FinSequence of NAT st
( s in Z | z & x9 = <*0*> ^ s ) ; ::_thesis: b1 in Z
hence x in Z by A4, TREES_1:def_6; ::_thesis: verum
end;
end;
end;
hence Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by TARSKI:1; ::_thesis: verum
end;
Lm2: for f being Function st dom f is finite holds
f is finite
proof
let f be Function; ::_thesis: ( dom f is finite implies f is finite )
assume A1: dom f is finite ; ::_thesis: f is finite
then rng f is finite by FINSET_1:8;
then [:(dom f),(rng f):] is finite by A1;
hence f is finite by FINSET_1:1, RELAT_1:7; ::_thesis: verum
end;
theorem Th23: :: MODAL_1:23
for D being non empty set
for Z being finite DecoratedTree of D
for z being Element of dom Z st succ (Root (dom Z)) = {z} holds
Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))
proof
let D be non empty set ; ::_thesis: for Z being finite DecoratedTree of D
for z being Element of dom Z st succ (Root (dom Z)) = {z} holds
Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))
set e = elementary_tree 1;
let Z be finite DecoratedTree of D; ::_thesis: for z being Element of dom Z st succ (Root (dom Z)) = {z} holds
Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))
let z be Element of dom Z; ::_thesis: ( succ (Root (dom Z)) = {z} implies Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) )
set E = (elementary_tree 1) --> (Root Z);
A1: dom ((elementary_tree 1) --> (Root Z)) = elementary_tree 1 by FUNCOP_1:13;
A2: dom (Z | z) = (dom Z) | z by TREES_2:def_10;
A3: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
then A4: <*0*> in dom ((elementary_tree 1) --> (Root Z)) by FUNCOP_1:13;
assume A5: succ (Root (dom Z)) = {z} ; ::_thesis: Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))
then card (succ (Root (dom Z))) = 1 by CARD_1:30;
then branchdeg (Root (dom Z)) = 1 by TREES_2:def_12;
then {z} = {<*0*>} by A5, Th18;
then z in {<*0*>} by TARSKI:def_1;
then A6: z = <*0*> by TARSKI:def_1;
A7: for s being FinSequence of NAT st s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) holds
(((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s
proof
let s be FinSequence of NAT ; ::_thesis: ( s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) implies (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s )
assume A8: s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s
A9: dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = (dom ((elementary_tree 1) --> (Root Z))) with-replacement (<*0*>,(dom (Z | z))) by A4, TREES_2:def_11;
then A10: ( ( not <*0*> is_a_prefix_of s & (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = ((elementary_tree 1) --> (Root Z)) . s ) or ex w being FinSequence of NAT st
( w in dom (Z | z) & s = <*0*> ^ w & (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = (Z | z) . w ) ) by A4, A8, TREES_2:def_11;
now__::_thesis:_(((elementary_tree_1)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_z)))_._s_=_Z_._s
percases ( ( s in dom ((elementary_tree 1) --> (Root Z)) & not <*0*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in dom (Z | z) & s = <*0*> ^ w ) ) by A4, A9, A8, TREES_1:def_9;
supposeA11: ( s in dom ((elementary_tree 1) --> (Root Z)) & not <*0*> is_a_proper_prefix_of s ) ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s
now__::_thesis:_(((elementary_tree_1)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_z)))_._s_=_Z_._s
percases ( s = {} or s = <*0*> ) by A11, TARSKI:def_2, TREES_1:51;
supposeA12: s = {} ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s
then s in elementary_tree 1 by TREES_1:22;
then A13: ((elementary_tree 1) --> (Root Z)) . s = Z . s by A12, FUNCOP_1:7;
for w being FinSequence of NAT holds
( not w in dom (Z | z) or not s = <*0*> ^ w or not (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = (Z | z) . w ) by A12;
hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A4, A9, A8, A13, TREES_2:def_11; ::_thesis: verum
end;
suppose s = <*0*> ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s
hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A6, A2, A10, TREES_2:def_10; ::_thesis: verum
end;
end;
end;
hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s ; ::_thesis: verum
end;
suppose ex w being FinSequence of NAT st
( w in dom (Z | z) & s = <*0*> ^ w ) ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s
hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A6, A2, A10, TREES_1:1, TREES_2:def_10; ::_thesis: verum
end;
end;
end;
hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s ; ::_thesis: verum
end;
dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = (elementary_tree 1) with-replacement (<*0*>,((dom Z) | z)) by A3, A1, A2, TREES_2:def_11;
then dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = dom Z by A5, Th22;
hence Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) by A7, TREES_2:31; ::_thesis: verum
end;
theorem Th24: :: MODAL_1:24
for Z being Tree
for x1, x2 being 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; ::_thesis: for x1, x2 being 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))
let x1, x2 be Element of Z; ::_thesis: ( x1 = <*0*> & x2 = <*1*> & succ (Root Z) = {x1,x2} implies Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) )
assume that
A1: x1 = <*0*> and
A2: x2 = <*1*> and
A3: succ (Root Z) = {x1,x2} ; ::_thesis: Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))
set T1 = (elementary_tree 2) with-replacement (<*0*>,(Z | x1));
A4: <*0*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53;
A5: now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_
(_(_not_s_in_Z_or_(_s_in_(elementary_tree_2)_with-replacement_(<*0*>,(Z_|_x1))_&_not_<*1*>_is_a_proper_prefix_of_s_)_or_ex_w_being_FinSequence_of_NAT_st_
(_w_in_Z_|_x2_&_s_=_<*1*>_^_w_)_)_&_(_(_(_s_in_(elementary_tree_2)_with-replacement_(<*0*>,(Z_|_x1))_&_not_<*1*>_is_a_proper_prefix_of_s_)_or_ex_w_being_FinSequence_of_NAT_st_
(_w_in_Z_|_x2_&_s_=_<*1*>_^_w_)_)_implies_s_in_Z_)_)
let s be FinSequence of NAT ; ::_thesis: ( ( not s in Z or ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) & ( ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z ) )
thus ( not s in Z or ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ::_thesis: ( ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z )
proof
assume A6: s in Z ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by TREES_1:12, TREES_1:15, TREES_1:22; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
then consider w being 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__::_thesis:_(_(_s_in_(elementary_tree_2)_with-replacement_(<*0*>,(Z_|_x1))_&_not_<*1*>_is_a_proper_prefix_of_s_)_or_ex_w_being_FinSequence_of_NAT_st_
(_w_in_Z_|_x2_&_s_=_<*1*>_^_w_)_)
percases ( <*n*> = <*0*> or <*n*> = <*1*> ) by A1, A2, A3, A9, TARSKI:def_2;
supposeA10: <*n*> = <*0*> ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
then w in Z | x1 by A1, A6, A7, TREES_1:def_6;
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A4, A7, A10, Th3, TREES_1:def_9; ::_thesis: verum
end;
supposeA11: <*n*> = <*1*> ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) )
then w in Z | x2 by A2, A6, A7, TREES_1:def_6;
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A7, A11; ::_thesis: verum
end;
end;
end;
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ; ::_thesis: verum
end;
end;
end;
assume A12: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ; ::_thesis: s in Z
now__::_thesis:_s_in_Z
percases ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A12;
supposeA13: ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) ; ::_thesis: s in Z
now__::_thesis:_s_in_Z
percases ( ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x1 & s = <*0*> ^ w ) ) by A4, A13, TREES_1:def_9;
suppose ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) ; ::_thesis: s in Z
then ( s = {} or s = <*0*> or s = <*1*> ) by ENUMSET1:def_1, TREES_1:53;
hence s in Z by A1, A2, A3; ::_thesis: verum
end;
suppose ex w being FinSequence of NAT st
( w in Z | x1 & s = <*0*> ^ w ) ; ::_thesis: s in Z
hence s in Z by A1, TREES_1:def_6; ::_thesis: verum
end;
end;
end;
hence s in Z ; ::_thesis: verum
end;
suppose ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ; ::_thesis: s in Z
hence s in Z by A2, TREES_1:def_6; ::_thesis: verum
end;
end;
end;
hence s in Z ; ::_thesis: verum
end;
A14: now__::_thesis:_not_<*0*>_is_a_proper_prefix_of_<*1*>
assume <*0*> is_a_proper_prefix_of <*1*> ; ::_thesis: contradiction
then <*0*> is_a_prefix_of <*1*> by XBOOLE_0:def_8;
hence contradiction by TREES_1:3; ::_thesis: verum
end;
<*1*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53;
then <*1*> in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) by A4, A14, TREES_1:def_9;
hence Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) by A5, TREES_1:def_9; ::_thesis: verum
end;
theorem Th25: :: MODAL_1:25
for D being non empty set
for Z being DecoratedTree of D
for 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
let D be non empty set ; ::_thesis: for Z being DecoratedTree of D
for 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))
A1: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:52;
set e = elementary_tree 2;
let Z be DecoratedTree of D; ::_thesis: for 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))
let x1, x2 be Element of dom Z; ::_thesis: ( x1 = <*0*> & x2 = <*1*> & succ (Root (dom Z)) = {x1,x2} implies Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) )
assume that
A2: x1 = <*0*> and
A3: x2 = <*1*> and
A4: succ (Root (dom Z)) = {x1,x2} ; ::_thesis: Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | 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 = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2));
A7: <*0*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53;
then A8: <*0*> in dom ((elementary_tree 2) --> (Root Z)) by FUNCOP_1:13;
then A9: dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) = (dom ((elementary_tree 2) --> (Root Z))) with-replacement (<*0*>,(dom (Z | x1))) by TREES_2:def_11;
<*1*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53;
then <*1*> in dom ((elementary_tree 2) --> (Root Z)) by FUNCOP_1:13;
then A10: <*1*> in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) by A8, A9, A1, TREES_1:def_9;
then A11: dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) = (dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1)))) with-replacement (<*1*>,(dom (Z | x2))) by TREES_2:def_11;
A12: dom ((elementary_tree 2) --> (Root Z)) = elementary_tree 2 by FUNCOP_1:13;
then A13: dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) = (elementary_tree 2) with-replacement (<*0*>,((dom Z) | x1)) by A7, A6, TREES_2:def_11;
A14: for s being FinSequence of NAT st s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) holds
((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
proof
let s be FinSequence of NAT ; ::_thesis: ( s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) implies ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s )
assume A15: s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
then A16: ( ( not <*1*> is_a_prefix_of s & ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s ) or ex u being FinSequence of NAT st
( u in dom (Z | x2) & s = <*1*> ^ u & ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (Z | x2) . u ) ) by A10, A11, TREES_2:def_11;
now__::_thesis:_((((elementary_tree_2)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_x1)))_with-replacement_(<*1*>,(Z_|_x2)))_._s_=_Z_._s
percases ( ( s in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in dom (Z | x2) & s = <*1*> ^ w ) ) by A10, A11, A15, TREES_1:def_9;
supposeA17: ( s in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) & not <*1*> is_a_proper_prefix_of s ) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
then A18: ( ( not <*0*> is_a_prefix_of s & (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s = ((elementary_tree 2) --> (Root Z)) . s ) or ex u being FinSequence of NAT st
( u in dom (Z | x1) & s = <*0*> ^ u & (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s = (Z | x1) . u ) ) by A8, A9, TREES_2:def_11;
now__::_thesis:_((((elementary_tree_2)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_x1)))_with-replacement_(<*1*>,(Z_|_x2)))_._s_=_Z_._s
percases ( ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in (dom Z) | x1 & s = <*0*> ^ w ) ) by A7, A13, A17, TREES_1:def_9;
supposeA19: ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
now__::_thesis:_((((elementary_tree_2)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_x1)))_with-replacement_(<*1*>,(Z_|_x2)))_._s_=_Z_._s
percases ( s = {} or s = <*0*> or s = <*1*> ) by A19, ENUMSET1:def_1, TREES_1:53;
supposeA20: s = {} ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
then ( ( for u being FinSequence of NAT holds
( not u in dom (Z | x2) or not s = <*1*> ^ u or not ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (Z | x2) . u ) ) & ((elementary_tree 2) --> (Root Z)) . s = Z . s ) by A19, FUNCOP_1:7;
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A10, A11, A15, A18, A20, TREES_2:def_11; ::_thesis: verum
end;
suppose s = <*0*> ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A2, A3, A6, A5, A16, A18, TREES_2:def_10; ::_thesis: verum
end;
suppose s = <*1*> ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A3, A5, A16, TREES_2:def_10; ::_thesis: verum
end;
end;
end;
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; ::_thesis: verum
end;
suppose ex w being FinSequence of NAT st
( w in (dom Z) | x1 & s = <*0*> ^ w ) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A2, A3, A6, A5, A16, A18, TREES_1:1, TREES_2:def_10; ::_thesis: verum
end;
end;
end;
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; ::_thesis: verum
end;
suppose ex w being FinSequence of NAT st
( w in dom (Z | x2) & s = <*1*> ^ w ) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A3, A5, A16, TREES_1:1, TREES_2:def_10; ::_thesis: verum
end;
end;
end;
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; ::_thesis: verum
end;
dom Z = dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) by A2, A3, A4, A12, A6, A5, A9, A11, Th24;
hence Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) by A14, TREES_2:31; ::_thesis: verum
end;
definition
func MP-variables -> set equals :: MODAL_1:def 3
[:{3},NAT:];
coherence
[:{3},NAT:] is set ;
end;
:: deftheorem defines MP-variables MODAL_1:def_3_:_
MP-variables = [:{3},NAT:];
registration
cluster MP-variables -> non empty ;
coherence
not MP-variables is empty ;
end;
definition
mode MP-variable is Element of MP-variables ;
end;
definition
func MP-conectives -> set equals :: MODAL_1:def 4
[:{0,1,2},NAT:];
coherence
[:{0,1,2},NAT:] is set ;
end;
:: deftheorem defines MP-conectives MODAL_1:def_4_:_
MP-conectives = [:{0,1,2},NAT:];
registration
cluster MP-conectives -> non empty ;
coherence
not MP-conectives is empty ;
end;
definition
mode MP-conective is Element of MP-conectives ;
end;
theorem Th26: :: MODAL_1:26
MP-conectives misses MP-variables
proof
assume not MP-conectives misses MP-variables ; ::_thesis: contradiction
then consider x being set such that
A1: x in [:{0,1,2},NAT:] and
A2: x in [:{3},NAT:] by XBOOLE_0:3;
consider x1, x2 being set 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; ::_thesis: verum
end;
definition
let T be finite Tree;
let v be Element of T;
:: original: branchdeg
redefine func branchdeg v -> Element of NAT ;
coherence
branchdeg v is Element of NAT
proof
branchdeg v = card (succ v) by TREES_2:def_12;
hence branchdeg v is Element of NAT ; ::_thesis: verum
end;
end;
definition
func MP-WFF -> DTree-set of [:NAT,NAT:] means :Def5: :: MODAL_1:def 5
( ( 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 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) );
existence
ex b1 being DTree-set of [:NAT,NAT:] st
( ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) )
proof
deffunc H1( set ) -> Element of [:NAT,NAT:] = [0,0];
set t = elementary_tree 0;
set A = [:NAT,NAT:];
defpred S1[ set ] means ( $1 is finite DecoratedTree of [:NAT,NAT:] & ( for y being finite DecoratedTree of [:NAT,NAT:] st y = $1 holds
( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or 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 set holds
( x in Y iff ( x in PFuncs ((NAT *),[:NAT,NAT:]) & S1[x] ) ) from XBOOLE_0:sch_1();
A2: for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in Y iff ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) )
proof
let x be finite DecoratedTree of [:NAT,NAT:]; ::_thesis: ( x in Y iff ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) )
thus ( x in Y implies ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) by A1; ::_thesis: ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) implies x in Y )
assume that
dom x is finite and
A3: for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: x in Y
A4: x in PFuncs ((NAT *),[:NAT,NAT:]) by Th10;
for y being finite DecoratedTree of [:NAT,NAT:] st y = x holds
( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) ) by A3;
hence x in Y by A1, A4; ::_thesis: verum
end;
consider T being DecoratedTree such that
A5: ( dom T = elementary_tree 0 & ( for p being FinSequence of NAT st p in elementary_tree 0 holds
T . p = H1(p) ) ) from TREES_2:sch_7();
rng T c= [:NAT,NAT:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng T or x in [:NAT,NAT:] )
assume x in rng T ; ::_thesis: x in [:NAT,NAT:]
then consider z being set such that
A6: z in dom T and
A7: x = T . z by FUNCT_1:def_3;
z = <*> NAT by A5, A6, TARSKI:def_1, TREES_1:29;
then reconsider z = z as FinSequence of NAT ;
T . z = [0,0] by A5, A6;
hence x in [:NAT,NAT:] by A7; ::_thesis: verum
end;
then reconsider T = T as finite DecoratedTree of [:NAT,NAT:] by A5, Lm2, RELAT_1:def_19;
A8: for y being finite DecoratedTree of [:NAT,NAT:] st y = T holds
( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) )
proof
let y be finite DecoratedTree of [:NAT,NAT:]; ::_thesis: ( y = T implies ( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) ) )
assume A9: y = T ; ::_thesis: ( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) )
thus dom y is finite ; ::_thesis: for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) )
let v be Element of dom y; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) )
A10: succ v = {}
proof
set x = the Element of succ v;
assume not succ v = {} ; ::_thesis: contradiction
then A11: the Element of succ v in succ v ;
succ v = { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in dom y } by TREES_2:def_5;
then ex n being Element of NAT st
( the Element of succ v = v ^ <*n*> & v ^ <*n*> in dom y ) by A11;
hence contradiction by A5, A9, TARSKI:def_1, TREES_1:29; ::_thesis: verum
end;
hence branchdeg v <= 2 by CARD_1:27, TREES_2:def_12; ::_thesis: ( ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) )
thus ( ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) by A5, A9, A10, CARD_1:27, TREES_2:def_12; ::_thesis: verum
end;
T in PFuncs ((NAT *),[:NAT,NAT:]) by Th10;
then reconsider Y = Y as non empty set by A1, A8;
for x being set st x in Y holds
x is DecoratedTree of [:NAT,NAT:] by A1;
then reconsider Y = Y as DTree-set of [:NAT,NAT:] by TREES_3:def_6;
take Y ; ::_thesis: ( ( for x being DecoratedTree of [:NAT,NAT:] st x in Y holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in Y iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) )
thus ( ( for x being DecoratedTree of [:NAT,NAT:] st x in Y holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in Y iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being DTree-set of [:NAT,NAT:] st ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) & ( for x being DecoratedTree of [:NAT,NAT:] st x in b2 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b2 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) holds
b1 = b2
proof
let D1, D2 be DTree-set of [:NAT,NAT:]; ::_thesis: ( ( for x being DecoratedTree of [:NAT,NAT:] st x in D1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in D1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) & ( for x being DecoratedTree of [:NAT,NAT:] st x in D2 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in D2 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) implies D1 = D2 )
assume 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 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ; ::_thesis: D1 = D2
thus D1 c= D2 :: according to XBOOLE_0:def_10 ::_thesis: D2 c= D1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in D2 )
assume A16: x in D1 ; ::_thesis: x in D2
reconsider y = x as finite DecoratedTree of [:NAT,NAT:] by A12, A16;
for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) by A13, A16;
hence x in D2 by A15; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in D1 )
assume A17: x in D2 ; ::_thesis: x in D1
reconsider y = x as finite DecoratedTree of [:NAT,NAT:] by A14, A17;
for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) by A15, A17;
hence x in D1 by A13; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines MP-WFF MODAL_1:def_5_:_
for b1 being DTree-set of [:NAT,NAT:] holds
( b1 = MP-WFF iff ( ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) );
definition
mode MP-wff is Element of MP-WFF ;
end;
registration
cluster -> finite for Element of MP-WFF ;
coherence
for b1 being MP-wff holds b1 is finite by Def5;
end;
definition
let A be MP-wff;
let a be Element of dom A;
:: original: |
redefine funcA | a -> MP-wff;
coherence
A | a is MP-wff
proof
set x = A | a;
A1: dom (A | a) = (dom A) | a by TREES_2:def_10;
then reconsider db = dom (A | a) as finite Tree ;
reconsider x = A | a as finite DecoratedTree of [:NAT,NAT:] by A1, Lm2;
now__::_thesis:_(_db_is_finite_&_(_for_v_being_Element_of_db_holds_
(_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_)_)_)
thus db is finite ; ::_thesis: for v being Element of db holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
let v be Element of db; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
set da = dom A;
reconsider v9 = v as Element of (dom A) | a by TREES_2:def_10;
v in db ;
then A2: v in (dom A) | a by TREES_2:def_10;
then reconsider w = a ^ v as Element of dom A by TREES_1:def_6;
( succ v9, succ w are_equipotent & succ v9 = succ v ) by Th16, TREES_2:def_10;
then card (succ v) = card (succ w) by CARD_1:5;
then branchdeg v = card (succ w) by TREES_2:def_12;
then A3: branchdeg v = branchdeg w by TREES_2:def_12;
hence branchdeg v <= 2 by Def5; ::_thesis: ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
thus ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) ::_thesis: ( ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
proof
assume A4: branchdeg v = 0 ; ::_thesis: ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] )
percases ( A . w = [0,0] or ex k being Element of NAT st A . w = [3,k] ) by A3, A4, Def5;
suppose A . w = [0,0] ; ::_thesis: ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] )
hence ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) by A2, TREES_2:def_10; ::_thesis: verum
end;
suppose ex k being Element of NAT st A . w = [3,k] ; ::_thesis: ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] )
then consider k being Element of NAT such that
A5: A . w = [3,k] ;
now__::_thesis:_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]
take k = k; ::_thesis: x . v = [3,k]
thus x . v = [3,k] by A2, A5, TREES_2:def_10; ::_thesis: verum
end;
hence ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) ; ::_thesis: verum
end;
end;
end;
thus ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) ::_thesis: ( branchdeg v = 2 implies x . v = [2,0] )
proof
assume A6: branchdeg v = 1 ; ::_thesis: ( x . v = [1,0] or x . v = [1,1] )
percases ( A . w = [1,0] or A . w = [1,1] ) by A3, A6, Def5;
suppose A . w = [1,0] ; ::_thesis: ( x . v = [1,0] or x . v = [1,1] )
hence ( x . v = [1,0] or x . v = [1,1] ) by A2, TREES_2:def_10; ::_thesis: verum
end;
suppose A . w = [1,1] ; ::_thesis: ( x . v = [1,0] or x . v = [1,1] )
hence ( x . v = [1,0] or x . v = [1,1] ) by A2, TREES_2:def_10; ::_thesis: verum
end;
end;
end;
thus ( branchdeg v = 2 implies x . v = [2,0] ) ::_thesis: verum
proof
assume branchdeg v = 2 ; ::_thesis: x . v = [2,0]
then A . w = [2,0] by A3, Def5;
hence x . v = [2,0] by A2, TREES_2:def_10; ::_thesis: verum
end;
end;
hence A | a is MP-wff by Def5; ::_thesis: verum
end;
end;
definition
let a be Element of MP-conectives ;
func the_arity_of a -> Element of NAT equals :: MODAL_1:def 6
a `1 ;
coherence
a `1 is Element of NAT
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 a `1 is Element of NAT by A1, MCART_1:7; ::_thesis: verum
end;
end;
:: deftheorem defines the_arity_of MODAL_1:def_6_:_
for a being Element of MP-conectives holds the_arity_of a = a `1 ;
definition
let D be non empty set ;
let T, T1 be DecoratedTree of D;
let p be FinSequence of NAT ;
assume A1: p in dom T ;
func @ (T,p,T1) -> DecoratedTree of D equals :Def7: :: MODAL_1:def 7
T with-replacement (p,T1);
coherence
T with-replacement (p,T1) is DecoratedTree of D
proof
set X = T with-replacement (p,T1);
rng (T with-replacement (p,T1)) c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (T with-replacement (p,T1)) or x in D )
assume x in rng (T with-replacement (p,T1)) ; ::_thesis: x in D
then consider z being set such that
A2: z in dom (T with-replacement (p,T1)) and
A3: x = (T with-replacement (p,T1)) . z by FUNCT_1:def_3;
reconsider z = z as FinSequence of NAT by A2, TREES_1:19;
A4: dom (T with-replacement (p,T1)) = (dom T) with-replacement (p,(dom T1)) by A1, TREES_2:def_11;
now__::_thesis:_x_in_D
percases ( ( not p is_a_prefix_of z & (T with-replacement (p,T1)) . z = T . z ) or ex s being FinSequence of NAT st
( s in dom T1 & z = p ^ s & (T with-replacement (p,T1)) . z = T1 . s ) ) by A1, A2, A4, TREES_2:def_11;
supposeA5: ( not p is_a_prefix_of z & (T with-replacement (p,T1)) . z = T . z ) ; ::_thesis: x in D
then for s being FinSequence of NAT holds
( not s in dom T1 or not z = p ^ s ) by TREES_1:1;
then reconsider z = z as Element of dom T by A1, A2, A4, TREES_1:def_9;
T . z is Element of D ;
hence x in D by A3, A5; ::_thesis: verum
end;
suppose ex s being FinSequence of NAT st
( s in dom T1 & z = p ^ s & (T with-replacement (p,T1)) . z = T1 . s ) ; ::_thesis: x in D
then consider s being FinSequence of NAT such that
A6: s in dom T1 and
z = p ^ s and
A7: (T with-replacement (p,T1)) . z = T1 . s ;
reconsider s = s as Element of dom T1 by A6;
T1 . s is Element of D ;
hence x in D by A3, A7; ::_thesis: verum
end;
end;
end;
hence x in D ; ::_thesis: verum
end;
hence T with-replacement (p,T1) is DecoratedTree of D by RELAT_1:def_19; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines @ MODAL_1:def_7_:_
for D being non empty set
for T, T1 being DecoratedTree of D
for p being FinSequence of NAT st p in dom T holds
@ (T,p,T1) = T with-replacement (p,T1);
theorem Th27: :: MODAL_1:27
for A being MP-wff holds ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff
proof
let A be MP-wff; ::_thesis: ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff
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) = ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) by Def7;
dom (((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(dom A)) by A1, TREES_2:def_11;
then dom (((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A)) = (elementary_tree 1) with-replacement (d,(dom A)) by FUNCOP_1:13;
then reconsider x = ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) 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 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
now__::_thesis:_(_branchdeg_v_<=_2_&_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_)
percases ( ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,0]) . v ) or ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & x . v = A . s ) ) by A1, A3, TREES_2:def_11;
supposeA4: ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,0]) . v ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A5: dom ((elementary_tree 1) --> [1,0]) = {{},<*0*>} by FUNCOP_1:13, TREES_1:51;
A6: for s being FinSequence of NAT holds
( not s in dom A or not v = <*0*> ^ s ) by A4, TREES_1:1;
then A7: v in dom ((elementary_tree 1) --> [1,0]) by A1, A3, TREES_1:def_9;
then A8: v = {} by A4, A5, TARSKI:def_2;
reconsider v9 = v as Element of dom ((elementary_tree 1) --> [1,0]) by A1, A3, A6, TREES_1:def_9;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_succ_v9_implies_x_in_{<*0*>}_)_&_(_x_in_{<*0*>}_implies_x_in_succ_v9_)_)
let x be set ; ::_thesis: ( ( x in succ v9 implies x in {<*0*>} ) & ( x in {<*0*>} implies x in succ v9 ) )
thus ( x in succ v9 implies x in {<*0*>} ) ::_thesis: ( x in {<*0*>} implies x in succ v9 )
proof
assume x in succ v9 ; ::_thesis: x in {<*0*>}
then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,0]) } by TREES_2:def_5;
then consider n being Element of NAT such that
A9: x = v9 ^ <*n*> and
A10: v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,0]) ;
<*n*> in dom ((elementary_tree 1) --> [1,0]) 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 x in {<*0*>} by A11, TARSKI:def_1; ::_thesis: verum
end;
assume x in {<*0*>} ; ::_thesis: x in succ v9
then A12: x = <*0*> by TARSKI:def_1;
then A13: x = v9 ^ <*0*> by A8, FINSEQ_1:34;
then v9 ^ <*0*> in dom ((elementary_tree 1) --> [1,0]) by A5, A12, TARSKI:def_2;
then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,0]) } by A13;
hence x in succ v9 by TREES_2:def_5; ::_thesis: verum
end;
then A14: succ v9 = {<*0*>} by TARSKI:1;
succ v = succ v9 by A1, A3, A8, Lm1, Th13;
then 1 = card (succ v) by A14, CARD_1:30;
then A15: branchdeg v = 1 by TREES_2:def_12;
hence branchdeg v <= 2 ; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
v in elementary_tree 1 by A7;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A4, A15, FUNCOP_1:7; ::_thesis: verum
end;
suppose ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & x . v = A . s ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
then consider s being FinSequence of NAT such that
A16: s in dom A and
A17: v = <*0*> ^ s and
A18: x . v = A . s ;
reconsider s = 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A21: ( not branchdeg s = 1 or A . s = [1,0] or A . s = [1,1] ) by Def5;
A22: ( branchdeg s = 2 implies A . s = [2,0] ) by Def5;
( not branchdeg s = 0 or A . s = [0,0] or ex m being Element of NAT st A . s = [3,m] ) by Def5;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A18, A20, A21, A22, A19, TREES_2:def_12; ::_thesis: verum
end;
end;
end;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: verum
end;
hence ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff by Def5; ::_thesis: verum
end;
theorem Th28: :: MODAL_1:28
for A being MP-wff holds ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff
proof
let A be MP-wff; ::_thesis: ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff
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 (((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11;
then A2: dom (((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A)) = (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 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
now__::_thesis:_(_branchdeg_v_<=_2_&_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_)
percases ( ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,1]) . v ) or ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & x . v = A . s ) ) by A1, A3, TREES_2:def_11;
supposeA4: ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,1]) . v ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A5: dom ((elementary_tree 1) --> [1,1]) = {{},<*0*>} by FUNCOP_1:13, TREES_1:51;
A6: for s being FinSequence of NAT holds
( not s in dom A or not v = <*0*> ^ s ) by A4, TREES_1:1;
then A7: v in dom ((elementary_tree 1) --> [1,1]) by A1, A3, TREES_1:def_9;
then A8: v = {} by A4, A5, TARSKI:def_2;
reconsider v9 = v as Element of dom ((elementary_tree 1) --> [1,1]) by A1, A3, A6, TREES_1:def_9;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_succ_v9_implies_x_in_{<*0*>}_)_&_(_x_in_{<*0*>}_implies_x_in_succ_v9_)_)
let x be set ; ::_thesis: ( ( x in succ v9 implies x in {<*0*>} ) & ( x in {<*0*>} implies x in succ v9 ) )
thus ( x in succ v9 implies x in {<*0*>} ) ::_thesis: ( x in {<*0*>} implies x in succ v9 )
proof
assume x in succ v9 ; ::_thesis: x in {<*0*>}
then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) } by TREES_2:def_5;
then consider n being Element of NAT such that
A9: x = v9 ^ <*n*> and
A10: v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) ;
<*n*> in dom ((elementary_tree 1) --> [1,1]) 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 x in {<*0*>} by A11, TARSKI:def_1; ::_thesis: verum
end;
assume x in {<*0*>} ; ::_thesis: x in succ v9
then A12: x = <*0*> by TARSKI:def_1;
then A13: x = v9 ^ <*0*> by A8, FINSEQ_1:34;
then v9 ^ <*0*> in dom ((elementary_tree 1) --> [1,1]) by A5, A12, TARSKI:def_2;
then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) } by A13;
hence x in succ v9 by TREES_2:def_5; ::_thesis: verum
end;
then A14: succ v9 = {<*0*>} by TARSKI:1;
succ v = succ v9 by A1, A3, A8, Lm1, Th13;
then 1 = card (succ v) by A14, CARD_1:30;
then A15: branchdeg v = 1 by TREES_2:def_12;
hence branchdeg v <= 2 ; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
v in elementary_tree 1 by A7;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A4, A15, FUNCOP_1:7; ::_thesis: verum
end;
suppose ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & x . v = A . s ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
then consider s being FinSequence of NAT such that
A16: s in dom A and
A17: v = <*0*> ^ s and
A18: x . v = A . s ;
reconsider s = 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A21: ( not branchdeg s = 1 or A . s = [1,0] or A . s = [1,1] ) by Def5;
A22: ( branchdeg s = 2 implies A . s = [2,0] ) by Def5;
( not branchdeg s = 0 or A . s = [0,0] or ex m being Element of NAT st A . s = [3,m] ) by Def5;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A18, A20, A21, A22, A19, TREES_2:def_12; ::_thesis: verum
end;
end;
end;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: verum
end;
hence ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff by Def5; ::_thesis: verum
end;
theorem Th29: :: MODAL_1:29
for A, B being MP-wff holds (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff
proof
let A, B be MP-wff; ::_thesis: (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff
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 = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B);
A1: not <*0*> is_a_proper_prefix_of <*1*>
proof
assume <*0*> is_a_proper_prefix_of <*1*> ; ::_thesis: contradiction
then <*0*> is_a_prefix_of <*1*> by XBOOLE_0:def_8;
hence contradiction by TREES_1:3; ::_thesis: verum
end;
reconsider db = dom B as finite Tree ;
reconsider da = dom A as finite Tree ;
<*0*> in elementary_tree 2 by TREES_1:28;
then A2: <*0*> in dom ((elementary_tree 2) --> [2,0]) by FUNCOP_1:13;
then @ (((elementary_tree 2) --> [2,0]),<*0*>,A) = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) by Def7;
then reconsider y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) 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 ((((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B)) = dy with-replacement (d1,db) & @ (y,<*1*>,B) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) ) by A5, Def7, TREES_2:def_11;
then reconsider x = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) 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 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
now__::_thesis:_(_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_)
percases ( ( not <*1*> is_a_prefix_of v & x . v = y . v ) or ex s being FinSequence of NAT st
( s in dom B & v = <*1*> ^ s & x . v = B . s ) ) by A5, A6, TREES_2:def_11;
supposeA7: ( not <*1*> is_a_prefix_of v & x . v = y . v ) ; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
then A8: for s being FinSequence of NAT holds
( not s in dom B or not v = <*1*> ^ s ) by TREES_1:1;
then A9: v in (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by A3, A5, A6, TREES_1:def_9;
now__::_thesis:_(_branchdeg_v_<=_2_&_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_)
percases ( ( not <*0*> is_a_prefix_of v & y . v = ((elementary_tree 2) --> [2,0]) . v ) or ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & y . v = A . s ) ) by A2, A9, TREES_2:def_11;
supposeA10: ( not <*0*> is_a_prefix_of v & y . v = ((elementary_tree 2) --> [2,0]) . v ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A11: dom ((elementary_tree 2) --> [2,0]) = {{},<*0*>,<*1*>} by FUNCOP_1:13, TREES_1:53;
A12: for s being FinSequence of NAT holds
( not s in dom A or not v = <*0*> ^ s ) by A10, TREES_1:1;
then A13: v in dom ((elementary_tree 2) --> [2,0]) by A2, A9, TREES_1:def_9;
then A14: v = {} by A7, A10, A11, ENUMSET1:def_1;
reconsider v9 = v as Element of dom ((elementary_tree 2) --> [2,0]) by A2, A9, A12, TREES_1:def_9;
A15: succ v = succ v9
proof
reconsider v99 = v as Element of dom y by A5, A6, A8, TREES_1:def_9;
succ v99 = succ v9 by A2, A3, A14, Lm1, Th13;
hence succ v = succ v9 by A5, A6, A14, Lm1, Th13; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_succ_v9_implies_x_in_{<*0*>,<*1*>}_)_&_(_x_in_{<*0*>,<*1*>}_implies_x_in_succ_v9_)_)
let x be set ; ::_thesis: ( ( x in succ v9 implies x in {<*0*>,<*1*>} ) & ( x in {<*0*>,<*1*>} implies x in succ v9 ) )
thus ( x in succ v9 implies x in {<*0*>,<*1*>} ) ::_thesis: ( x in {<*0*>,<*1*>} implies x in succ v9 )
proof
assume x in succ v9 ; ::_thesis: x in {<*0*>,<*1*>}
then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) } by TREES_2:def_5;
then consider n being Element of NAT such that
A16: x = v9 ^ <*n*> and
A17: v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) ;
<*n*> in dom ((elementary_tree 2) --> [2,0]) 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 x in {<*0*>,<*1*>} by A18, TARSKI:def_2; ::_thesis: verum
end;
assume x in {<*0*>,<*1*>} ; ::_thesis: x in succ v9
then A19: ( x = <*0*> or x = <*1*> ) by TARSKI:def_2;
now__::_thesis:_x_in_succ_v9
percases ( x = v9 ^ <*0*> or x = v9 ^ <*1*> ) by A14, A19, FINSEQ_1:34;
supposeA20: x = v9 ^ <*0*> ; ::_thesis: x in succ v9
then v9 ^ <*0*> in dom ((elementary_tree 2) --> [2,0]) by A11, A19, ENUMSET1:def_1;
then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) } by A20;
hence x in succ v9 by TREES_2:def_5; ::_thesis: verum
end;
supposeA21: x = v9 ^ <*1*> ; ::_thesis: x in succ v9
then v9 ^ <*1*> in dom ((elementary_tree 2) --> [2,0]) by A11, A19, ENUMSET1:def_1;
then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) } by A21;
hence x in succ v9 by TREES_2:def_5; ::_thesis: verum
end;
end;
end;
hence x in succ v9 ; ::_thesis: verum
end;
then A22: succ v9 = {<*0*>,<*1*>} by TARSKI:1;
<*0*> <> <*1*> by TREES_1:3;
then A23: 2 = card (succ v) by A22, A15, CARD_2:57;
hence branchdeg v <= 2 by TREES_2:def_12; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
v in elementary_tree 2 by A13;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A7, A10, A23, FUNCOP_1:7, TREES_2:def_12; ::_thesis: verum
end;
suppose ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & y . v = A . s ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
then consider s being FinSequence of NAT such that
A24: s in dom A and
A25: v = <*0*> ^ s and
A26: y . v = A . s ;
reconsider s = 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 succ v, succ s are_equipotent by A5, A6, A25, Th1, Th14; ::_thesis: verum
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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A29: ( not branchdeg s = 1 or A . s = [1,0] or A . s = [1,1] ) by Def5;
A30: ( branchdeg s = 2 implies A . s = [2,0] ) by Def5;
( not branchdeg s = 0 or A . s = [0,0] or ex m being Element of NAT st A . s = [3,m] ) by Def5;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A7, A26, A28, A29, A30, A27, TREES_2:def_12; ::_thesis: verum
end;
end;
end;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: verum
end;
suppose ex s being FinSequence of NAT st
( s in dom B & v = <*1*> ^ s & x . v = B . s ) ; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
then consider s being FinSequence of NAT such that
A31: s in dom B and
A32: v = <*1*> ^ s and
A33: x . v = B . s ;
reconsider s = 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: ( not branchdeg s = 1 or B . s = [1,0] or B . s = [1,1] ) by Def5;
A37: ( not branchdeg s = 0 or B . s = [0,0] or ex m being Element of NAT st B . s = [3,m] ) by Def5;
branchdeg s <= 2 by Def5;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A33, A37, A36, A35, A34, TREES_2:def_12; ::_thesis: verum
end;
end;
end;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: verum
end;
hence (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff by Def5; ::_thesis: verum
end;
definition
let A be MP-wff;
func 'not' A -> MP-wff equals :: MODAL_1:def 8
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A);
coherence
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff by Th27;
func (#) A -> MP-wff equals :: MODAL_1:def 9
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A);
coherence
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff by Th28;
let B be MP-wff;
funcA '&' B -> MP-wff equals :: MODAL_1:def 10
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B);
coherence
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff by Th29;
end;
:: deftheorem defines 'not' MODAL_1:def_8_:_
for A being MP-wff holds 'not' A = ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A);
:: deftheorem defines (#) MODAL_1:def_9_:_
for A being MP-wff holds (#) A = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A);
:: deftheorem defines '&' MODAL_1:def_10_:_
for A, B being MP-wff holds A '&' B = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B);
definition
let A be MP-wff;
func ? A -> MP-wff equals :: MODAL_1:def 11
'not' ((#) ('not' A));
correctness
coherence
'not' ((#) ('not' A)) is MP-wff;
;
let B be MP-wff;
funcA 'or' B -> MP-wff equals :: MODAL_1:def 12
'not' (('not' A) '&' ('not' B));
correctness
coherence
'not' (('not' A) '&' ('not' B)) is MP-wff;
;
funcA => B -> MP-wff equals :: MODAL_1:def 13
'not' (A '&' ('not' B));
correctness
coherence
'not' (A '&' ('not' B)) is MP-wff;
;
end;
:: deftheorem defines ? MODAL_1:def_11_:_
for A being MP-wff holds ? A = 'not' ((#) ('not' A));
:: deftheorem defines 'or' MODAL_1:def_12_:_
for A, B being MP-wff holds A 'or' B = 'not' (('not' A) '&' ('not' B));
:: deftheorem defines => MODAL_1:def_13_:_
for A, B being MP-wff holds A => B = 'not' (A '&' ('not' B));
theorem Th30: :: MODAL_1:30
for n being Element of NAT holds (elementary_tree 0) --> [3,n] is MP-wff
proof
let n be Element of NAT ; ::_thesis: (elementary_tree 0) --> [3,n] is MP-wff
set x = (elementary_tree 0) --> [3,n];
A1: dom ((elementary_tree 0) --> [3,n]) = {{}} by FUNCOP_1:13, TREES_1:29;
reconsider x = (elementary_tree 0) --> [3,n] 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 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A3: succ v = {}
proof
set y = the Element of succ v;
assume not succ v = {} ; ::_thesis: contradiction
then the Element of succ v in succ v ;
then the Element of succ v in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in dom x } by TREES_2:def_5;
then ex m being Element of NAT st
( the Element of succ v = v ^ <*m*> & v ^ <*m*> in dom x ) ;
hence contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
hence branchdeg v <= 2 by CARD_1:27, TREES_2:def_12; ::_thesis: ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
thus ( not branchdeg v = 0 or x . v = [0,0] or ex m being Element of NAT st x . v = [3,m] ) by A2, FUNCOP_1:7; ::_thesis: ( ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
thus ( ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A3, CARD_1:27, TREES_2:def_12; ::_thesis: verum
end;
hence (elementary_tree 0) --> [3,n] is MP-wff by Def5; ::_thesis: verum
end;
theorem Th31: :: MODAL_1:31
(elementary_tree 0) --> [0,0] is MP-wff
proof
set x = (elementary_tree 0) --> [0,0];
reconsider x = (elementary_tree 0) --> [0,0] 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 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A3: succ v = {}
proof
set y = the Element of succ v;
assume not succ v = {} ; ::_thesis: contradiction
then the Element of succ v in succ v ;
then the Element of succ v in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in dom x } by TREES_2:def_5;
then ex m being Element of NAT st
( the Element of succ v = v ^ <*m*> & v ^ <*m*> in dom x ) ;
hence contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
hence branchdeg v <= 2 by CARD_1:27, TREES_2:def_12; ::_thesis: ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
thus ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A2, A3, CARD_1:27, FUNCOP_1:7, TREES_2:def_12; ::_thesis: verum
end;
hence (elementary_tree 0) --> [0,0] is MP-wff by Def5; ::_thesis: verum
end;
definition
let p be MP-variable;
func @ p -> MP-wff equals :: MODAL_1:def 14
(elementary_tree 0) --> p;
coherence
(elementary_tree 0) --> p is MP-wff
proof
consider x1, x2 being set 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 (elementary_tree 0) --> p is MP-wff by A2, Th30; ::_thesis: verum
end;
end;
:: deftheorem defines @ MODAL_1:def_14_:_
for p being MP-variable holds @ p = (elementary_tree 0) --> p;
theorem Th32: :: MODAL_1:32
for p, q being MP-variable st @ p = @ q holds
p = q
proof
let p, q be MP-variable; ::_thesis: ( @ p = @ q implies p = q )
assume A1: @ p = @ q ; ::_thesis: 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 p = q ; ::_thesis: verum
end;
Lm3: for n, m being Element of NAT holds <*0*> in dom ((elementary_tree 1) --> [n,m])
proof
let n, m be Element of NAT ; ::_thesis: <*0*> in dom ((elementary_tree 1) --> [n,m])
<*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
hence <*0*> in dom ((elementary_tree 1) --> [n,m]) by FUNCOP_1:13; ::_thesis: verum
end;
theorem Th33: :: MODAL_1:33
for A, B being MP-wff st 'not' A = 'not' B holds
A = B
proof
let A, B be MP-wff; ::_thesis: ( 'not' A = 'not' B implies A = B )
assume A1: 'not' A = 'not' B ; ::_thesis: A = B
<*0*> in dom ((elementary_tree 1) --> [1,0]) by Lm3;
hence A = B by A1, Th12; ::_thesis: verum
end;
theorem Th34: :: MODAL_1:34
for A, B being MP-wff st (#) A = (#) B holds
A = B
proof
let A, B be MP-wff; ::_thesis: ( (#) A = (#) B implies A = B )
set AA = (elementary_tree 1) --> [1,1];
assume A1: (#) A = (#) B ; ::_thesis: A = B
<*0*> in dom ((elementary_tree 1) --> [1,1]) by Lm3;
hence A = B by A1, Th12; ::_thesis: verum
end;
theorem Th35: :: MODAL_1:35
for A, B, A1, B1 being MP-wff st A '&' B = A1 '&' B1 holds
( A = A1 & B = B1 )
proof
let A, B, A1, B1 be MP-wff; ::_thesis: ( A '&' B = A1 '&' B1 implies ( A = A1 & B = B1 ) )
set e = elementary_tree 2;
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A);
set y1 = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1);
assume A1: A '&' B = A1 '&' B1 ; ::_thesis: ( A = A1 & B = B1 )
A2: <*1*> in elementary_tree 2 by TREES_1:28;
A3: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28;
then A4: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) = (dom ((elementary_tree 2) --> [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 ((elementary_tree 2) --> [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 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) by A2, A3, A4, TREES_1:def_9;
A8: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by A3, TREES_2:def_11;
then A9: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, A6, TREES_1:def_9;
then A10: dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,(dom B)) by TREES_2:def_11;
A11: dom (A1 '&' B1) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1))) with-replacement (<*1*>,(dom B1)) by A7, TREES_2:def_11;
now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_
(_(_s_in_dom_B_implies_s_in_dom_B1_)_&_(_s_in_dom_B1_implies_s_in_dom_B_)_)
let s be FinSequence of NAT ; ::_thesis: ( ( s in dom B implies s in dom B1 ) & ( s in dom B1 implies s in dom B ) )
thus ( s in dom B implies s in dom B1 ) ::_thesis: ( s in dom B1 implies s in dom B )
proof
assume s in dom B ; ::_thesis: s in dom B1
then A12: <*1*> ^ s in dom (A1 '&' B1) by A1, A9, A10, TREES_1:def_9;
now__::_thesis:_s_in_dom_B1
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: s in dom B1
hence s in dom B1 by TREES_1:22; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: s in dom B1
then <*1*> is_a_proper_prefix_of <*1*> ^ s by TREES_1:10;
then ex w being FinSequence of NAT st
( w in dom B1 & <*1*> ^ s = <*1*> ^ w ) by A7, A11, A12, TREES_1:def_9;
hence s in dom B1 by FINSEQ_1:33; ::_thesis: verum
end;
end;
end;
hence s in dom B1 ; ::_thesis: verum
end;
assume s in dom B1 ; ::_thesis: s in dom B
then A13: <*1*> ^ s in dom (A '&' B) by A1, A7, A11, TREES_1:def_9;
now__::_thesis:_s_in_dom_B
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: s in dom B
hence s in dom B by TREES_1:22; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: s in dom B
then <*1*> is_a_proper_prefix_of <*1*> ^ s by TREES_1:10;
then ex w being FinSequence of NAT 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; ::_thesis: verum
end;
end;
end;
hence s in dom B ; ::_thesis: verum
end;
then A14: dom B = dom B1 by TREES_2:def_1;
A15: for s being FinSequence of NAT st s in dom B holds
B . s = B1 . s
proof
let s be FinSequence of NAT ; ::_thesis: ( s in dom B implies B . s = B1 . s )
assume s in dom B ; ::_thesis: B . s = B1 . s
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 being FinSequence of NAT 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 being FinSequence of NAT 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 B . s = B1 . s by A1, A19, A20, FINSEQ_1:33; ::_thesis: verum
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 ((elementary_tree 2) --> [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 ((elementary_tree 2) --> [2,0])) with-replacement (<*1*>,(dom B))) with-replacement (<*0*>,(dom A1)) by A22, A2, A3, A4, A11, A14, TREES_2:8;
then A25: dom A = dom A1 by A1, A5, A23, Th11;
for s being FinSequence of NAT st s in dom A holds
A . s = A1 . s
proof
let s be FinSequence of NAT ; ::_thesis: ( s in dom A implies A . s = A1 . s )
assume A26: s in dom A ; ::_thesis: A . s = A1 . s
then A27: <*0*> ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A3, A8, TREES_1:def_9;
A28: <*0*> is_a_prefix_of <*0*> ^ s by TREES_1:1;
then A29: ex w being FinSequence of NAT st
( w in dom A & <*0*> ^ s = <*0*> ^ w & (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) . (<*0*> ^ s) = A . w ) by A3, A8, A27, TREES_2:def_11;
<*0*> ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) by A3, A4, A25, A26, TREES_1:def_9;
then A30: ex u being FinSequence of NAT st
( u in dom A1 & <*0*> ^ s = <*0*> ^ u & (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) . (<*0*> ^ s) = A1 . u ) by A3, A4, A28, TREES_2:def_11;
not <*1*> is_a_proper_prefix_of <*0*> ^ s by Th3;
then A31: <*0*> ^ s in dom (A '&' B) by A9, A10, A27, TREES_1:def_9;
now__::_thesis:_for_w_being_FinSequence_of_NAT_holds_
(_not_w_in_dom_B_or_not_<*0*>_^_s_=_<*1*>_^_w_or_not_(A_'&'_B)_._(<*0*>_^_s)_=_B_._w_)
given w being FinSequence of NAT such that w in dom B and
A32: <*0*> ^ s = <*1*> ^ w and
(A '&' B) . (<*0*> ^ s) = B . w ; ::_thesis: contradiction
<*0*> is_a_prefix_of <*1*> ^ w by A32, TREES_1:1;
hence contradiction by TREES_1:50; ::_thesis: verum
end;
then (A '&' B) . (<*0*> ^ s) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) . (<*0*> ^ s) by A9, A10, A31, TREES_2:def_11;
then A33: A . s = (A1 '&' B) . (<*0*> ^ s) by A1, A21, A29, FINSEQ_1:33;
now__::_thesis:_for_w_being_FinSequence_of_NAT_holds_
(_not_w_in_dom_B1_or_not_<*0*>_^_s_=_<*1*>_^_w_or_not_(A1_'&'_B1)_._(<*0*>_^_s)_=_B1_._w_)
given w being FinSequence of NAT such that w in dom B1 and
A34: <*0*> ^ s = <*1*> ^ w and
(A1 '&' B1) . (<*0*> ^ s) = B1 . w ; ::_thesis: contradiction
<*0*> is_a_prefix_of <*1*> ^ w by A34, TREES_1:1;
hence contradiction by TREES_1:50; ::_thesis: verum
end;
then (A1 '&' B1) . (<*0*> ^ s) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) . (<*0*> ^ s) by A1, A7, A11, A31, TREES_2:def_11;
hence A . s = A1 . s by A21, A33, A30, FINSEQ_1:33; ::_thesis: verum
end;
hence ( A = A1 & B = B1 ) by A1, A5, A14, A23, A24, A15, Th11, TREES_2:31; ::_thesis: verum
end;
definition
func VERUM -> MP-wff equals :: MODAL_1:def 15
(elementary_tree 0) --> [0,0];
coherence
(elementary_tree 0) --> [0,0] is MP-wff by Th31;
end;
:: deftheorem defines VERUM MODAL_1:def_15_:_
VERUM = (elementary_tree 0) --> [0,0];
theorem Th36: :: MODAL_1:36
for A being MP-wff holds
( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p )
proof
let A be MP-wff; ::_thesis: ( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p )
assume card (dom A) = 1 ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p )
then consider x being set such that
A1: dom A = {x} by CARD_2:42;
reconsider x = 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 succ x = {} ; ::_thesis: contradiction
then A5: the Element of succ x in succ x ;
succ x = { (x ^ <*n*>) where n is Element of NAT : x ^ <*n*> in dom A } by TREES_2:def_5;
then ex n being Element of NAT st
( the Element of succ x = x ^ <*n*> & x ^ <*n*> in dom A ) by A5;
hence contradiction by A4, TARSKI:def_1; ::_thesis: verum
end;
then A6: branchdeg x = 0 by CARD_1:27, TREES_2:def_12;
now__::_thesis:_(_A_=_VERUM_or_ex_p_being_MP-variable_st_A_=_@_p_)
percases ( A . x = [0,0] or ex n being Element of NAT st A . x = [3,n] ) by A6, Def5;
suppose A . x = [0,0] ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p )
then for z being set st z in dom A holds
A . z = [0,0] by A1, TARSKI:def_1;
hence ( A = VERUM or ex p being MP-variable st A = @ p ) by A3, FUNCOP_1:11; ::_thesis: verum
end;
suppose ex n being Element of NAT st A . x = [3,n] ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p )
then consider n being Element of NAT such that
A7: A . x = [3,n] ;
reconsider p = [3,n] as MP-variable by ZFMISC_1:105;
for z being set st z in dom A holds
A . z = [3,n] by A1, A7, TARSKI:def_1;
then A = @ p by A3, FUNCOP_1:11;
hence ( A = VERUM or ex p being MP-variable st A = @ p ) ; ::_thesis: verum
end;
end;
end;
hence ( A = VERUM or ex p being MP-variable st A = @ p ) ; ::_thesis: verum
end;
theorem Th37: :: MODAL_1:37
for A being MP-wff holds
( not card (dom A) >= 2 or ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
proof
let A be MP-wff; ::_thesis: ( not card (dom A) >= 2 or ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
set b = branchdeg (Root (dom A));
set a = Root (dom A);
assume A1: card (dom A) >= 2 ; ::_thesis: ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
A2: now__::_thesis:_not_branchdeg_(Root_(dom_A))_=_0
assume branchdeg (Root (dom A)) = 0 ; ::_thesis: contradiction
then card (dom A) = 1 by Th17;
hence contradiction by A1; ::_thesis: verum
end;
A3: branchdeg (Root (dom A)) <= 2 by Def5;
now__::_thesis:_(_(_branchdeg_(Root_(dom_A))_=_1_&_ex_B_being_MP-wff_st_
(_ex_B_being_MP-wff_st_
(_A_=_'not'_B_or_A_=_(#)_B_)_or_ex_B,_C_being_MP-wff_st_A_=_B_'&'_C_)_)_or_(_branchdeg_(Root_(dom_A))_=_2_&_ex_B,_C_being_MP-wff_st_
(_ex_B_being_MP-wff_st_
(_A_=_'not'_B_or_A_=_(#)_B_)_or_ex_B,_C_being_MP-wff_st_A_=_B_'&'_C_)_)_)
percases ( branchdeg (Root (dom A)) = 1 or branchdeg (Root (dom A)) = 2 ) by A3, A2, NAT_1:26;
caseA4: branchdeg (Root (dom A)) = 1 ; ::_thesis: ex B being MP-wff st
( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
then card (succ (Root (dom A))) = 1 by TREES_2:def_12;
then consider x being set such that
A5: succ (Root (dom A)) = {x} by CARD_2:42;
x in succ (Root (dom A)) by A5, TARSKI:def_1;
then reconsider x9 = x as Element of dom A ;
take B = A | x9; ::_thesis: ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
now__::_thesis:_(_A_=_'not'_B_or_A_=_(#)_B_)
percases ( A . (Root (dom A)) = [1,0] or A . (Root (dom A)) = [1,1] ) by A4, Def5;
suppose A . (Root (dom A)) = [1,0] ; ::_thesis: ( A = 'not' B or A = (#) B )
then Root A = [1,0] ;
hence ( A = 'not' B or A = (#) B ) by A5, Th23; ::_thesis: verum
end;
suppose A . (Root (dom A)) = [1,1] ; ::_thesis: ( A = 'not' B or A = (#) B )
then Root A = [1,1] ;
hence ( A = 'not' B or A = (#) B ) by A5, Th23; ::_thesis: verum
end;
end;
end;
hence ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: verum
end;
caseA6: branchdeg (Root (dom A)) = 2 ; ::_thesis: ex B, C being MP-wff st
( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
then A7: succ (Root (dom A)) = {<*0*>,<*1*>} by Th19;
then ( <*0*> in succ (Root (dom A)) & <*1*> in succ (Root (dom A)) ) by TARSKI:def_2;
then reconsider x = <*0*>, y = <*1*> as Element of dom A ;
take B = A | x; ::_thesis: ex C being MP-wff st
( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
take C = A | y; ::_thesis: ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
Root A = [2,0] by A6, Def5;
then A = B '&' C by A7, Th25;
hence ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: verum
end;
end;
end;
hence ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: verum
end;
theorem Th38: :: MODAL_1:38
for A being MP-wff holds card (dom A) < card (dom ('not' A))
proof
let A be MP-wff; ::_thesis: card (dom A) < card (dom ('not' A))
set e = elementary_tree 1;
<*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
then A1: <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13;
then A2: dom ('not' A) = (dom ((elementary_tree 1) --> [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__::_thesis:_for_s_being_FinSequence_of_NAT_holds_
(_(_s_in_dom_A_implies_o_^_s_in_dom_('not'_A)_)_&_(_o_^_s_in_dom_('not'_A)_implies_s_in_dom_A_)_)
let s be FinSequence of NAT ; ::_thesis: ( ( s in dom A implies o ^ s in dom ('not' A) ) & ( o ^ s in dom ('not' A) implies s in dom A ) )
thus ( s in dom A implies o ^ s in dom ('not' A) ) by A1, A2, TREES_1:def_9; ::_thesis: ( o ^ s in dom ('not' A) implies s in dom A )
assume A3: o ^ s in dom ('not' A) ; ::_thesis: s in dom A
now__::_thesis:_s_in_dom_A
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: s in dom A
hence s in dom A by TREES_1:22; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: s in dom A
then o is_a_proper_prefix_of o ^ s by TREES_1:10;
then ex w being FinSequence of NAT 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; ::_thesis: verum
end;
end;
end;
hence s in dom A ; ::_thesis: verum
end;
then A4: dom A = (dom ('not' A)) | o by TREES_1:def_6;
o <> Root (dom ('not' A)) ;
hence card (dom A) < card (dom ('not' A)) by A4, Th21; ::_thesis: verum
end;
theorem Th39: :: MODAL_1:39
for A being MP-wff holds card (dom A) < card (dom ((#) A))
proof
let A be MP-wff; ::_thesis: card (dom A) < card (dom ((#) A))
set e = elementary_tree 1;
<*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
then A1: <*0*> in dom ((elementary_tree 1) --> [1,1]) by FUNCOP_1:13;
then A2: dom ((#) A) = (dom ((elementary_tree 1) --> [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__::_thesis:_for_s_being_FinSequence_of_NAT_holds_
(_(_s_in_dom_A_implies_o_^_s_in_dom_((#)_A)_)_&_(_o_^_s_in_dom_((#)_A)_implies_s_in_dom_A_)_)
let s be FinSequence of NAT ; ::_thesis: ( ( s in dom A implies o ^ s in dom ((#) A) ) & ( o ^ s in dom ((#) A) implies s in dom A ) )
thus ( s in dom A implies o ^ s in dom ((#) A) ) by A1, A2, TREES_1:def_9; ::_thesis: ( o ^ s in dom ((#) A) implies s in dom A )
assume A3: o ^ s in dom ((#) A) ; ::_thesis: s in dom A
now__::_thesis:_s_in_dom_A
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: s in dom A
hence s in dom A by TREES_1:22; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: s in dom A
then o is_a_proper_prefix_of o ^ s by TREES_1:10;
then ex w being FinSequence of NAT 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; ::_thesis: verum
end;
end;
end;
hence s in dom A ; ::_thesis: verum
end;
then A4: dom A = (dom ((#) A)) | o by TREES_1:def_6;
o <> Root (dom ((#) A)) ;
hence card (dom A) < card (dom ((#) A)) by A4, Th21; ::_thesis: verum
end;
theorem Th40: :: MODAL_1:40
for A, B being MP-wff holds
( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) )
proof
let A, B be MP-wff; ::_thesis: ( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) )
set e = elementary_tree 2;
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A);
A1: not <*1*> is_a_proper_prefix_of <*0*> by TREES_1:52;
A2: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28;
then A3: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11;
( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52;
then A4: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, TREES_1:def_9;
then A5: dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) 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 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) 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__::_thesis:_for_s_being_FinSequence_of_NAT_holds_
(_(_s_in_dom_A_implies_o_^_s_in_dom_(A_'&'_B)_)_&_(_o_^_s_in_dom_(A_'&'_B)_implies_s_in_dom_A_)_)
let s be FinSequence of NAT ; ::_thesis: ( ( s in dom A implies o ^ s in dom (A '&' B) ) & ( o ^ s in dom (A '&' B) implies s in dom A ) )
thus ( s in dom A implies o ^ s in dom (A '&' B) ) ::_thesis: ( o ^ s in dom (A '&' B) implies s in dom A )
proof
assume s in dom A ; ::_thesis: o ^ s in dom (A '&' B)
then A6: o ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, TREES_1:def_9;
not <*1*> is_a_proper_prefix_of o ^ s by Th3;
hence o ^ s in dom (A '&' B) by A4, A5, A6, TREES_1:def_9; ::_thesis: verum
end;
assume A7: o ^ s in dom (A '&' B) ; ::_thesis: s in dom A
now__::_thesis:_s_in_dom_A
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: s in dom A
hence s in dom A by TREES_1:22; ::_thesis: verum
end;
supposeA8: s <> {} ; ::_thesis: s in dom A
now__::_thesis:_for_w_being_FinSequence_of_NAT_holds_
(_not_w_in_dom_B_or_not_o_^_s_=_<*1*>_^_w_)
given w being FinSequence of NAT such that w in dom B and
A9: o ^ s = <*1*> ^ w ; ::_thesis: contradiction
o is_a_prefix_of <*1*> ^ w by A9, TREES_1:1;
hence contradiction by TREES_1:50; ::_thesis: verum
end;
then A10: o ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A4, A5, A7, TREES_1:def_9;
o is_a_proper_prefix_of o ^ s by A8, TREES_1:10;
then ex w being FinSequence of NAT st
( w in dom A & o ^ s = o ^ w ) by A2, A3, A10, TREES_1:def_9;
hence s in dom A by FINSEQ_1:33; ::_thesis: verum
end;
end;
end;
hence s in dom A ; ::_thesis: verum
end;
then A11: dom A = (dom (A '&' B)) | o by TREES_1:def_6;
now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_
(_(_s_in_dom_B_implies_u_^_s_in_dom_(A_'&'_B)_)_&_(_u_^_s_in_dom_(A_'&'_B)_implies_s_in_dom_B_)_)
let s be FinSequence of NAT ; ::_thesis: ( ( s in dom B implies u ^ s in dom (A '&' B) ) & ( u ^ s in dom (A '&' B) implies s in dom B ) )
thus ( s in dom B implies u ^ s in dom (A '&' B) ) by A4, A5, TREES_1:def_9; ::_thesis: ( u ^ s in dom (A '&' B) implies s in dom B )
assume A12: u ^ s in dom (A '&' B) ; ::_thesis: s in dom B
now__::_thesis:_s_in_dom_B
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: s in dom B
hence s in dom B by TREES_1:22; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: s in dom B
then <*1*> is_a_proper_prefix_of u ^ s by TREES_1:10;
then ex w being FinSequence of NAT st
( w in dom B & u ^ s = <*1*> ^ w ) by A4, A5, A12, TREES_1:def_9;
hence s in dom B by FINSEQ_1:33; ::_thesis: verum
end;
end;
end;
hence s in dom B ; ::_thesis: verum
end;
then A13: dom B = (dom (A '&' B)) | u by TREES_1:def_6;
o <> Root (dom (A '&' B)) ;
hence card (dom A) < card (dom (A '&' B)) by A11, Th21; ::_thesis: card (dom B) < card (dom (A '&' B))
u <> Root (dom (A '&' B)) ;
hence card (dom B) < card (dom (A '&' B)) by A13, Th21; ::_thesis: verum
end;
definition
let IT be MP-wff;
attrIT is atomic means :Def16: :: MODAL_1:def 16
ex p being MP-variable st IT = @ p;
attrIT is negative means :Def17: :: MODAL_1:def 17
ex A being MP-wff st IT = 'not' A;
attrIT is necessitive means :Def18: :: MODAL_1:def 18
ex A being MP-wff st IT = (#) A;
attrIT is conjunctive means :Def19: :: MODAL_1:def 19
ex A, B being MP-wff st IT = A '&' B;
end;
:: deftheorem Def16 defines atomic MODAL_1:def_16_:_
for IT being MP-wff holds
( IT is atomic iff ex p being MP-variable st IT = @ p );
:: deftheorem Def17 defines negative MODAL_1:def_17_:_
for IT being MP-wff holds
( IT is negative iff ex A being MP-wff st IT = 'not' A );
:: deftheorem Def18 defines necessitive MODAL_1:def_18_:_
for IT being MP-wff holds
( IT is necessitive iff ex A being MP-wff st IT = (#) A );
:: deftheorem Def19 defines conjunctive MODAL_1:def_19_:_
for IT being MP-wff holds
( IT is conjunctive iff ex A, B being MP-wff st IT = A '&' B );
registration
cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like atomic for Element of MP-WFF ;
existence
ex b1 being MP-wff st b1 is atomic
proof
reconsider p = [3,0] as MP-variable by ZFMISC_1:105;
take @ p ; ::_thesis: @ p is atomic
take p ; :: according to MODAL_1:def_16 ::_thesis: @ p = @ p
thus @ p = @ p ; ::_thesis: verum
end;
cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like negative for Element of MP-WFF ;
existence
ex b1 being MP-wff st b1 is negative
proof
set A = VERUM ;
take 'not' VERUM ; ::_thesis: 'not' VERUM is negative
take VERUM ; :: according to MODAL_1:def_17 ::_thesis: 'not' VERUM = 'not' VERUM
thus 'not' VERUM = 'not' VERUM ; ::_thesis: verum
end;
cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like necessitive for Element of MP-WFF ;
existence
ex b1 being MP-wff st b1 is necessitive
proof
set A = VERUM ;
take (#) VERUM ; ::_thesis: (#) VERUM is necessitive
take VERUM ; :: according to MODAL_1:def_18 ::_thesis: (#) VERUM = (#) VERUM
thus (#) VERUM = (#) VERUM ; ::_thesis: verum
end;
cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like conjunctive for Element of MP-WFF ;
existence
ex b1 being MP-wff st b1 is conjunctive
proof
set B = VERUM ;
set A = VERUM ;
take VERUM '&' VERUM ; ::_thesis: VERUM '&' VERUM is conjunctive
take VERUM ; :: according to MODAL_1:def_19 ::_thesis: ex B being MP-wff st VERUM '&' VERUM = VERUM '&' B
take VERUM ; ::_thesis: VERUM '&' VERUM = VERUM '&' VERUM
thus VERUM '&' VERUM = VERUM '&' VERUM ; ::_thesis: verum
end;
end;
scheme :: MODAL_1:sch 1
MPInd{ P1[ Element of MP-WFF ] } :
for A being Element of MP-WFF holds P1[A]
provided
A1: P1[ VERUM ] and
A2: for p being MP-variable holds P1[ @ p] and
A3: for A being Element of MP-WFF st P1[A] holds
P1[ 'not' A] and
A4: for A being Element of MP-WFF st P1[A] holds
P1[ (#) A] and
A5: for A, B being Element of MP-WFF st P1[A] & P1[B] holds
P1[A '&' B]
proof
defpred S1[ Element of NAT ] means for A being MP-wff st card (dom A) <= $1 holds
P1[A];
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: for A being MP-wff st card (dom A) <= k holds
P1[A] ; ::_thesis: S1[k + 1]
let A be MP-wff; ::_thesis: ( card (dom A) <= k + 1 implies P1[A] )
assume A8: card (dom A) <= k + 1 ; ::_thesis: P1[A]
set a = Root (dom A);
set b = branchdeg (Root (dom A));
A9: branchdeg (Root (dom A)) <= 2 by Def5;
now__::_thesis:_P1[A]
percases ( branchdeg (Root (dom A)) = 0 or branchdeg (Root (dom A)) = 1 or branchdeg (Root (dom A)) = 2 ) by A9, NAT_1:26;
suppose branchdeg (Root (dom A)) = 0 ; ::_thesis: P1[A]
then A10: card (dom A) = 1 by Th17;
now__::_thesis:_P1[A]
percases ( A = VERUM or ex p being MP-variable st A = @ p ) by A10, Th36;
suppose A = VERUM ; ::_thesis: P1[A]
hence P1[A] by A1; ::_thesis: verum
end;
suppose ex p being MP-variable st A = @ p ; ::_thesis: P1[A]
hence P1[A] by A2; ::_thesis: verum
end;
end;
end;
hence P1[A] ; ::_thesis: verum
end;
supposeA11: branchdeg (Root (dom A)) = 1 ; ::_thesis: P1[A]
then A12: succ (Root (dom A)) = {<*0*>} by Th18;
then <*0*> in succ (Root (dom A)) by TARSKI:def_1;
then reconsider o = <*0*> as Element of dom A ;
A13: A = ((elementary_tree 1) --> (Root A)) with-replacement (<*0*>,(A | o)) by A12, Th23;
now__::_thesis:_P1[A]
percases ( A . (Root (dom A)) = [1,0] or A . (Root (dom A)) = [1,1] ) by A11, Def5;
supposeA14: A . (Root (dom A)) = [1,0] ; ::_thesis: P1[A]
( dom (A | o) = (dom A) | o & o <> Root (dom A) ) by TREES_2:def_10;
then card (dom (A | o)) < k + 1 by A8, Th21, XXREAL_0:2;
then A15: card (dom (A | o)) <= k by NAT_1:13;
A = 'not' (A | o) by A13, A14;
hence P1[A] by A3, A7, A15; ::_thesis: verum
end;
supposeA16: A . (Root (dom A)) = [1,1] ; ::_thesis: P1[A]
( dom (A | o) = (dom A) | o & o <> Root (dom A) ) by TREES_2:def_10;
then card (dom (A | o)) < k + 1 by A8, Th21, XXREAL_0:2;
then A17: card (dom (A | o)) <= k by NAT_1:13;
A = (#) (A | o) by A13, A16;
hence P1[A] by A4, A7, A17; ::_thesis: verum
end;
end;
end;
hence P1[A] ; ::_thesis: verum
end;
supposeA18: branchdeg (Root (dom A)) = 2 ; ::_thesis: P1[A]
then A19: succ (Root (dom A)) = {<*0*>,<*1*>} by Th19;
then ( <*0*> in succ (Root (dom A)) & <*1*> in succ (Root (dom A)) ) by TARSKI:def_2;
then reconsider o1 = <*0*>, o2 = <*1*> as Element of dom A ;
( dom (A | o1) = (dom A) | o1 & o1 <> Root (dom A) ) by TREES_2:def_10;
then card (dom (A | o1)) < k + 1 by A8, Th21, XXREAL_0:2;
then card (dom (A | o1)) <= k by NAT_1:13;
then A20: P1[A | o1] by A7;
( dom (A | o2) = (dom A) | o2 & o2 <> Root (dom A) ) by TREES_2:def_10;
then card (dom (A | o2)) < k + 1 by A8, Th21, XXREAL_0:2;
then card (dom (A | o2)) <= k by NAT_1:13;
then A21: P1[A | o2] by A7;
A = (((elementary_tree 2) --> (Root A)) with-replacement (<*0*>,(A | o1))) with-replacement (<*1*>,(A | o2)) by A19, Th25;
then A = (A | o1) '&' (A | o2) by A18, Def5;
hence P1[A] by A5, A20, A21; ::_thesis: verum
end;
end;
end;
hence P1[A] ; ::_thesis: verum
end;
let A be MP-wff; ::_thesis: P1[A]
A22: card (dom A) <= card (dom A) ;
A23: S1[ 0 ] by NAT_1:2;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A23, A6);
hence P1[A] by A22; ::_thesis: verum
end;
theorem :: MODAL_1:41
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 S1[ 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: S1[ VERUM ] ;
A2: for A being Element of MP-WFF st S1[A] holds
S1[ 'not' A] by Def17;
A3: for A, B being Element of MP-WFF st S1[A] & S1[B] holds
S1[A '&' B] by Def19;
A4: for A being Element of MP-WFF st S1[A] holds
S1[ (#) A] by Def18;
A5: for p being MP-variable holds S1[ @ p] by Def16;
thus for A being Element of MP-WFF holds S1[A] from MODAL_1:sch_1(A1, A5, A2, A4, A3); ::_thesis: verum
end;
theorem Th42: :: MODAL_1:42
for A being MP-wff holds
( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C )
proof
let A be MP-wff; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C )
now__::_thesis:_(_A_=_VERUM_or_ex_p_being_MP-variable_st_A_=_@_p_or_ex_B_being_MP-wff_st_A_=_'not'_B_or_ex_B_being_MP-wff_st_A_=_(#)_B_or_ex_B,_C_being_MP-wff_st_A_=_B_'&'_C_)
percases ( card (dom A) = 1 or card (dom A) >= 2 ) by NAT_1:26;
suppose card (dom A) = 1 ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C )
hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) by Th36; ::_thesis: verum
end;
suppose card (dom A) >= 2 ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C )
hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) by Th37; ::_thesis: verum
end;
end;
end;
hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: verum
end;
theorem Th43: :: MODAL_1:43
for p being MP-variable
for A, B being MP-wff holds
( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )
proof
let p be MP-variable; ::_thesis: for A, B being MP-wff holds
( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )
let A, B be MP-wff; ::_thesis: ( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )
set e2 = elementary_tree 2;
set e1 = elementary_tree 1;
set e0 = elementary_tree 0;
A1: dom (@ p) = elementary_tree 0 by FUNCOP_1:13;
A2: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
dom ((elementary_tree 1) --> [1,0]) = elementary_tree 1 by FUNCOP_1:13;
then dom ('not' A) = (elementary_tree 1) 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; ::_thesis: ( @ p <> (#) A & @ p <> A '&' B )
dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1 by FUNCOP_1:13;
then dom ((#) A) = (elementary_tree 1) 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; ::_thesis: @ p <> A '&' B
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A);
A3: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52;
A4: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28;
then dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11;
then A5: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A4, A3, TREES_1:def_9;
then dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,(dom B)) by TREES_2:def_11;
then <*1*> in dom (A '&' B) by A5, TREES_1:def_9;
hence @ p <> A '&' B by A1, TARSKI:def_1, TREES_1:29; ::_thesis: verum
end;
theorem Th44: :: MODAL_1:44
for A, B, C being MP-wff holds
( 'not' A <> (#) B & 'not' A <> B '&' C )
proof
let A, B, C be MP-wff; ::_thesis: ( 'not' A <> (#) B & 'not' A <> B '&' C )
set e2 = elementary_tree 2;
set e1 = elementary_tree 1;
set E = (elementary_tree 1) --> [1,0];
set F = (elementary_tree 1) --> [1,1];
reconsider e = {} as Element of dom ('not' A) by TREES_1:22;
A1: ( {} in dom ((#) B) & ( for u being FinSequence of NAT holds
( not u in dom B or not e = <*0*> ^ u or not ((#) B) . e = B . u ) ) ) by TREES_1:22;
A2: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
then A3: <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13;
then A4: dom ('not' A) = (dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11;
A5: <*0*> in dom ((elementary_tree 1) --> [1,1]) by A2, FUNCOP_1:13;
then dom ((#) B) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom B)) by TREES_2:def_11;
then A6: ((#) B) . e = ((elementary_tree 1) --> [1,1]) . e by A5, A1, TREES_2:def_11;
e in elementary_tree 1 by TREES_1:22;
then A7: ( ((elementary_tree 1) --> [1,0]) . e = [1,0] & ((elementary_tree 1) --> [1,1]) . e = [1,1] ) by FUNCOP_1:7;
( ( for u being FinSequence of NAT holds
( not u in dom A or not e = <*0*> ^ u or not ('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; ::_thesis: 'not' A <> B '&' C
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B);
A8: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52;
A9: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28;
then dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom B)) by TREES_2:def_11;
then A10: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) by A9, A8, TREES_1:def_9;
then dom (B '&' C) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B))) 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__::_thesis:_not_<*1*>_in_dom_((elementary_tree_1)_-->_[1,0])
assume <*1*> in dom ((elementary_tree 1) --> [1,0]) ; ::_thesis: contradiction
then ( <*1*> = {} or <*1*> = <*0*> ) by TARSKI:def_2, TREES_1:51;
hence contradiction by TREES_1:3; ::_thesis: verum
end;
assume not 'not' A <> B '&' C ; ::_thesis: contradiction
then ex s being FinSequence of NAT 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; ::_thesis: verum
end;
theorem Th45: :: MODAL_1:45
for A, B, C being MP-wff holds (#) A <> B '&' C
proof
let A, B, C be MP-wff; ::_thesis: (#) A <> B '&' C
set e2 = elementary_tree 2;
set e1 = elementary_tree 1;
set F = (elementary_tree 1) --> [1,1];
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B);
A1: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52;
A2: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28;
then dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom B)) by TREES_2:def_11;
then A3: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) by A2, A1, TREES_1:def_9;
then dom (B '&' C) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B))) 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 (#) A <> B '&' C ; ::_thesis: contradiction
A6: now__::_thesis:_not_<*1*>_in_dom_((elementary_tree_1)_-->_[1,1])
assume <*1*> in dom ((elementary_tree 1) --> [1,1]) ; ::_thesis: contradiction
then ( <*1*> = {} or <*1*> = <*0*> ) by TARSKI:def_2, TREES_1:51;
hence contradiction by TREES_1:3; ::_thesis: verum
end;
<*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
then A7: <*0*> in dom ((elementary_tree 1) --> [1,1]) by FUNCOP_1:13;
then dom ((#) A) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11;
then ex s being FinSequence of NAT 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; ::_thesis: verum
end;
Lm4: for A, B being MP-wff holds
( VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B )
proof
let A, B be MP-wff; ::_thesis: ( VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B )
set e2 = elementary_tree 2;
set e1 = elementary_tree 1;
A1: dom VERUM = elementary_tree 0 by FUNCOP_1:13;
set F = (elementary_tree 1) --> [1,1];
set E = (elementary_tree 1) --> [1,0];
A2: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
then <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13;
then ( dom ((elementary_tree 1) --> [1,0]) = elementary_tree 1 & dom ('not' A) = (dom ((elementary_tree 1) --> [1,0])) 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; ::_thesis: ( VERUM <> (#) A & VERUM <> A '&' B )
<*0*> in dom ((elementary_tree 1) --> [1,1]) by A2, FUNCOP_1:13;
then ( dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1 & dom ((#) A) = (dom ((elementary_tree 1) --> [1,1])) 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; ::_thesis: VERUM <> A '&' B
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A);
A3: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52;
A4: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28;
then dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11;
then A5: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A4, A3, TREES_1:def_9;
then dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) 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 VERUM <> A '&' B ; ::_thesis: contradiction
hence contradiction by A1, A6, TARSKI:def_1, TREES_1:29; ::_thesis: verum
end;
Lm5: [0,0] is MP-conective
proof
0 in {0,1,2} by ENUMSET1:def_1;
hence [0,0] is MP-conective by ZFMISC_1:87; ::_thesis: verum
end;
Lm6: for p being MP-variable holds VERUM <> @ p
proof
let p be MP-variable; ::_thesis: VERUM <> @ p
assume A1: not VERUM <> @ p ; ::_thesis: contradiction
( rng (@ p) = {p} & rng VERUM = {[0,0]} ) by FUNCOP_1:8;
then [0,0] in {p} by A1, TARSKI:def_1;
hence contradiction by Lm5, Th26, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: MODAL_1:46
for p being MP-variable
for A, B being MP-wff holds
( VERUM <> @ p & VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B ) by Lm4, Lm6;
scheme :: MODAL_1:sch 2
MPFuncEx{ F1() -> non empty set , F2() -> Element of F1(), F3( Element of MP-variables ) -> Element of F1(), F4( Element of F1()) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1() } :
ex f being Function of MP-WFF,F1() st
( f . VERUM = F2() & ( for p being MP-variable holds f . (@ p) = F3(p) ) & ( for A being Element of MP-WFF holds f . ('not' A) = F4((f . A)) ) & ( for A being Element of MP-WFF holds f . ((#) A) = F5((f . A)) ) & ( for A, B being Element of MP-WFF holds f . (A '&' B) = F6((f . A),(f . B)) ) )
proof
defpred S1[ Function of MP-WFF,F1(), Element of NAT ] means for A being MP-wff st card (dom A) <= $2 holds
( ( A = VERUM implies $1 . A = F2() ) & ( for p being MP-variable st A = @ p holds
$1 . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
$1 . A = F4(($1 . B)) ) & ( for B being MP-wff st A = (#) B holds
$1 . A = F5(($1 . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
$1 . A = F6(($1 . B),($1 . C)) ) );
defpred S2[ Element of F1(), Function of MP-WFF,F1(), Element of MP-WFF ] means ( ( $3 = VERUM implies $1 = F2() ) & ( for p being MP-variable st $3 = @ p holds
$1 = F3(p) ) & ( for A being MP-wff st $3 = 'not' A holds
$1 = F4(($2 . A)) ) & ( for A being MP-wff st $3 = (#) A holds
$1 = F5(($2 . A)) ) & ( for A, B being MP-wff st $3 = A '&' B holds
$1 = F6(($2 . A),($2 . B)) ) );
defpred S3[ Element of NAT ] means ex F being Function of MP-WFF,F1() st S1[F,$1];
defpred S4[ set , set ] means ex A being Element of MP-WFF st
( A = $1 & ( for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds
$2 = g . A ) );
A1: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
given F being Function of MP-WFF,F1() such that A2: S1[F,k] ; ::_thesis: S3[k + 1]
defpred S5[ Element of MP-WFF , Element of F1()] means ( ( card (dom $1) <> k + 1 implies $2 = F . $1 ) & ( card (dom $1) = k + 1 implies S2[$2,F,$1] ) );
A3: for x being Element of MP-WFF ex y being Element of F1() st S5[x,y]
proof
let A be Element of MP-WFF ; ::_thesis: ex y being Element of F1() st S5[A,y]
now__::_thesis:_(_(_card_(dom_A)_<>_k_+_1_&_ex_y_being_Element_of_F1()_st_verum_)_or_(_card_(dom_A)_=_k_+_1_&_A_=_VERUM_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_or_(_card_(dom_A)_=_k_+_1_&_ex_p_being_MP-variable_st_A_=_@_p_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_or_(_card_(dom_A)_=_k_+_1_&_ex_B_being_MP-wff_st_A_=_'not'_B_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_or_(_card_(dom_A)_=_k_+_1_&_ex_B_being_MP-wff_st_A_=_(#)_B_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_or_(_card_(dom_A)_=_k_+_1_&_ex_B,_C_being_MP-wff_st_A_=_B_'&'_C_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_)
percases ( card (dom A) <> k + 1 or ( card (dom A) = k + 1 & A = VERUM ) or ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B ) or ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C ) ) by Th42;
case card (dom A) <> k + 1 ; ::_thesis: ex y being Element of F1() st verum
take y = F . A; ::_thesis: verum
end;
caseA4: ( card (dom A) = k + 1 & A = VERUM ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A]
take y = F2(); ::_thesis: S2[y,F,A]
thus S2[y,F,A] by A4, Lm4, Lm6; ::_thesis: verum
end;
case ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A]
then consider p being MP-variable such that
A5: A = @ p ;
take y = F3(p); ::_thesis: S2[y,F,A]
thus S2[y,F,A] by A5, Lm6, Th32, Th43; ::_thesis: verum
end;
case ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A]
then consider B being MP-wff such that
A6: A = 'not' B ;
take y = F4((F . B)); ::_thesis: S2[y,F,A]
thus S2[y,F,A] by A6, Lm4, Th33, Th43, Th44; ::_thesis: verum
end;
case ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A]
then consider B being MP-wff such that
A7: A = (#) B ;
take y = F5((F . B)); ::_thesis: S2[y,F,A]
thus S2[y,F,A] by A7, Lm4, Th34, Th43, Th44, Th45; ::_thesis: verum
end;
case ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A]
then consider B, C being MP-wff such that
A8: A = B '&' C ;
take y = F6((F . B),(F . C)); ::_thesis: S2[y,F,A]
now__::_thesis:_for_B1,_C1_being_MP-wff_st_A_=_B1_'&'_C1_holds_
y_=_F6((F_._B1),(F_._C1))
let B1, C1 be MP-wff; ::_thesis: ( A = B1 '&' C1 implies y = F6((F . B1),(F . C1)) )
assume A9: A = B1 '&' C1 ; ::_thesis: y = F6((F . B1),(F . C1))
then B = B1 by A8, Th35;
hence y = F6((F . B1),(F . C1)) by A8, A9, Th35; ::_thesis: verum
end;
hence S2[y,F,A] by A8, Lm4, Th43, Th44, Th45; ::_thesis: verum
end;
end;
end;
hence ex y being Element of F1() st S5[A,y] ; ::_thesis: verum
end;
consider G being Function of MP-WFF,F1() such that
A10: for p being Element of MP-WFF holds S5[p,G . p] from FUNCT_2:sch_3(A3);
take H = G; ::_thesis: S1[H,k + 1]
thus S1[H,k + 1] ::_thesis: verum
proof
let A be Element of MP-WFF ; ::_thesis: ( card (dom A) <= k + 1 implies ( ( A = VERUM implies H . A = F2() ) & ( for p being MP-variable st A = @ p holds
H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) ) )
set p = card (dom A);
assume A11: card (dom A) <= k + 1 ; ::_thesis: ( ( A = VERUM implies H . A = F2() ) & ( for p being MP-variable st A = @ p holds
H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) )
thus ( A = VERUM implies H . A = F2() ) ::_thesis: ( ( for p being MP-variable st A = @ p holds
H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) )
proof
percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; ::_thesis: ( A = VERUM implies H . A = F2() )
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence ( A = VERUM implies H . A = F2() ) by A2; ::_thesis: verum
end;
suppose card (dom A) = k + 1 ; ::_thesis: ( A = VERUM implies H . A = F2() )
hence ( A = VERUM implies H . A = F2() ) by A10; ::_thesis: verum
end;
end;
end;
thus for p being MP-variable st A = @ p holds
H . A = F3(p) ::_thesis: ( ( for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) )
proof
let q be MP-variable; ::_thesis: ( A = @ q implies H . A = F3(q) )
assume A12: A = @ q ; ::_thesis: H . A = F3(q)
percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; ::_thesis: H . A = F3(q)
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F3(q) by A2, A12; ::_thesis: verum
end;
suppose card (dom A) = k + 1 ; ::_thesis: H . A = F3(q)
hence H . A = F3(q) by A10, A12; ::_thesis: verum
end;
end;
end;
thus for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ::_thesis: ( ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) )
proof
let B be MP-wff; ::_thesis: ( A = 'not' B implies H . A = F4((H . B)) )
assume A13: A = 'not' B ; ::_thesis: H . A = F4((H . B))
then card (dom B) <> k + 1 by A11, Th38;
then A14: H . B = F . B by A10;
percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; ::_thesis: H . A = F4((H . B))
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F4((H . B)) by A2, A13, A14; ::_thesis: verum
end;
suppose card (dom A) = k + 1 ; ::_thesis: H . A = F4((H . B))
hence H . A = F4((H . B)) by A10, A13, A14; ::_thesis: verum
end;
end;
end;
thus for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ::_thesis: for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C))
proof
let B be MP-wff; ::_thesis: ( A = (#) B implies H . A = F5((H . B)) )
assume A15: A = (#) B ; ::_thesis: H . A = F5((H . B))
then card (dom B) <> k + 1 by A11, Th39;
then A16: H . B = F . B by A10;
percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; ::_thesis: H . A = F5((H . B))
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F5((H . B)) by A2, A15, A16; ::_thesis: verum
end;
suppose card (dom A) = k + 1 ; ::_thesis: H . A = F5((H . B))
hence H . A = F5((H . B)) by A10, A15, A16; ::_thesis: verum
end;
end;
end;
thus for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ::_thesis: verum
proof
let B, C be MP-wff; ::_thesis: ( A = B '&' C implies H . A = F6((H . B),(H . C)) )
assume A17: A = B '&' C ; ::_thesis: H . A = F6((H . B),(H . C))
then card (dom B) <> k + 1 by A11, Th40;
then A18: H . B = F . B by A10;
card (dom C) <> k + 1 by A11, A17, Th40;
then A19: H . C = F . C by A10;
percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; ::_thesis: H . A = F6((H . B),(H . C))
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F6((H . B),(H . C)) by A2, A17, A18, A19; ::_thesis: verum
end;
suppose card (dom A) = k + 1 ; ::_thesis: H . A = F6((H . B),(H . C))
hence H . A = F6((H . B),(H . C)) by A10, A17, A18, A19; ::_thesis: verum
end;
end;
end;
end;
end;
A20: S3[ 0 ]
proof
set F = the Function of MP-WFF,F1();
take the Function of MP-WFF,F1() ; ::_thesis: S1[ the Function of MP-WFF,F1(), 0 ]
let A be MP-wff; ::_thesis: ( card (dom A) <= 0 implies ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) ) )
assume card (dom A) <= 0 ; ::_thesis: ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) )
hence ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) ) by NAT_1:2; ::_thesis: verum
end;
A21: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A20, A1);
A22: for x being set st x in MP-WFF holds
ex y being set st S4[x,y]
proof
let x be set ; ::_thesis: ( x in MP-WFF implies ex y being set st S4[x,y] )
assume x in MP-WFF ; ::_thesis: ex y being set st S4[x,y]
then reconsider x9 = x as Element of MP-WFF ;
consider F being Function of MP-WFF,F1() such that
A23: S1[F, card (dom x9)] by A21;
take F . x ; ::_thesis: S4[x,F . x]
take x9 ; ::_thesis: ( x9 = x & ( for g being Function of MP-WFF,F1() st S1[g, card (dom x9)] holds
F . x = g . x9 ) )
thus x = x9 ; ::_thesis: for g being Function of MP-WFF,F1() st S1[g, card (dom x9)] holds
F . x = g . x9
let G be Function of MP-WFF,F1(); ::_thesis: ( S1[G, card (dom x9)] implies F . x = G . x9 )
defpred S5[ Element of MP-WFF ] means ( card (dom $1) <= card (dom x9) implies F . $1 = G . $1 );
assume A24: S1[G, card (dom x9)] ; ::_thesis: F . x = G . x9
A25: for p being MP-variable holds S5[ @ p]
proof
let p be MP-variable; ::_thesis: S5[ @ p]
assume A26: card (dom (@ p)) <= card (dom x9) ; ::_thesis: F . (@ p) = G . (@ p)
hence F . (@ p) = F3(p) by A23
.= G . (@ p) by A24, A26 ;
::_thesis: verum
end;
A27: for A, B being Element of MP-WFF st S5[A] & S5[B] holds
S5[A '&' B]
proof
let A, B be MP-wff; ::_thesis: ( S5[A] & S5[B] implies S5[A '&' B] )
assume that
A28: ( S5[A] & S5[B] ) and
A29: card (dom (A '&' B)) <= card (dom x9) ; ::_thesis: F . (A '&' B) = G . (A '&' B)
( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) ) by Th40;
hence F . (A '&' B) = F6((G . A),(G . B)) by A23, A28, A29, XXREAL_0:2
.= G . (A '&' B) by A24, A29 ;
::_thesis: verum
end;
A30: for A being Element of MP-WFF st S5[A] holds
S5[ (#) A]
proof
let A be MP-wff; ::_thesis: ( S5[A] implies S5[ (#) A] )
assume A31: S5[A] ; ::_thesis: S5[ (#) A]
assume A32: card (dom ((#) A)) <= card (dom x9) ; ::_thesis: F . ((#) A) = G . ((#) A)
card (dom A) < card (dom ((#) A)) by Th39;
hence F . ((#) A) = F5((G . A)) by A23, A31, A32, XXREAL_0:2
.= G . ((#) A) by A24, A32 ;
::_thesis: verum
end;
A33: for A being Element of MP-WFF st S5[A] holds
S5[ 'not' A]
proof
let A be MP-wff; ::_thesis: ( S5[A] implies S5[ 'not' A] )
assume A34: S5[A] ; ::_thesis: S5[ 'not' A]
assume A35: card (dom ('not' A)) <= card (dom x9) ; ::_thesis: F . ('not' A) = G . ('not' A)
card (dom A) < card (dom ('not' A)) by Th38;
hence F . ('not' A) = F4((G . A)) by A23, A34, A35, XXREAL_0:2
.= G . ('not' A) by A24, A35 ;
::_thesis: verum
end;
A36: S5[ VERUM ]
proof
assume A37: card (dom VERUM) <= card (dom x9) ; ::_thesis: F . VERUM = G . VERUM
hence F . VERUM = F2() by A23
.= G . VERUM by A24, A37 ;
::_thesis: verum
end;
for p being Element of MP-WFF holds S5[p] from MODAL_1:sch_1(A36, A25, A33, A30, A27);
hence F . x = G . x9 ; ::_thesis: verum
end;
consider F being Function such that
A38: dom F = MP-WFF and
A39: for x being set st x in MP-WFF holds
S4[x,F . x] from CLASSES1:sch_1(A22);
rng F c= F1()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in F1() )
assume y in rng F ; ::_thesis: y in F1()
then consider x being set such that
A40: ( x in MP-WFF & y = F . x ) by A38, FUNCT_1:def_3;
consider p being Element of MP-WFF such that
p = x and
A41: for g being Function of MP-WFF,F1() st S1[g, card (dom p)] holds
y = g . p by A39, A40;
consider G being Function of MP-WFF,F1() such that
A42: S1[G, card (dom p)] by A21;
y = G . p by A41, A42;
hence y in F1() ; ::_thesis: verum
end;
then reconsider F = F as Function of MP-WFF,F1() by A38, FUNCT_2:def_1, RELSET_1:4;
consider A being MP-wff such that
A43: A = VERUM and
A44: for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds
F . VERUM = g . A by A39;
take F ; ::_thesis: ( F . VERUM = F2() & ( for p being MP-variable holds F . (@ p) = F3(p) ) & ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) )
consider G being Function of MP-WFF,F1() such that
A45: S1[G, card (dom A)] by A21;
F . VERUM = G . VERUM by A43, A44, A45;
hence F . VERUM = F2() by A43, A45; ::_thesis: ( ( for p being MP-variable holds F . (@ p) = F3(p) ) & ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) )
thus for p being MP-variable holds F . (@ p) = F3(p) ::_thesis: ( ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) )
proof
let p be MP-variable; ::_thesis: F . (@ p) = F3(p)
consider A being MP-wff such that
A46: A = @ p and
A47: for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds
F . (@ p) = g . A by A39;
consider G being Function of MP-WFF,F1() such that
A48: S1[G, card (dom A)] by A21;
F . (@ p) = G . (@ p) by A46, A47, A48;
hence F . (@ p) = F3(p) by A46, A48; ::_thesis: verum
end;
thus for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ::_thesis: ( ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) )
proof
let A be Element of MP-WFF ; ::_thesis: F . ('not' A) = F4((F . A))
consider A1 being MP-wff such that
A49: A1 = 'not' A and
A50: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds
F . ('not' A) = g . A1 by A39;
consider G being Function of MP-WFF,F1() such that
A51: S1[G, card (dom A1)] by A21;
A52: for k being Element of NAT st k < card (dom ('not' A)) holds
S1[G,k]
proof
let k be Element of NAT ; ::_thesis: ( k < card (dom ('not' A)) implies S1[G,k] )
assume A53: k < card (dom ('not' A)) ; ::_thesis: S1[G,k]
let a be Element of MP-WFF ; ::_thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; ::_thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) )
then card (dom a) <= card (dom ('not' A)) by A53, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) by A49, A51; ::_thesis: verum
end;
A54: ex B being MP-wff st
( B = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B)] holds
F . A = g . B ) ) by A39;
set k = card (dom A);
card (dom A) < card (dom ('not' A)) by Th38;
then S1[G, card (dom A)] by A52;
then A55: F . A = G . A by A54;
F . ('not' A) = G . ('not' A) by A49, A50, A51;
hence F . ('not' A) = F4((F . A)) by A49, A51, A55; ::_thesis: verum
end;
thus for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ::_thesis: for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B))
proof
let A be Element of MP-WFF ; ::_thesis: F . ((#) A) = F5((F . A))
consider A1 being MP-wff such that
A56: A1 = (#) A and
A57: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds
F . ((#) A) = g . A1 by A39;
consider G being Function of MP-WFF,F1() such that
A58: S1[G, card (dom A1)] by A21;
A59: for k being Element of NAT st k < card (dom ((#) A)) holds
S1[G,k]
proof
let k be Element of NAT ; ::_thesis: ( k < card (dom ((#) A)) implies S1[G,k] )
assume A60: k < card (dom ((#) A)) ; ::_thesis: S1[G,k]
let a be Element of MP-WFF ; ::_thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; ::_thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) )
then card (dom a) <= card (dom ((#) A)) by A60, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) by A56, A58; ::_thesis: verum
end;
A61: ex B being MP-wff st
( B = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B)] holds
F . A = g . B ) ) by A39;
set k = card (dom A);
card (dom A) < card (dom ((#) A)) by Th39;
then S1[G, card (dom A)] by A59;
then A62: F . A = G . A by A61;
F . ((#) A) = G . ((#) A) by A56, A57, A58;
hence F . ((#) A) = F5((F . A)) by A56, A58, A62; ::_thesis: verum
end;
thus for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ::_thesis: verum
proof
let A, B be Element of MP-WFF ; ::_thesis: F . (A '&' B) = F6((F . A),(F . B))
set k1 = card (dom A);
set k2 = card (dom B);
consider A1 being MP-wff such that
A63: A1 = A '&' B and
A64: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds
F . (A '&' B) = g . A1 by A39;
consider G being Function of MP-WFF,F1() such that
A65: S1[G, card (dom A1)] by A21;
A66: for k being Element of NAT st k < card (dom (A '&' B)) holds
S1[G,k]
proof
let k be Element of NAT ; ::_thesis: ( k < card (dom (A '&' B)) implies S1[G,k] )
assume A67: k < card (dom (A '&' B)) ; ::_thesis: S1[G,k]
let a be Element of MP-WFF ; ::_thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; ::_thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) )
then card (dom a) <= card (dom (A '&' B)) by A67, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) by A63, A65; ::_thesis: verum
end;
A68: ex B1 being MP-wff st
( B1 = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B1)] holds
F . A = g . B1 ) ) by A39;
card (dom A) < card (dom (A '&' B)) by Th40;
then S1[G, card (dom A)] by A66;
then A69: F . A = G . A by A68;
A70: ex C being MP-wff st
( C = B & ( for g being Function of MP-WFF,F1() st S1[g, card (dom C)] holds
F . B = g . C ) ) by A39;
card (dom B) < card (dom (A '&' B)) by Th40;
then S1[G, card (dom B)] by A66;
then A71: F . B = G . B by A70;
F . (A '&' B) = G . (A '&' B) by A63, A64, A65;
hence F . (A '&' B) = F6((F . A),(F . B)) by A63, A65, A69, A71; ::_thesis: verum
end;
end;