:: MODAL_1 semantic presentation

Lemma1: for b1 being Nat holds {} is_a_proper_prefix_of <*b1*>
proof end;

definition
let c1 be Tree;
func Root c1 -> Element of a1 equals :: MODAL_1:def 1
 {} ;
coherence
{} is Element of c1 by TREES_1:47;
end;

:: deftheorem Def1 defines Root MODAL_1:def 1 :
for b1 being Tree holds Root b1 = {} ;

definition
let c1 be non empty set ;
let c2 be DecoratedTree of c1;
func Root c2 -> Element of a1 equals :: MODAL_1:def 2
a2 . (Root (dom a2));
coherence
c2 . (Root (dom c2)) is Element of c1 ;
end;

:: deftheorem Def2 defines Root MODAL_1:def 2 :
for b1 being non empty set
for b2 being DecoratedTree of b1 holds Root b2 = b2 . (Root (dom b2));

theorem Th1: :: MODAL_1:1
canceled;

theorem Th2: :: MODAL_1:2
canceled;

theorem Th3: :: MODAL_1:3
for b1, b2 being Nat
for b3 being FinSequence of NAT st b1 <> b2 holds
not <*b1*>,<*b2*> ^ b3 are_c=-comparable
proof end;

theorem Th4: :: MODAL_1:4
for b1 being FinSequence of NAT st b1 <> {} holds
ex b2 being FinSequence of NAT ex b3 being Nat st b1 = <*b3*> ^ b2
proof end;

theorem Th5: :: MODAL_1:5
for b1, b2 being Nat
for b3 being FinSequence of NAT st b1 <> b2 holds
not <*b1*> is_a_proper_prefix_of <*b2*> ^ b3
proof end;

theorem Th6: :: MODAL_1:6
for b1, b2 being Nat
for b3 being FinSequence of NAT st b1 <> b2 holds
not <*b1*> is_a_prefix_of <*b2*> ^ b3
proof end;

theorem Th7: :: MODAL_1:7
for b1, b2 being Nat holds not <*b1*> is_a_proper_prefix_of <*b2*>
proof end;

theorem Th8: :: MODAL_1:8
canceled;

theorem Th9: :: MODAL_1:9
elementary_tree 1 = {{} ,<*0*>}
proof end;

theorem Th10: :: MODAL_1:10
elementary_tree 2 = {{} ,<*0*>,<*1*>}
proof end;

theorem Th11: :: MODAL_1:11
for b1 being Tree
for b2, b3 being Nat st b2 <= b3 & <*b3*> in b1 holds
<*b2*> in b1
proof end;

theorem Th12: :: MODAL_1:12
for b1, b2, b3 being FinSequence of NAT st b1 ^ b2 is_a_proper_prefix_of b1 ^ b3 holds
b2 is_a_proper_prefix_of b3
proof end;

theorem Th13: :: MODAL_1:13
for b1 being DecoratedTree of [:NAT ,NAT :] holds b1 in PFuncs (NAT * ),[:NAT ,NAT :]
proof end;

theorem Th14: :: MODAL_1:14
canceled;

theorem Th15: :: MODAL_1:15
for b1, b2, b3 being Tree
for b4 being Element of b1 st b1 with-replacement b4,b2 = b1 with-replacement b4,b3 holds
b2 = b3
proof end;

theorem Th16: :: MODAL_1:16
for b1 being non empty set
for b2, b3, b4 being DecoratedTree of b1
for b5 being Element of dom b2 st b2 with-replacement b5,b3 = b2 with-replacement b5,b4 holds
b3 = b4
proof end;

theorem Th17: :: MODAL_1:17
for b1, b2 being Tree
for b3 being FinSequence of NAT st b3 in b1 holds
for b4 being Element of b1 with-replacement b3,b2
for b5 being Element of b1 st b4 = b5 & b5 is_a_proper_prefix_of b3 holds
succ b4 = succ b5
proof end;

theorem Th18: :: MODAL_1:18
for b1, b2 being Tree
for b3 being FinSequence of NAT st b3 in b1 holds
for b4 being Element of b1 with-replacement b3,b2
for b5 being Element of b1 st b4 = b5 & not b3,b5 are_c=-comparable holds
succ b4 = succ b5
proof end;

