:: by Alicia de la Cruz

::

:: Received September 30, 1991

:: Copyright (c) 1991-2017 Association of Mizar Users

Lm1: for m being Nat holds {} is_a_proper_prefix_of <*m*>

by XBOOLE_1:2;

definition
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));

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 Nat

for s being FinSequence of NAT st n <> m holds

not <*n*>,<*m*> ^ s are_c=-comparable

for s being FinSequence of NAT st n <> m holds

not <*n*>,<*m*> ^ s are_c=-comparable

proof end;

::$CT

theorem Th2: :: MODAL_1:3

for n, m being Nat

for s being FinSequence of NAT st n <> m holds

not <*n*> is_a_proper_prefix_of <*m*> ^ s

for s being FinSequence of NAT st n <> m holds

not <*n*> is_a_proper_prefix_of <*m*> ^ s

proof end;

::$CT 4

theorem :: MODAL_1:9

for w, s, t 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;

t is_a_proper_prefix_of s by TREES_1:49;

theorem Th6: :: 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

for z being Element of Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds

Z1 = Z2

proof end;

theorem Th7: :: 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

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 Th8: :: 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

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 Th9: :: 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

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

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 Th11: :: 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

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 Th15: :: 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 } )

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

theorem Th17: :: 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))

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 Th18: :: 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))

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

theorem Th19: :: 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))

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

theorem Th20: :: 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))

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

definition
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

end;
let v be Element of T;

:: original: branchdeg

redefine func branchdeg v -> Nat;

coherence

branchdeg v is Nat

proof end;

definition

ex b_{1} being DTree-set of [:NAT,NAT:] st

( ( for x being DecoratedTree of [:NAT,NAT:] st x in b_{1} holds

x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds

( x in b_{1} 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 b_{1}, b_{2} being DTree-set of [:NAT,NAT:] st ( for x being DecoratedTree of [:NAT,NAT:] st x in b_{1} holds

x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds

( x in b_{1} 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 b_{2} holds

x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds

( x in b_{2} 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

b_{1} = b_{2}
end;

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 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 ( ( 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] ) ) ) ) );

ex b

( ( for x being DecoratedTree of [:NAT,NAT:] st x in b

x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds

( x in b

( 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 b

x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds

( x in b

( 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 b

x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds

( x in b

( 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

b

proof end;

:: deftheorem Def5 defines MP-WFF MODAL_1:def 5 :

for b_{1} being DTree-set of [:NAT,NAT:] holds

( b_{1} = MP-WFF iff ( ( for x being DecoratedTree of [:NAT,NAT:] st x in b_{1} holds

x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds

( x in b_{1} 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 b

( b

x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds

( x in b

( 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] ) ) ) ) ) );

:: [0,0] = VERUM

:: [1,0] = negation

:: [1,1] = modal operator of necessity

:: [2,0] = &

:: [1,0] = negation

:: [1,1] = modal operator of necessity

:: [2,0] = &

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

end;
let a be Element of dom A;

:: original: |

redefine func A | a -> MP-wff;

coherence

A | a is MP-wff

proof end;

:: deftheorem defines the_arity_of MODAL_1:def 6 :

for a being Element of MP-conectives holds the_arity_of a = a `1 ;

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 ;

coherence

T with-replacement (p,T1) is DecoratedTree of D

end;
let T, T1 be DecoratedTree of D;

let p be FinSequence of NAT ;

assume A1: p in dom T ;

coherence

T with-replacement (p,T1) is DecoratedTree of D

proof 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);

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

definition

let A be MP-wff;

((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff by Th22;

((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff by Th23;

let B be MP-wff;

(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff by Th24;

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

((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff by Th22;

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

((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff by Th23;

let B be MP-wff;

func A '&' 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);

(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff by Th24;

:: deftheorem defines 'not' MODAL_1:def 8 :

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

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

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

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;

correctness

coherence

'not' ((#) ('not' A)) is MP-wff;

;

let B be MP-wff;

correctness

coherence

'not' (('not' A) '&' ('not' B)) is MP-wff;

;

correctness

coherence

'not' (A '&' ('not' B)) is MP-wff;

;

end;
correctness

coherence

'not' ((#) ('not' A)) is MP-wff;

;

let B be MP-wff;

correctness

coherence

'not' (('not' A) '&' ('not' B)) is MP-wff;

;

correctness

coherence

'not' (A '&' ('not' B)) is MP-wff;

;

:: deftheorem defines 'or' MODAL_1:def 12 :

for A, B being MP-wff holds A 'or' B = 'not' (('not' A) '&' ('not' B));

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

for A, B being MP-wff holds A => B = 'not' (A '&' ('not' B));

:: deftheorem defines @ MODAL_1:def 14 :

for p being MP-variable holds @ p = (elementary_tree 0) --> p;

for p being MP-variable holds @ p = (elementary_tree 0) --> p;

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

proof end;

theorem Th32: :: 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 )

( 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 Th35: :: MODAL_1:40

for A, B being MP-wff holds

( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) )

( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) )

proof 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 );

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

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

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

for IT being MP-wff holds

( IT is conjunctive iff ex A, B being MP-wff st IT = A '&' B );

registration

ex b_{1} being MP-wff st b_{1} is atomic

ex b_{1} being MP-wff st b_{1} is negative

ex b_{1} being MP-wff st b_{1} is necessitive

ex b_{1} being MP-wff st b_{1} is conjunctive
end;

cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like atomic for Element of MP-WFF ;

existence ex b

proof end;

cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like negative for Element of MP-WFF ;

existence ex b

proof end;

cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like necessitive for Element of MP-WFF ;

existence ex b

proof end;

cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like conjunctive for Element of MP-WFF ;

existence ex b

proof end;

scheme :: MODAL_1:sch 1

MPInd{ P_{1}[ Element of MP-WFF ] } :

provided

MPInd{ P

provided

A1:
P_{1}[ VERUM ]
and

A2: for p being MP-variable holds P_{1}[ @ p]
and

A3: for A being Element of MP-WFF st P_{1}[A] holds

P_{1}[ 'not' A]
and

A4: for A being Element of MP-WFF st P_{1}[A] holds

P_{1}[ (#) A]
and

A5: for A, B being Element of MP-WFF st P_{1}[A] & P_{1}[B] holds

P_{1}[A '&' B]

A2: for p being MP-variable holds P

A3: for A being Element of MP-WFF st P

P

A4: for A being Element of MP-WFF st P

P

A5: for A, B being Element of MP-WFF st P

P

proof 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 )

( 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 Th37: :: 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 )

( 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 Th38: :: MODAL_1:43

for p being MP-variable

for A, B being MP-wff holds

( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )

for A, B being MP-wff holds

( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B )

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:46

scheme :: MODAL_1:sch 2

MPFuncEx{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}( Element of MP-variables ) -> Element of F_{1}(), F_{4}( Element of F_{1}()) -> Element of F_{1}(), F_{5}( Element of F_{1}()) -> Element of F_{1}(), F_{6}( Element of F_{1}(), Element of F_{1}()) -> Element of F_{1}() } :

MPFuncEx{ F

ex f being Function of MP-WFF,F_{1}() st

( f . VERUM = F_{2}() & ( for p being MP-variable holds f . (@ p) = F_{3}(p) ) & ( for A being Element of MP-WFF holds f . ('not' A) = F_{4}((f . A)) ) & ( for A being Element of MP-WFF holds f . ((#) A) = F_{5}((f . A)) ) & ( for A, B being Element of MP-WFF holds f . (A '&' B) = F_{6}((f . A),(f . B)) ) )

( f . VERUM = F

proof end;