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;

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;

end;

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;

end;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

hence
(SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
by A1, A2, NAT_1:25; :: thesis: verumassume A4:
1 < i
; :: thesis: contradiction

not (SAT M) . [(n + 1),TFALSUM] = 1 by Def11;

hence contradiction by A3, A4; :: thesis: verum

end;not (SAT M) . [(n + 1),TFALSUM] = 1 by Def11;

hence contradiction by A3, A4; :: thesis: verum

suppose A5:
(SAT M) . [n,(TFALSUM 'U' A)] = 0
; :: thesis: (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]

end;

now :: thesis: not (SAT M) . [(n + 1),A] = 1

hence
(SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
by A5, XBOOLEAN:def 3; :: thesis: verumassume 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;( 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