:: by Mariusz Giero

::

:: Received October 22, 2015

:: Copyright (c) 2015-2018 Association of Mizar Users

theorem Lm1: :: LTLAXIO5:1

for X being set

for f being FinSequence of X

for i being Nat st 1 <= i & i <= len f holds

f . i = f /. i

for f being FinSequence of X

for i being Nat st 1 <= i & i <= len f holds

f . i = f /. i

proof end;

::#INSERT: LTLB with normal semantics is monotonic

theorem th17: :: LTLAXIO5:4

for A, B, C being Element of LTLB_WFF holds (A => (B => C)) => ((A => B) => (A => C)) is LTL_TAUT_OF_PL

proof end;

theorem th20: :: LTLAXIO5:8

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF holds F |- ('G' (A => B)) => (('G' (A => ('X' A))) => ('G' (A => ('G' B))))

for F being Subset of LTLB_WFF holds F |- ('G' (A => B)) => (('G' (A => ('X' A))) => ('G' (A => ('G' B))))

proof end;

::#INSERT: A formula A is initially valid in the temporal structure M

definition

let M be LTLModel;

let A be Element of LTLB_WFF ;

end;
let A be Element of LTLB_WFF ;

::#INSERT: A formula A is initially valid in the temporal structure M

:: deftheorem defines |=0 LTLAXIO5:def 1 :

for M being LTLModel

for A being Element of LTLB_WFF holds

( M |=0 A iff (SAT M) . [0,A] = 1 );

for M being LTLModel

for A being Element of LTLB_WFF holds

( M |=0 A iff (SAT M) . [0,A] = 1 );

::#INSERT: A set F of formulas is initially valid in the temporal structure M

definition

let M be LTLModel;

let F be Subset of LTLB_WFF;

end;
let F be Subset of LTLB_WFF;

::#INSERT: A set F of formulas is initially valid in the temporal structure M

:: deftheorem defines |=0 LTLAXIO5:def 2 :

for M being LTLModel

for F being Subset of LTLB_WFF holds

( M |=0 F iff for A being Element of LTLB_WFF st A in F holds

M |=0 A );

for M being LTLModel

for F being Subset of LTLB_WFF holds

( M |=0 F iff for A being Element of LTLB_WFF st A in F holds

M |=0 A );

::#INSERT: A formula A is an initial consequence of a set F of formulas

:: deftheorem defines |=0 LTLAXIO5:def 3 :

for F being Subset of LTLB_WFF

for A being Element of LTLB_WFF holds

( F |=0 A iff for M being LTLModel st M |=0 F holds

M |=0 A );

for F being Subset of LTLB_WFF

for A being Element of LTLB_WFF holds

( F |=0 A iff for M being LTLModel st M |=0 F holds

M |=0 A );

::#INSERT: The numbers 2.6.1-2.6.8, put in comments in the article,

::#INSERT: correspond to the ones in: Kroeger, Merz. Temporal Logic and State

::#INSERT: Systems. 2008. Springer-Verlag.

::#INSERT: 2.6.1a-trivial: M |= A implies M |=0 A

::#INSERT: correspond to the ones in: Kroeger, Merz. Temporal Logic and State

::#INSERT: Systems. 2008. Springer-Verlag.

::#INSERT: 2.6.1a-trivial: M |= A implies M |=0 A

::#INSERT: 2.6.1b

::#INSERT: 2.6.2a

definition

let F be Subset of LTLB_WFF;

coherence

{ ('G' A) where A is Element of LTLB_WFF : A in F } is Subset of LTLB_WFF;

end;
func 'G' F -> Subset of LTLB_WFF equals :: LTLAXIO5:def 4

{ ('G' A) where A is Element of LTLB_WFF : A in F } ;

correctness { ('G' A) where A is Element of LTLB_WFF : A in F } ;

coherence

{ ('G' A) where A is Element of LTLB_WFF : A in F } is Subset of LTLB_WFF;

proof end;

:: deftheorem defines 'G' LTLAXIO5:def 4 :

for F being Subset of LTLB_WFF holds 'G' F = { ('G' A) where A is Element of LTLB_WFF : A in F } ;

for F being Subset of LTLB_WFF holds 'G' F = { ('G' A) where A is Element of LTLB_WFF : A in F } ;

::#INSERT: 2.6.2b

::#INSERT: The converse of 2.6.2a does not hold in general

theorem th263pa: :: LTLAXIO5:19

for F, G being Subset of LTLB_WFF

for M being LTLModel holds

( ( M |=0 F & M |=0 G ) iff M |=0 F \/ G )

for M being LTLModel holds

( ( M |=0 F & M |=0 G ) iff M |=0 F \/ G )

proof end;

::#INSERT: 2.6.3

