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 + b2),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 + b1),A] = 1
A3: ( not (SAT M) . [n,TVERUM] = 1 or not (SAT M) . [n,(TVERUM 'U' ('not' A))] = 1 ) by A1, Th8;
per cases ( i = 0 or 0 < i ) ;
suppose i = 0 ; :: thesis: (SAT M) . [(n + b1),A] = 1
hence (SAT M) . [(n + i),A] = 1 by Th5, XBOOLEAN:def 3, A2; :: thesis: verum
end;
suppose 0 < i ; :: thesis: (SAT M) . [(n + b1),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, Def11, Th6;
hence (SAT M) . [(n + i),A] = 1 by XBOOLEAN:def 3, Th5, Th6; :: 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 :: thesis: not (SAT M) . [n,('G' A)] = 0
assume (SAT M) . [n,('G' A)] = 0 ; :: thesis: contradiction
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;
suppose (SAT M) . [n,('not' A)] = 1 ; :: thesis: contradiction
then (SAT M) . [(n + 0),A] = 0 by Th5;
hence contradiction by A4; :: thesis: verum
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;
end;
end;
hence (SAT M) . [n,('G' A)] = 1 by XBOOLEAN:def 3; :: thesis: verum