:: MODAL_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for m being Nat holds {} is_a_proper_prefix_of <*m*>
proof 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:47;
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 :: MODAL_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MODAL_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: MODAL_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for s being FinSequence of NAT st n <> m holds
not <*n*>,<*m*> ^ s are_c=-comparable
proof end;

theorem Th4: :: MODAL_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being FinSequence of NAT st s <> {} holds
ex w being FinSequence of NAT ex n being Nat st s = <*n*> ^ w
proof end;

theorem Th5: :: MODAL_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for s being FinSequence of NAT st n <> m holds
not <*n*> is_a_proper_prefix_of <*m*> ^ s
proof end;

theorem Th6: :: MODAL_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for s being FinSequence of NAT st n <> m holds
not <*n*> is_a_prefix_of <*m*> ^ s
proof end;

theorem Th7: :: MODAL_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat holds not <*n*> is_a_proper_prefix_of <*m*>
proof end;

theorem :: MODAL_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: MODAL_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
elementary_tree 1 = {{} ,<*0*>}
proof end;

theorem Th10: :: MODAL_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
elementary_tree 2 = {{} ,<*0*>,<*1*>}
proof end;

theorem Th11: :: MODAL_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being Tree
for n, m being Nat st n <= m & <*m*> in Z holds
<*n*> in Z
proof end;

theorem Th12: :: MODAL_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th13: :: MODAL_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t1 being DecoratedTree of [:NAT ,NAT :] holds t1 in PFuncs (NAT * ),[:NAT ,NAT :]
proof end;

theorem :: MODAL_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: MODAL_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th16: :: MODAL_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th17: :: MODAL_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th18: :: MODAL_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th19: :: MODAL_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th20: :: MODAL_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: MODAL_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th22: :: MODAL_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being finite Tree st branchdeg (Root Z) = 0 holds
( card Z = 1 & Z = {{} } )
proof end;

theorem Th23: :: MODAL_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being finite Tree st branchdeg (Root Z) = 1 holds
succ (Root Z) = {<*0*>}
proof end;

theorem Th24: :: MODAL_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being finite Tree st branchdeg (Root Z) = 2 holds
succ (Root Z) = {<*0*>,<*1*>}
proof end;

theorem Th25: :: MODAL_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being Tree
for o being Element of Z st o <> Root Z holds
( Z | o,{ (o ^ s') where s' is Element of NAT * : o ^ s' in Z } are_equipotent & not Root Z in { (o ^ w') where w' is Element of NAT * : o ^ w' in Z } )
proof end;

theorem Th26: :: MODAL_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being finite Tree
for o being Element of Z st o <> Root Z holds
card (Z | o) < card Z
proof end;

theorem Th27: :: MODAL_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

Lm2: for f being Function st dom f is finite holds
f is finite
proof end;

theorem Th28: :: MODAL_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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} & dom Z is finite holds
Z = ((elementary_tree 1) --> (Root Z)) with-replacement <*0*>,(Z | z)
proof end;

theorem Th29: :: MODAL_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being Tree
for x1, x2 being Element of Z st Z is finite & 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 end;

theorem Th30: :: MODAL_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for Z being DecoratedTree of D
for x1, x2 being Element of dom Z st dom Z is finite & 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 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
proof end;
end;

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

theorem Th31: :: MODAL_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
MP-conectives misses MP-variables
proof end;

definition
let T be finite Tree;
let v be Element of T;
:: original: branchdeg
redefine func branchdeg v -> Nat;
coherence
branchdeg v is Nat
proof end;
end;

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

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

definition
let D0 be non empty set ;
let D be DOMAIN_DecoratedTree of D0;
:: original: Element
redefine mode Element of D -> DecoratedTree of D0;
coherence
for b1 being Element of D holds b1 is DecoratedTree of D0 by Def5;
end;