::#INSERT: In compare to normal consequence (LTLAXIO1:30), the relationship

::#INSERT: between implication and initial consequence holds in the classical

::#INSERT: form

::#INSERT: In compare to normal consequence (LTLAXIO1:30), the relationship

::#INSERT: between implication and initial consequence holds in the classical

::#INSERT: form

theorem th263: :: LTLAXIO5:21

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF holds

( F \/ {A} |=0 B iff F |=0 A => B )

for F being Subset of LTLB_WFF holds

( F \/ {A} |=0 B iff F |=0 A => B )

proof end;

::#INSERT: Universal validity concepts are equaivalent as far as

::#INSERT: initial and normal semantics is concerned:

::#INSERT: 2.6.4: one line proof:

::#INSERT: {}LTLB_WFF |= A iff {}LTLB_WFF |=0 A by th262b,th264p

::#INSERT: 2.1.8

::#INSERT: initial and normal semantics is concerned:

::#INSERT: 2.6.4: one line proof:

::#INSERT: {}LTLB_WFF |= A iff {}LTLB_WFF |=0 A by th262b,th264p

::#INSERT: 2.1.8

theorem th218: :: LTLAXIO5:23

for A being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds

{} LTLB_WFF |= B ) holds

{} LTLB_WFF |= A

for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds

{} LTLB_WFF |= B ) holds

{} LTLB_WFF |= A

proof end;

::#INSERT: 2.6.5

theorem th265: :: LTLAXIO5:24

for A being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds

{} LTLB_WFF |=0 B ) holds

{} LTLB_WFF |=0 A

for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds

{} LTLB_WFF |=0 B ) holds

{} LTLB_WFF |=0 A

proof end;

::#INSERT: Axioms

::#INSERT: Derivation rules

definition

let p, q be Element of LTLB_WFF ;

end;
pred p NEX0_rule q means :: LTLAXIO5:def 7

ex A being Element of LTLB_WFF st

( p = 'G' A & q = 'G' ('X' A) );

let r be Element of LTLB_WFF ;ex A being Element of LTLB_WFF st

( p = 'G' A & q = 'G' ('X' A) );

:: deftheorem defines REFL0_rule LTLAXIO5:def 6 :

for p, q being Element of LTLB_WFF holds

( p REFL0_rule q iff p = 'G' q );

for p, q being Element of LTLB_WFF holds

( p REFL0_rule q iff p = 'G' q );

:: deftheorem defines NEX0_rule LTLAXIO5:def 7 :

for p, q being Element of LTLB_WFF holds

( p NEX0_rule q iff ex A being Element of LTLB_WFF st

( p = 'G' A & q = 'G' ('X' A) ) );

for p, q being Element of LTLB_WFF holds

( p NEX0_rule q iff ex A being Element of LTLB_WFF st

( p = 'G' A & q = 'G' ('X' A) ) );

:: deftheorem defines MP0_rule LTLAXIO5:def 8 :

for p, q, r being Element of LTLB_WFF holds

( p,q MP0_rule r iff ex A, B being Element of LTLB_WFF st

( p = 'G' A & q = 'G' (A => B) & r = 'G' B ) );

for p, q, r being Element of LTLB_WFF holds

( p,q MP0_rule r iff ex A, B being Element of LTLB_WFF st

( p = 'G' A & q = 'G' (A => B) & r = 'G' B ) );

:: deftheorem defines IND0_rule LTLAXIO5:def 9 :

for p, q, r being Element of LTLB_WFF holds

( p,q IND0_rule r iff ex A, B being Element of LTLB_WFF st

( p = 'G' (A => B) & q = 'G' (A => ('X' A)) & r = 'G' (A => ('G' B)) ) );

for p, q, r being Element of LTLB_WFF holds

( p,q IND0_rule r iff ex A, B being Element of LTLB_WFF st

( p = 'G' (A => B) & q = 'G' (A => ('X' A)) & r = 'G' (A => ('G' B)) ) );

::#INSERT: Definition of derivation step

definition

let i be Nat;

let f be FinSequence of LTLB_WFF ;

let X be Subset of LTLB_WFF;

end;
let f be FinSequence of LTLB_WFF ;

let X be Subset of LTLB_WFF;

::#INSERT: Definition of derivation step

pred prc0 f,X,i means :Def29: :: LTLAXIO5:def 10

( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) );

( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) );

:: deftheorem Def29 defines prc0 LTLAXIO5:def 10 :

for i being Nat

for f being FinSequence of LTLB_WFF

for X being Subset of LTLB_WFF holds

( prc0 f,X,i iff ( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) );

for i being Nat

for f being FinSequence of LTLB_WFF

for X being Subset of LTLB_WFF holds