theorem Th19: :: MODAL_1:19
for b1, b2 being Tree
for b3 being FinSequence of NAT st b3 in b1 holds
for b4 being Element of b1 with-replacement b3,b2
for b5 being Element of b2 st b4 = b3 ^ b5 holds
succ b4, succ b5 are_equipotent
proof end;

theorem Th20: :: MODAL_1:20
for b1 being Tree
for b2 being FinSequence of NAT st b2 in b1 holds
for b3 being Element of b1
for b4 being Element of b1 | b2 st b3 = b2 ^ b4 holds
succ b3, succ b4 are_equipotent
proof end;

theorem Th21: :: MODAL_1:21
canceled;

theorem Th22: :: MODAL_1:22
for b1 being finite Tree st branchdeg (Root b1) = 0 holds
( card b1 = 1 & b1 = {{} } )
proof end;

theorem Th23: :: MODAL_1:23
for b1 being finite Tree st branchdeg (Root b1) = 1 holds
succ (Root b1) = {<*0*>}
proof end;

theorem Th24: :: MODAL_1:24
for b1 being finite Tree st branchdeg (Root b1) = 2 holds
succ (Root b1) = {<*0*>,<*1*>}
proof end;

theorem Th25: :: MODAL_1:25
for b1 being Tree
for b2 being Element of b1 st b2 <> Root b1 holds
( b1 | b2,{ (b2 ^ b3) where B is Element of NAT * : b2 ^ b3 in b1 } are_equipotent & not Root b1 in { (b2 ^ b3) where B is Element of NAT * : b2 ^ b3 in b1 } )
proof end;

theorem Th26: :: MODAL_1:26
for b1 being finite Tree
for b2 being Element of b1 st b2 <> Root b1 holds
card (b1 | b2) < card b1
proof end;

theorem Th27: :: MODAL_1:27
for b1 being finite Tree
for b2 being Element of b1 st succ (Root b1) = {b2} holds
b1 = (elementary_tree 1) with-replacement <*0*>,(b1 | b2)
proof end;

Lemma24: for b1 being Function st dom b1 is finite holds
b1 is finite
proof end;

theorem Th28: :: MODAL_1:28
for b1 being non empty set
for b2 being finite DecoratedTree of b1
for b3 being Element of dom b2 st succ (Root (dom b2)) = {b3} & dom b2 is finite holds
b2 = ((elementary_tree 1) --> (Root b2)) with-replacement <*0*>,(b2 | b3)
proof end;

theorem Th29: :: MODAL_1:29
for b1 being Tree
for b2, b3 being Element of b1 st b1 is finite & b2 = <*0*> & b3 = <*1*> & succ (Root b1) = {b2,b3} holds
b1 = ((elementary_tree 2) with-replacement <*0*>,(b1 | b2)) with-replacement <*1*>,(b1 | b3)
proof end;

theorem Th30: :: MODAL_1:30
for b1 being non empty set
for b2 being DecoratedTree of b1
for b3, b4 being Element of dom b2 st dom b2 is finite & b3 = <*0*> & b4 = <*1*> & succ (Root (dom b2)) = {b3,b4} holds
b2 = (((elementary_tree 2) --> (Root b2)) with-replacement <*0*>,(b2 | b3)) with-replacement <*1*>,(b2 | b4)
proof end;

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

:: deftheorem Def3 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 Def4 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
proof end;
end;

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

theorem Th31: :: MODAL_1:31
MP-conectives misses MP-variables
proof end;

definition
let c1 be finite Tree;
let c2 be Element of c1;
redefine func branchdeg as branchdeg c2 -> Nat;
coherence
branchdeg c2 is Nat
proof end;
end;

definition
let c1 be non empty set ;
mode DOMAIN_DecoratedTree of c1 -> non empty set means :Def5: :: MODAL_1:def 5
for b1 being set st b1 in a2 holds
b1 is DecoratedTree of a1;
existence
ex b1 being non empty set st
for b2 being set st b2 in b1 holds
b2 is DecoratedTree of c1
proof end;
end;

:: deftheorem Def5 defines DOMAIN_DecoratedTree MODAL_1:def 5 :
for b1, b2 being non empty set holds
( b2 is DOMAIN_DecoratedTree of b1 iff for b3 being set st b3 in b2 holds
b3 is DecoratedTree of b1 );

