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;

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

assume (SAT M) . [n,('G' A)] = 1 ; :: thesis: for i being Element of NAT holds (SAT M) . [(n + b₂),A] = 1
then A1: (SAT M) . [n,(('not' A) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' A))))] = 0 by Th6;
then not (SAT M) . [n,('not' A)] = 1 by Th9;
then A2: not (SAT M) . [n,A] = 0 by Th6;
let i be Element of NAT ; :: thesis: (SAT M) . [(n + b₁),A] = 1
not (SAT M) . [n,(TVERUM '&&' (TVERUM 'Us' ('not' A)))] = 1 by A1, Th9;
then A3: ( not (SAT M) . [n,TVERUM] = 1 or not (SAT M) . [n,(TVERUM 'Us' ('not' A))] = 1 ) by Th8;

per cases ( i = 0 or 0 < i ) ;

suppose i = 0 ; :: thesis: (SAT M) . [(n + b₁),A] = 1

hence (SAT M) . [(n + i),A] = 1 by A2, XBOOLEAN:def 3; :: thesis: verum

end;

suppose 0 < i ; :: thesis: (SAT M) . [(n + b₁),A] = 1

then ( not (SAT M) . [(n + i),('not' A)] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not (SAT M) . [(n + j),TVERUM] = 1 ) ) by A3, Def12, Th7;
then not (SAT M) . [(n + i),A] = 0 by Th6, Th7;
hence (SAT M) . [(n + i),A] = 1 by XBOOLEAN:def 3; :: thesis: verum

end;

end;

end;

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

now

assume (SAT M) . [n,('G' A)] = 0 ; :: thesis: contradiction
then not (SAT M) . [n,(('not' A) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' A))))] = 0 by Th6;
then A5: (SAT M) . [n,(('not' A) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' A))))] = 1 by XBOOLEAN:def 3;

per cases ( (SAT M) . [n,('not' A)] = 1 or (SAT M) . [n,(TVERUM '&&' (TVERUM 'Us' ('not' A)))] = 1 ) by A5, Th9;

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

then (SAT M) . [(n + 0),A] = 0 by Th6;
hence contradiction by A4; :: thesis: verum

end;

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

then (SAT M) . [n,(TVERUM 'Us' ('not' A))] = 1 by Th8;
then consider i being Element of NAT such that
0 < i and
A6: (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 Def12;
(SAT M) . [(n + i),A] = 0 by A6, Th6;
hence contradiction by A4; :: thesis: verum

end;

end;

end;

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