( prc0 f,X,i iff ( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) );

::#INSERT: Properties of derivation step prc0 - analogue of "prc" from LTLAXIO1

theorem Th38: :: LTLAXIO5:26

for X being Subset of LTLB_WFF

for f, f2 being FinSequence of LTLB_WFF

for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i holds

prc0 f2,X,i + n

for f, f2 being FinSequence of LTLB_WFF

for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i holds

prc0 f2,X,i + n

proof end;

theorem Th39: :: LTLAXIO5:27

for X being Subset of LTLB_WFF

for f, f1, f2 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds

prc0 f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds

prc0 f1,X,i ) holds

for i being Nat st 1 <= i & i <= len f2 holds

prc0 f2,X,i

for f, f1, f2 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds

prc0 f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds

prc0 f1,X,i ) holds

for i being Nat st 1 <= i & i <= len f2 holds

prc0 f2,X,i

proof end;

:: Derivability

:: deftheorem defines |-0 LTLAXIO5:def 11 :

for X being Subset of LTLB_WFF

for p being Element of LTLB_WFF holds

( X |-0 p iff ex f being FinSequence of LTLB_WFF st

( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds

prc0 f,X,i ) ) );

for X being Subset of LTLB_WFF

for p being Element of LTLB_WFF holds

( X |-0 p iff ex f being FinSequence of LTLB_WFF st

( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds

prc0 f,X,i ) ) );

:: Properties of derivation sequences

theorem Th40: :: LTLAXIO5:28

for p being Element of LTLB_WFF

for X being Subset of LTLB_WFF

for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds

prc0 f1,X,i ) & prc0 f,X, len f holds

( ( for i being Nat st 1 <= i & i <= len f holds

prc0 f,X,i ) & X |-0 p )

for X being Subset of LTLB_WFF

for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds

prc0 f1,X,i ) & prc0 f,X, len f holds

( ( for i being Nat st 1 <= i & i <= len f holds

prc0 f,X,i ) & X |-0 p )

proof end;

::#INSERT: Axioms are sound

::#INSERT: MP_rule is sound

theorem Th3: :: LTLAXIO5:30

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |=0 A & F |=0 A => B holds

F |=0 B

for F being Subset of LTLB_WFF st F |=0 A & F |=0 A => B holds

F |=0 B

proof end;

::#INSERT: MP0_rule is sound

theorem Th4: :: LTLAXIO5:31

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |=0 'G' A & F |=0 'G' (A => B) holds

F |=0 'G' B

for F being Subset of LTLB_WFF st F |=0 'G' A & F |=0 'G' (A => B) holds

F |=0 'G' B

proof end;

::#INSERT: NEX0_rule is sound

theorem Th5: :: LTLAXIO5:32

for A being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |=0 'G' A holds

F |=0 'G' ('X' A)

for F being Subset of LTLB_WFF st F |=0 'G' A holds

F |=0 'G' ('X' A)

proof end;

::#INSERT: REFL0_rule is sound

::#INSERT: IND0_rule is sound

theorem Th7: :: LTLAXIO5:34

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |=0 'G' (A => B) & F |=0 'G' (A => ('X' A)) holds

F |=0 'G' (A => ('G' B))

for F being Subset of LTLB_WFF st F |=0 'G' (A => B) & F |=0 'G' (A => ('X' A)) holds

F |=0 'G' (A => ('G' B))

proof end;

::#INSERT: Axioms and premises are derivable

theorem th10: :: LTLAXIO5:36

for A being Element of LTLB_WFF

for F being Subset of LTLB_WFF st ( A in LTL0_axioms or A in F ) holds

F |-0 A

for F being Subset of LTLB_WFF st ( A in LTL0_axioms or A in F ) holds

F |-0 A

proof end;

::#INSERT: REFL0_rule is derivable

::#INSERT: NEX0_rule is derivable

theorem th12: :: LTLAXIO5:38

for A being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |-0 'G' A holds

F |-0 'G' ('X' A)

for F being Subset of LTLB_WFF st F |-0 'G' A holds

F |-0 'G' ('X' A)

proof end;

::#INSERT: MP_rule is derivable

theorem th11a: :: LTLAXIO5:39

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |-0 A & F |-0 A => B holds

F |-0 B

for F being Subset of LTLB_WFF st F |-0 A & F |-0 A => B holds

F |-0 B

proof end;

::#INSERT: MP0_rule is derivable

theorem th11: :: LTLAXIO5:40

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |-0 'G' A & F |-0 'G' (A => B) holds

F |-0 'G' B

for F being Subset of LTLB_WFF st F |-0 'G' A & F |-0 'G' (A => B) holds

F |-0 'G' B

proof end;

::#INSERT: IND0_rule is derivable