definition
let c1 be non empty set ;
let c2 be DOMAIN_DecoratedTree of c1;
redefine mode Element as Element of c2 -> DecoratedTree of a1;
coherence
for b1 being Element of c2 holds b1 is DecoratedTree of c1 by Def5;
end;

definition
func MP-WFF -> DOMAIN_DecoratedTree of [:NAT ,NAT :] means :Def6: :: MODAL_1:def 6
( ( for b1 being DecoratedTree of [:NAT ,NAT :] st b1 in a1 holds
b1 is finite ) & ( for b1 being finite DecoratedTree of [:NAT ,NAT :] holds
( b1 in a1 iff for b2 being Element of dom b1 holds
( branchdeg b2 <= 2 & ( not branchdeg b2 = 0 or b1 . b2 = [0,0] or ex b3 being Nat st b1 . b2 = [3,b3] ) & ( not branchdeg b2 = 1 or b1 . b2 = [1,0] or b1 . b2 = [1,1] ) & ( branchdeg b2 = 2 implies b1 . b2 = [2,0] ) ) ) ) );
existence
ex b1 being DOMAIN_DecoratedTree of [:NAT ,NAT :] st
( ( for b2 being DecoratedTree of [:NAT ,NAT :] st b2 in b1 holds
b2 is finite ) & ( for b2 being finite DecoratedTree of [:NAT ,NAT :] holds
( b2 in b1 iff for b3 being Element of dom b2 holds
( branchdeg b3 <= 2 & ( not branchdeg b3 = 0 or b2 . b3 = [0,0] or ex b4 being Nat st b2 . b3 = [3,b4] ) & ( not branchdeg b3 = 1 or b2 . b3 = [1,0] or b2 . b3 = [1,1] ) & ( branchdeg b3 = 2 implies b2 . b3 = [2,0] ) ) ) ) )
proof end;
uniqueness
for b1, b2 being DOMAIN_DecoratedTree of [:NAT ,NAT :] st ( for b3 being DecoratedTree of [:NAT ,NAT :] st b3 in b1 holds
b3 is finite ) & ( for b3 being finite DecoratedTree of [:NAT ,NAT :] holds
( b3 in b1 iff for b4 being Element of dom b3 holds
( branchdeg b4 <= 2 & ( not branchdeg b4 = 0 or b3 . b4 = [0,0] or ex b5 being Nat st b3 . b4 = [3,b5] ) & ( not branchdeg b4 = 1 or b3 . b4 = [1,0] or b3 . b4 = [1,1] ) & ( branchdeg b4 = 2 implies b3 . b4 = [2,0] ) ) ) ) & ( for b3 being DecoratedTree of [:NAT ,NAT :] st b3 in b2 holds
b3 is finite ) & ( for b3 being finite DecoratedTree of [:NAT ,NAT :] holds
( b3 in b2 iff for b4 being Element of dom b3 holds
( branchdeg b4 <= 2 & ( not branchdeg b4 = 0 or b3 . b4 = [0,0] or ex b5 being Nat st b3 . b4 = [3,b5] ) & ( not branchdeg b4 = 1 or b3 . b4 = [1,0] or b3 . b4 = [1,1] ) & ( branchdeg b4 = 2 implies b3 . b4 = [2,0] ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines MP-WFF MODAL_1:def 6 :
for b1 being DOMAIN_DecoratedTree of [:NAT ,NAT :] holds
( b1 = MP-WFF iff ( ( for b2 being DecoratedTree of [:NAT ,NAT :] st b2 in b1 holds
b2 is finite ) & ( for b2 being finite DecoratedTree of [:NAT ,NAT :] holds
( b2 in b1 iff for b3 being Element of dom b2 holds
( branchdeg b3 <= 2 & ( not branchdeg b3 = 0 or b2 . b3 = [0,0] or ex b4 being Nat st b2 . b3 = [3,b4] ) & ( not branchdeg b3 = 1 or b2 . b3 = [1,0] or b2 . b3 = [1,1] ) & ( branchdeg b3 = 2 implies b2 . b3 = [2,0] ) ) ) ) ) );

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

registration
cluster -> finite Element of MP-WFF ;
coherence
for b1 being MP-wff holds b1 is finite by Def6;
end;

definition
let c1 be MP-wff;
let c2 be Element of dom c1;
redefine func | as c1 | c2 -> MP-wff;
coherence
c1 | c2 is MP-wff
proof end;
end;

definition
let c1 be Element of MP-conectives ;
func the_arity_of c1 -> Nat equals :: MODAL_1:def 7
a1 `1 ;
coherence
c1 `1 is Nat
proof end;
end;

:: deftheorem Def7 defines the_arity_of MODAL_1:def 7 :
for b1 being Element of MP-conectives holds the_arity_of b1 = b1 `1 ;

definition
let c1 be non empty set ;
let c2, c3 be DecoratedTree of c1;
let c4 be FinSequence of NAT ;
assume E31: c4 in dom c2 ;
func @ c2,c4,c3 -> DecoratedTree of a1 equals :Def8: :: MODAL_1:def 8
a2 with-replacement a4,a3;
coherence
c2 with-replacement c4,c3 is DecoratedTree of c1
proof end;
end;

:: deftheorem Def8 defines @ MODAL_1:def 8 :
for b1 being non empty set
for b2, b3 being DecoratedTree of b1
for b4 being FinSequence of NAT st b4 in dom b2 holds
@ b2,b4,b3 = b2 with-replacement b4,b3;

theorem Th32: :: MODAL_1:32
for b1 being MP-wff holds ((elementary_tree 1) --> [1,0]) with-replacement <*0*>,b1 is MP-wff
proof end;

theorem Th33: :: MODAL_1:33
for b1 being MP-wff holds ((elementary_tree 1) --> [1,1]) with-replacement <*0*>,b1 is MP-wff
proof end;

theorem Th34: :: MODAL_1:34
for b1, b2 being MP-wff holds (((elementary_tree 2) --> [2,0]) with-replacement <*0*>,b1) with-replacement <*1*>,b2 is MP-wff
proof end;

definition
let c1 be MP-wff;
func 'not' c1 -> MP-wff equals :: MODAL_1:def 9
((elementary_tree 1) --> [1,0]) with-replacement <*0*>,a1;
coherence
((elementary_tree 1) --> [1,0]) with-replacement <*0*>,c1 is MP-wff by Th32;
func (#) c1 -> MP-wff equals :: MODAL_1:def 10
((elementary_tree 1) --> [1,1]) with-replacement <*0*>,a1;
coherence
((elementary_tree 1) --> [1,1]) with-replacement <*0*>,c1 is MP-wff by Th33;
let c2 be MP-wff;
func c1 '&' c2 -> MP-wff equals :: MODAL_1:def 11
(((elementary_tree 2) --> [2,0]) with-replacement <*0*>,a1) with-replacement <*1*>,a2;
coherence
(((elementary_tree 2) --> [2,0]) with-replacement <*0*>,c1) with-replacement <*1*>,c2 is MP-wff by Th34;
end;

:: deftheorem Def9 defines 'not' MODAL_1:def 9 :
for b1 being MP-wff holds 'not' b1 = ((elementary_tree 1) --> [1,0]) with-replacement <*0*>,b1;

:: deftheorem Def10 defines (#) MODAL_1:def 10 :
for b1 being MP-wff holds (#) b1 = ((elementary_tree 1) --> [1,1]) with-replacement <*0*>,b1;

:: deftheorem Def11 defines '&' MODAL_1:def 11 :
for b1, b2 being MP-wff holds b1 '&' b2 = (((elementary_tree 2) --> [2,0]) with-replacement <*0*>,b1) with-replacement <*1*>,b2;

definition
let c1 be MP-wff;
func ? c1 -> MP-wff equals :: MODAL_1:def 12
 'not' ((#) ('not' a1));
correctness
coherence
'not' ((#) ('not' c1)) is MP-wff;
;
let c2 be MP-wff;
func c1 'or' c2 -> MP-wff equals :: MODAL_1:def 13
 'not' (('not' a1) '&' ('not' a2));
correctness
coherence
'not' (('not' c1) '&' ('not' c2)) is MP-wff;
;
func c1 => c2 -> MP-wff equals :: MODAL_1:def 14
 'not' (a1 '&' ('not' a2));
correctness
coherence
'not' (c1 '&' ('not' c2)) is MP-wff;
;
end;

:: deftheorem Def12 defines ? MODAL_1:def 12 :
for b1 being MP-wff holds ? b1 = 'not' ((#) ('not' b1));

:: deftheorem Def13 defines 'or' MODAL_1:def 13 :
for b1, b2 being MP-wff holds b1 'or' b2 = 'not' (('not' b1) '&' ('not' b2));

:: deftheorem Def14 defines => MODAL_1:def 14 :
for b1, b2 being MP-wff holds b1 => b2 = 'not' (b1 '&' ('not' b2));

theorem Th35: :: MODAL_1:35
for b1 being Nat holds (elementary_tree 0) --> [3,b1] is MP-wff
proof end;

theorem Th36: :: MODAL_1:36
(elementary_tree 0) --> [0,0] is MP-wff
proof end;

definition
let c1 be MP-variable;
func @ c1 -> MP-wff equals :: MODAL_1:def 15
(elementary_tree 0) --> a1;
coherence
(elementary_tree 0) --> c1 is MP-wff
proof end;
end;

:: deftheorem Def15 defines @ MODAL_1:def 15 :
for b1 being MP-variable holds @ b1 = (elementary_tree 0) --> b1;

theorem Th37: :: MODAL_1:37
for b1, b2 being MP-variable st @ b1 = @ b2 holds
b1 = b2
proof end;

Lemma38: for b1, b2 being Nat holds <*0*> in dom ((elementary_tree 1) --> [b1,b2])
proof end;

theorem Th38: :: MODAL_1:38
for b1, b2 being MP-wff st 'not' b1 = 'not' b2 holds
b1 = b2
proof end;

theorem Th39: :: MODAL_1:39
for b1, b2 being MP-wff st (#) b1 = (#) b2 holds
b1 = b2
proof end;

theorem Th40: :: MODAL_1:40
for b1, b2, b3, b4 being MP-wff st b1 '&' b2 = b3 '&' b4 holds
( b1 = b3 & b2 = b4 )
proof end;

definition
func VERUM -> MP-wff equals :: MODAL_1:def 16
(elementary_tree 0) --> [0,0];
coherence
(elementary_tree 0) --> [0,0] is MP-wff by Th36;
end;

:: deftheorem Def16 defines VERUM MODAL_1:def 16 :
VERUM = (elementary_tree 0) --> [0,0];

theorem Th41: :: MODAL_1:41
canceled;

theorem Th42: :: MODAL_1:42
for b1 being MP-wff holds
( not card (dom b1) = 1 or b1 = VERUM or ex b2 being MP-variable st b1 = @ b2 )
proof end;

theorem Th43: :: MODAL_1:43
for b1 being MP-wff holds
( not card (dom b1) >= 2 or ex b2 being MP-wff st
( b1 = 'not' b2 or b1 = (#) b2 ) or ex b2, b3 being MP-wff st b1 = b2 '&' b3 )
proof end;

theorem Th44: :: MODAL_1:44
for b1 being MP-wff holds card (dom b1) < card (dom ('not' b1))
proof end;

theorem Th45: :: MODAL_1:45
for b1 being MP-wff holds card (dom b1) < card (dom ((#) b1))
proof end;

theorem Th46: :: MODAL_1:46
for b1, b2 being MP-wff holds
( card (dom b1) < card (dom (b1 '&' b2)) & card (dom b2) < card (dom (b1 '&' b2)) )
proof end;

definition
let c1 be MP-wff;
attr a1 is atomic means :Def17: :: MODAL_1:def 17
ex b1 being MP-variable st a1 = @ b1;
attr a1 is negative means :Def18: :: MODAL_1:def 18
ex b1 being MP-wff st a1 = 'not' b1;
attr a1 is necessitive means :Def19: :: MODAL_1:def 19
ex b1 being MP-wff st a1 = (#) b1;
attr a1 is conjunctive means :Def20: :: MODAL_1:def 20
ex b1, b2 being MP-wff st a1 = b1 '&' b2;
end;

:: deftheorem Def17 defines atomic MODAL_1:def 17 :
for b1 being MP-wff holds
( b1 is atomic iff ex b2 being MP-variable st b1 = @ b2 );

:: deftheorem Def18 defines negative MODAL_1:def 18 :
for b1 being MP-wff holds
( b1 is negative iff ex b2 being MP-wff st b1 = 'not' b2 );

:: deftheorem Def19 defines necessitive MODAL_1:def 19 :
for b1 being MP-wff holds
( b1 is necessitive iff ex b2 being MP-wff st b1 = (#) b2 );

:: deftheorem Def20 defines conjunctive MODAL_1:def 20 :
for b1 being MP-wff holds
( b1 is conjunctive iff ex b2, b3 being MP-wff st b1 = b2 '&' b3 );

registration
cluster finite atomic Element of MP-WFF ;
existence
ex b1 being MP-wff st b1 is atomic
proof end;
cluster finite negative Element of MP-WFF ;
existence
ex b1 being MP-wff st b1 is negative
proof end;
cluster finite necessitive Element of MP-WFF ;
existence
ex b1 being MP-wff st b1 is necessitive
proof end;
cluster finite conjunctive Element of MP-WFF ;
existence
ex b1 being MP-wff st b1 is conjunctive
proof end;
end;

scheme :: MODAL_1:sch 1
s1{ P1[ Element of MP-WFF ] } :
for b1 being Element of MP-WFF holds P1[b1]
provided
E51: P1[ VERUM ] and
E52: for b1 being MP-variable holds P1[ @ b1] and
E53: for b1 being Element of MP-WFF st P1[b1] holds
P1[ 'not' b1] and
E54: for b1 being Element of MP-WFF st P1[b1] holds
P1[ (#) b1] and
E55: for b1, b2 being Element of MP-WFF st P1[b1] & P1[b2] holds
P1[b1 '&' b2]
proof end;

theorem Th47: :: MODAL_1:47
for b1 being Element of MP-WFF holds
( b1 = VERUM or b1 is atomic MP-wff or b1 is negative MP-wff or b1 is necessitive MP-wff or b1 is conjunctive MP-wff )
proof end;

theorem Th48: :: MODAL_1:48
for b1 being MP-wff holds
( b1 = VERUM or ex b2 being MP-variable st b1 = @ b2 or ex b2 being MP-wff st b1 = 'not' b2 or ex b2 being MP-wff st b1 = (#) b2 or ex b2, b3 being MP-wff st b1 = b2 '&' b3 )
proof end;

theorem Th49: :: MODAL_1:49
for b1 being MP-variable
for b2, b3 being MP-wff holds
( @ b1 <> 'not' b2 & @ b1 <> (#) b2 & @ b1 <> b2 '&' b3 )
proof end;

theorem Th50: :: MODAL_1:50
for b1, b2, b3 being MP-wff holds
( 'not' b1 <> (#) b2 & 'not' b1 <> b2 '&' b3 )
proof end;

theorem Th51: :: MODAL_1:51
for b1, b2, b3 being MP-wff holds (#) b1 <> b2 '&' b3
proof end;

Lemma55: for b1, b2 being MP-wff holds
( VERUM <> 'not' b1 & VERUM <> (#) b1 & VERUM <> b1 '&' b2 )
proof end;

Lemma56: [0,0] is MP-conective
proof end;

Lemma57: for b1 being MP-variable holds VERUM <> @ b1
proof end;

theorem Th52: :: MODAL_1:52
for b1 being MP-variable
for b2, b3 being MP-wff holds
( VERUM <> @ b1 & VERUM <> 'not' b2 & VERUM <> (#) b2 & VERUM <> b2 '&' b3 ) by Lemma55, Lemma57;

scheme :: MODAL_1:sch 2
s2{ 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 b1 being Function of MP-WFF ,F1() st
( b1 . VERUM = F2() & ( for b2 being MP-variable holds b1 . (@ b2) = F3(b2) ) & ( for b2 being Element of MP-WFF holds b1 . ('not' b2) = F4((b1 . b2)) ) & ( for b2 being Element of MP-WFF holds b1 . ((#) b2) = F5((b1 . b2)) ) & ( for b2, b3 being Element of MP-WFF holds b1 . (b2 '&' b3) = F6((b1 . b2),(b1 . b3)) ) )
proof end;

theorem Th53: :: MODAL_1:53
for b1 being Tree
for b2 being Element of b1 holds
( b2 in Leaves b1 iff not b2 ^ <*0*> in b1 )
proof end;

theorem Th54: :: MODAL_1:54
for b1 being Tree
for b2 being Element of b1 holds
( b2 in Leaves b1 iff for b3 being Nat holds not b2 ^ <*b3*> in b1 )
proof end;