let A be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
let M be LTLModel; :: thesis: (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
set f = TFALSUM ;
set sm = SAT M;
per cases ( (SAT M) . [n,(TFALSUM 'U' A)] = 1 or (SAT M) . [n,(TFALSUM 'U' A)] = 0 ) by XBOOLEAN:def 3;
suppose A1: (SAT M) . [n,(TFALSUM 'U' A)] = 1 ; :: thesis: (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
then consider i being Element of NAT such that
A2: ( 0 < i & (SAT M) . [(n + i),A] = 1 ) and
A3: for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [(n + j),TFALSUM] = 1 by Def11;
now :: thesis: not 1 < i
assume A4: 1 < i ; :: thesis: contradiction
not (SAT M) . [(n + 1),TFALSUM] = 1 by Def11;
hence contradiction by A3, A4; :: thesis: verum
end;
hence (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A] by A1, A2, NAT_1:25; :: thesis: verum
end;
suppose A5: (SAT M) . [n,(TFALSUM 'U' A)] = 0 ; :: thesis: (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
now :: thesis: not (SAT M) . [(n + 1),A] = 1
assume A6: (SAT M) . [(n + 1),A] = 1 ; :: thesis: contradiction
( not 0 < 1 or not (SAT M) . [(n + 1),A] = 1 or ex j being Element of NAT st
( 1 <= j & j < 1 & not (SAT M) . [(n + j),TFALSUM] = 1 ) ) by A5, Def11;
hence contradiction by A6; :: thesis: verum
end;
hence (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A] by A5, XBOOLEAN:def 3; :: thesis: verum
end;
end;