theorem th13: :: LTLAXIO5:41

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |-0 'G' (A => B) & F |-0 'G' (A => ('X' A)) holds

F |-0 'G' (A => ('G' B))

for F being Subset of LTLB_WFF st F |-0 'G' (A => B) & F |-0 'G' (A => ('X' A)) holds

F |-0 'G' (A => ('G' B))

proof end;

::#INSERT: 2.6.7

::#INSERT: auxilliary theorem to prove completeness theorem

::#INSERT: auxilliary theorem to prove completeness theorem

::#INSERT: Generalized theorem 2.6.7 does not hold, i.e.,

::#INSERT: not for F,A holds (F |- A implies F |-0 A);

::#INSERT: not for F,A holds (F |- A implies F |-0 A);

::#INSERT: LTLB with initial semantics is monotonic

definition

let f be FinSequence of LTLB_WFF ;

let A be Element of LTLB_WFF ;

( ( len f > 0 implies ex b_{1} being FinSequence of LTLB_WFF st

( len b_{1} = len f & b_{1} . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

b_{1} . (i + 1) = (f /. (i + 1)) => (b_{1} /. i) ) ) ) & ( not len f > 0 implies ex b_{1} being FinSequence of LTLB_WFF st b_{1} = <*> LTLB_WFF ) )

for b_{1}, b_{2} being FinSequence of LTLB_WFF holds

( ( len f > 0 & len b_{1} = len f & b_{1} . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

b_{1} . (i + 1) = (f /. (i + 1)) => (b_{1} /. i) ) & len b_{2} = len f & b_{2} . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

b_{2} . (i + 1) = (f /. (i + 1)) => (b_{2} /. i) ) implies b_{1} = b_{2} ) & ( not len f > 0 & b_{1} = <*> LTLB_WFF & b_{2} = <*> LTLB_WFF implies b_{1} = b_{2} ) )

for b_{1} being FinSequence of LTLB_WFF holds verum
;

end;
let A be Element of LTLB_WFF ;

func implications (f,A) -> FinSequence of LTLB_WFF means :imps: :: LTLAXIO5:def 12

( len it = len f & it . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

it . (i + 1) = (f /. (i + 1)) => (it /. i) ) ) if len f > 0

otherwise it = <*> LTLB_WFF;

existence ( len it = len f & it . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

it . (i + 1) = (f /. (i + 1)) => (it /. i) ) ) if len f > 0

otherwise it = <*> LTLB_WFF;

( ( len f > 0 implies ex b

( len b

b

proof end;

uniqueness for b

( ( len f > 0 & len b

b

b

proof end;

consistency for b

:: deftheorem imps defines implications LTLAXIO5:def 12 :

for f being FinSequence of LTLB_WFF

for A being Element of LTLB_WFF

for b_{3} being FinSequence of LTLB_WFF holds

( ( len f > 0 implies ( b_{3} = implications (f,A) iff ( len b_{3} = len f & b_{3} . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

b_{3} . (i + 1) = (f /. (i + 1)) => (b_{3} /. i) ) ) ) ) & ( not len f > 0 implies ( b_{3} = implications (f,A) iff b_{3} = <*> LTLB_WFF ) ) );

for f being FinSequence of LTLB_WFF

for A being Element of LTLB_WFF

for b

( ( len f > 0 implies ( b

b

::#INSERT: Deduction theorem holds in the classical form compared with

::#INSERT: Deduction theorem for LTLB with normal semantics (see LTLAXIO1:57)

::#INSERT: Deduction theorem for LTLB with normal semantics (see LTLAXIO1:57)

theorem :: LTLAXIO5:48

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F \/ {A} |-0 B holds

F |-0 A => B

for F being Subset of LTLB_WFF st F \/ {A} |-0 B holds

F |-0 A => B

proof end;

:: Converse of Deduction Theorem

theorem :: LTLAXIO5:49

for A, B being Element of LTLB_WFF

for F being Subset of LTLB_WFF st F |-0 A => B holds

F \/ {A} |-0 B

for F being Subset of LTLB_WFF st F |-0 A => B holds

F \/ {A} |-0 B

proof end;

registration
end;

theorem :: LTLAXIO5:50

for A being Element of LTLB_WFF

for F being finite Subset of LTLB_WFF holds

( F |- A iff 'G' F |-0 A )

for F being finite Subset of LTLB_WFF holds

( F |- A iff 'G' F |-0 A )

proof end;

::#INSERT: The counterexample that "for F,A holds (F |- A implies F |-0 A)"

::#INSERT: is not true. Another counterexample see above for theorem "th14".

::#INSERT: is not true. Another counterexample see above for theorem "th14".

::#INSERT: The converse of the above theorem does not hold