let A be Element of LTLB_WFF ; :: thesis: for n being Element of NAT

for M being LTLModel holds

( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )

let n be Element of NAT ; :: thesis: for M being LTLModel holds

( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )

let M be LTLModel; :: thesis: ( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )

set f = TFALSUM ;

set t = TVERUM ;

set sm = SAT M;

for M being LTLModel holds

( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )

let n be Element of NAT ; :: thesis: for M being LTLModel holds

( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )

let M be LTLModel; :: thesis: ( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )

set f = TFALSUM ;

set t = TVERUM ;

set sm = SAT M;

hereby :: thesis: ( ( for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 ) implies (SAT M) . [n,('G' A)] = 1 )

assume A4:
for i being Element of NAT holds (SAT M) . [(n + i),A] = 1
; :: thesis: (SAT M) . [n,('G' A)] = 1assume
(SAT M) . [n,('G' A)] = 1
; :: thesis: for i being Element of NAT holds (SAT M) . [(n + b_{2}),A] = 1

then A1: (SAT M) . [n,(('not' A) 'or' (TVERUM 'U' ('not' A)))] = 0 by Th5;

then A2: not (SAT M) . [n,('not' A)] = 1 by Th8;

let i be Element of NAT ; :: thesis: (SAT M) . [(n + b_{1}),A] = 1

A3: ( not (SAT M) . [n,TVERUM] = 1 or not (SAT M) . [n,(TVERUM 'U' ('not' A))] = 1 ) by A1, Th8;

end;then A1: (SAT M) . [n,(('not' A) 'or' (TVERUM 'U' ('not' A)))] = 0 by Th5;

then A2: not (SAT M) . [n,('not' A)] = 1 by Th8;

let i be Element of NAT ; :: thesis: (SAT M) . [(n + b

A3: ( not (SAT M) . [n,TVERUM] = 1 or not (SAT M) . [n,(TVERUM 'U' ('not' A))] = 1 ) by A1, Th8;

now :: thesis: not (SAT M) . [n,('G' A)] = 0

hence
(SAT M) . [n,('G' A)] = 1
by XBOOLEAN:def 3; :: thesis: verumassume
(SAT M) . [n,('G' A)] = 0
; :: thesis: contradiction

then not (SAT M) . [n,(('not' A) 'or' (TVERUM 'U' ('not' A)))] = 0 by Th5;

end;then not (SAT M) . [n,(('not' A) 'or' (TVERUM 'U' ('not' A)))] = 0 by Th5;

per cases then
( (SAT M) . [n,('not' A)] = 1 or (SAT M) . [n,(TVERUM 'U' ('not' A))] = 1 )
by Th8, XBOOLEAN:def 3;

end;

suppose
(SAT M) . [n,(TVERUM 'U' ('not' A))] = 1
; :: thesis: contradiction

then consider i being Element of NAT such that

0 < i and

A5: (SAT M) . [(n + i),('not' A)] = 1 and

for j being Element of NAT st 1 <= j & j < i holds

(SAT M) . [(n + j),TVERUM] = 1 by Def11;

(SAT M) . [(n + i),A] = 0 by A5, Th5;

hence contradiction by A4; :: thesis: verum

end;0 < i and

A5: (SAT M) . [(n + i),('not' A)] = 1 and

for j being Element of NAT st 1 <= j & j < i holds

(SAT M) . [(n + j),TVERUM] = 1 by Def11;

(SAT M) . [(n + i),A] = 0 by A5, Th5;

hence contradiction by A4; :: thesis: verum