definition
func MP-WFF -> DOMAIN_DecoratedTree of [:NAT ,NAT :] means :Def6: :: MODAL_1:def 6
( ( 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 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 DOMAIN_DecoratedTree 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 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 end;
uniqueness
for b1, b2 being DOMAIN_DecoratedTree 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 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 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 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 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 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 Element of MP-WFF ;
coherence
for b1 being MP-wff holds b1 is finite by Def6;
end;

definition
let A be MP-wff;
let a be Element of dom A;
:: original: |
redefine func A | a -> MP-wff;
coherence
A | a is MP-wff
proof end;
end;

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

:: deftheorem defines the_arity_of MODAL_1:def 7 :
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 :Def8: :: MODAL_1:def 8
T with-replacement p,T1;
coherence
T with-replacement p,T1 is DecoratedTree of D
proof end;
end;

:: deftheorem Def8 defines @ MODAL_1:def 8 :
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 Th32: :: MODAL_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being MP-wff holds ((elementary_tree 1) --> [1,0]) with-replacement <*0*>,A is MP-wff
proof end;

theorem Th33: :: MODAL_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being MP-wff holds ((elementary_tree 1) --> [1,1]) with-replacement <*0*>,A is MP-wff
proof end;

theorem Th34: :: MODAL_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being MP-wff holds (((elementary_tree 2) --> [2,0]) with-replacement <*0*>,A) with-replacement <*1*>,B is MP-wff
proof end;

definition
let A be MP-wff;
func 'not' A -> MP-wff equals :: MODAL_1:def 9
((elementary_tree 1) --> [1,0]) with-replacement <*0*>,A;
coherence
((elementary_tree 1) --> [1,0]) with-replacement <*0*>,A is MP-wff by Th32;
func (#) A -> MP-wff equals :: MODAL_1:def 10
((elementary_tree 1) --> [1,1]) with-replacement <*0*>,A;
coherence
((elementary_tree 1) --> [1,1]) with-replacement <*0*>,A is MP-wff by Th33;
let B be MP-wff;
func A '&' B -> MP-wff equals :: MODAL_1:def 11
(((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 Th34;
end;

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

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

:: deftheorem defines '&' MODAL_1:def 11 :
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 12
 'not' ((#) ('not' A));
correctness
coherence
'not' ((#) ('not' A)) is MP-wff;
;
let B be MP-wff;
func A 'or' B -> MP-wff equals :: MODAL_1:def 13
 'not' (('not' A) '&' ('not' B));
correctness
coherence
'not' (('not' A) '&' ('not' B)) is MP-wff;
;
func A => B -> MP-wff equals :: MODAL_1:def 14
 'not' (A '&' ('not' B));
correctness
coherence
'not' (A '&' ('not' B)) is MP-wff;
;
end;

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

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

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

theorem Th35: :: MODAL_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds (elementary_tree 0) --> [3,n] is MP-wff
proof end;

theorem Th36: :: MODAL_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(elementary_tree 0) --> [0,0] is MP-wff
proof end;

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

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

theorem Th37: :: MODAL_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being MP-variable st @ p = @ q holds
p = q
proof end;

Lm3: for n, m being Nat holds <*0*> in dom ((elementary_tree 1) --> [n,m])
proof end;

theorem Th38: :: MODAL_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being MP-wff st 'not' A = 'not' B holds
A = B
proof end;

theorem Th39: :: MODAL_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being MP-wff st (#) A = (#) B holds
A = B
proof end;

theorem Th40: :: MODAL_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, A1, B1 being MP-wff st A '&' B = A1 '&' B1 holds
( A = A1 & B = B1 )
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 defines VERUM MODAL_1:def 16 :
VERUM = (elementary_tree 0) --> [0,0];

theorem :: MODAL_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th42: :: MODAL_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being MP-wff holds
( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p )
proof end;

theorem Th43: :: MODAL_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th44: :: MODAL_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being MP-wff holds card (dom A) < card (dom ('not' A))
proof end;

theorem Th45: :: MODAL_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being MP-wff holds card (dom A) < card (dom ((#) A))
proof end;

theorem Th46: :: MODAL_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being MP-wff holds
( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) )
proof end;

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

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

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

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

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

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
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 end;

theorem :: MODAL_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th48: :: MODAL_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th49: :: MODAL_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being MP-variable
for A, B being MP-wff holds
( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )
proof end;

theorem Th50: :: MODAL_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being MP-wff holds
( 'not' A <> (#) B & 'not' A <> B '&' C )
proof end;

theorem Th51: :: MODAL_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being MP-wff holds (#) A <> B '&' C
proof end;

Lm4: for A, B being MP-wff holds
( VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B )
proof end;

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

Lm6: for p being MP-variable holds VERUM <> @ p
proof end;

theorem :: MODAL_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: MODAL_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for t being Element of T holds
( t in Leaves T iff not t ^ <*0*> in T )
proof end;

theorem :: MODAL_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for t being Element of T holds
( t in Leaves T iff for n being Nat holds not t ^ <*n*> in T )
proof end;