let A be Element of LTLB_WFF ; :: thesis: for i, j being Element of NAT

for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]

let i, j be Element of NAT ; :: thesis: for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]

let M be LTLModel; :: thesis: (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]

defpred S_{1}[ Element of LTLB_WFF ] means for k being Element of NAT holds (SAT (M ^\ i)) . [k,$1] = (SAT M) . [(i + k),$1];

A1: for n being Element of NAT holds S_{1}[ prop n]
_{1}[r] & S_{1}[s] holds

( S_{1}[r 'U' s] & S_{1}[r => s] )
_{1}[ TFALSUM ]
;

for r being Element of LTLB_WFF holds S_{1}[r]
from HILBERT2:sch 2(A18, A1, A6);

hence (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A] ; :: thesis: verum

for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]

let i, j be Element of NAT ; :: thesis: for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]

let M be LTLModel; :: thesis: (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]

defpred S

A1: for n being Element of NAT holds S

proof

A6:
for r, s being Element of LTLB_WFF st S
let n, k be Element of NAT ; :: thesis: (SAT (M ^\ i)) . [k,(prop n)] = (SAT M) . [(i + k),(prop n)]

end;per cases
( prop n in (M ^\ i) . k or not prop n in (M ^\ i) . k )
;

end;

suppose A2:
prop n in (M ^\ i) . k
; :: thesis: (SAT (M ^\ i)) . [k,(prop n)] = (SAT M) . [(i + k),(prop n)]

then A3:
prop n in M . (i + k)
by NAT_1:def 3;

thus (SAT (M ^\ i)) . [k,(prop n)] = 1 by A2, Def11

.= (SAT M) . [(i + k),(prop n)] by A3, Def11 ; :: thesis: verum

end;thus (SAT (M ^\ i)) . [k,(prop n)] = 1 by A2, Def11

.= (SAT M) . [(i + k),(prop n)] by A3, Def11 ; :: thesis: verum

suppose A4:
not prop n in (M ^\ i) . k
; :: thesis: (SAT (M ^\ i)) . [k,(prop n)] = (SAT M) . [(i + k),(prop n)]

then
not prop n in M . (i + k)
by NAT_1:def 3;

then A5: not (SAT M) . [(i + k),(prop n)] = 1 by Def11;

not (SAT (M ^\ i)) . [k,(prop n)] = 1 by A4, Def11;

hence (SAT (M ^\ i)) . [k,(prop n)] = 0 by XBOOLEAN:def 3

.= (SAT M) . [(i + k),(prop n)] by A5, XBOOLEAN:def 3 ;

:: thesis: verum

end;then A5: not (SAT M) . [(i + k),(prop n)] = 1 by Def11;

not (SAT (M ^\ i)) . [k,(prop n)] = 1 by A4, Def11;

hence (SAT (M ^\ i)) . [k,(prop n)] = 0 by XBOOLEAN:def 3

.= (SAT M) . [(i + k),(prop n)] by A5, XBOOLEAN:def 3 ;

:: thesis: verum

( S

proof

let r, s be Element of LTLB_WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r 'U' s] & S_{1}[r => s] ) )

assume that

A7: S_{1}[r]
and

A8: S_{1}[s]
; :: thesis: ( S_{1}[r 'U' s] & S_{1}[r => s] )

thus S_{1}[r 'U' s]
:: thesis: S_{1}[r => s]_{1}[r => s]
:: thesis: verum

end;assume that

A7: S

A8: S

thus S

proof

thus
S
let k be Element of NAT ; :: thesis: (SAT (M ^\ i)) . [k,(r 'U' s)] = (SAT M) . [(i + k),(r 'U' s)]

A9: ( (SAT (M ^\ i)) . [k,(r 'U' s)] = 1 iff (SAT M) . [(i + k),(r 'U' s)] = 1 )

end;A9: ( (SAT (M ^\ i)) . [k,(r 'U' s)] = 1 iff (SAT M) . [(i + k),(r 'U' s)] = 1 )

proof

then consider m being Element of NAT such that

A14: 0 < m and

A15: (SAT M) . [((i + k) + m),s] = 1 and

A16: for j being Element of NAT st 1 <= j & j < m holds

(SAT M) . [((i + k) + j),r] = 1 by Def11;

then (SAT (M ^\ i)) . [(k + m),s] = 1 by A8;

hence (SAT (M ^\ i)) . [k,(r 'U' s)] = 1 by A14, A17, Def11; :: thesis: verum

end;

hereby :: thesis: ( (SAT M) . [(i + k),(r 'U' s)] = 1 implies (SAT (M ^\ i)) . [k,(r 'U' s)] = 1 )

assume
(SAT M) . [(i + k),(r 'U' s)] = 1
; :: thesis: (SAT (M ^\ i)) . [k,(r 'U' s)] = 1assume
(SAT (M ^\ i)) . [k,(r 'U' s)] = 1
; :: thesis: (SAT M) . [(i + k),(r 'U' s)] = 1

then consider m being Element of NAT such that

A10: 0 < m and

A11: (SAT (M ^\ i)) . [(k + m),s] = 1 and

A12: for j being Element of NAT st 1 <= j & j < m holds

(SAT (M ^\ i)) . [(k + j),r] = 1 by Def11;

then (SAT M) . [((i + k) + m),s] = 1 ;

hence (SAT M) . [(i + k),(r 'U' s)] = 1 by A10, A13, Def11; :: thesis: verum

end;then consider m being Element of NAT such that

A10: 0 < m and

A11: (SAT (M ^\ i)) . [(k + m),s] = 1 and

A12: for j being Element of NAT st 1 <= j & j < m holds

(SAT (M ^\ i)) . [(k + j),r] = 1 by Def11;

A13: now :: thesis: for j being Element of NAT st 1 <= j & j < m holds

(SAT M) . [((i + k) + j),r] = 1

(SAT M) . [(i + (k + m)),s] = 1
by A8, A11;(SAT M) . [((i + k) + j),r] = 1

let j be Element of NAT ; :: thesis: ( 1 <= j & j < m implies (SAT M) . [((i + k) + j),r] = 1 )

assume ( 1 <= j & j < m ) ; :: thesis: (SAT M) . [((i + k) + j),r] = 1

then (SAT (M ^\ i)) . [(k + j),r] = 1 by A12;

then (SAT M) . [(i + (k + j)),r] = 1 by A7;

hence (SAT M) . [((i + k) + j),r] = 1 ; :: thesis: verum

end;assume ( 1 <= j & j < m ) ; :: thesis: (SAT M) . [((i + k) + j),r] = 1

then (SAT (M ^\ i)) . [(k + j),r] = 1 by A12;

then (SAT M) . [(i + (k + j)),r] = 1 by A7;

hence (SAT M) . [((i + k) + j),r] = 1 ; :: thesis: verum

then (SAT M) . [((i + k) + m),s] = 1 ;

hence (SAT M) . [(i + k),(r 'U' s)] = 1 by A10, A13, Def11; :: thesis: verum

then consider m being Element of NAT such that

A14: 0 < m and

A15: (SAT M) . [((i + k) + m),s] = 1 and

A16: for j being Element of NAT st 1 <= j & j < m holds

(SAT M) . [((i + k) + j),r] = 1 by Def11;

A17: now :: thesis: for j being Element of NAT st 1 <= j & j < m holds

(SAT (M ^\ i)) . [(k + j),r] = 1

(SAT M) . [(i + (k + m)),s] = 1
by A15;(SAT (M ^\ i)) . [(k + j),r] = 1

let j be Element of NAT ; :: thesis: ( 1 <= j & j < m implies (SAT (M ^\ i)) . [(k + j),r] = 1 )

assume ( 1 <= j & j < m ) ; :: thesis: (SAT (M ^\ i)) . [(k + j),r] = 1

then (SAT M) . [((i + k) + j),r] = 1 by A16;

then (SAT M) . [(i + (k + j)),r] = 1 ;

hence (SAT (M ^\ i)) . [(k + j),r] = 1 by A7; :: thesis: verum

end;assume ( 1 <= j & j < m ) ; :: thesis: (SAT (M ^\ i)) . [(k + j),r] = 1

then (SAT M) . [((i + k) + j),r] = 1 by A16;

then (SAT M) . [(i + (k + j)),r] = 1 ;

hence (SAT (M ^\ i)) . [(k + j),r] = 1 by A7; :: thesis: verum

then (SAT (M ^\ i)) . [(k + m),s] = 1 by A8;

hence (SAT (M ^\ i)) . [k,(r 'U' s)] = 1 by A14, A17, Def11; :: thesis: verum

proof

let k be Element of NAT ; :: thesis: (SAT (M ^\ i)) . [k,(r => s)] = (SAT M) . [(i + k),(r => s)]

thus (SAT (M ^\ i)) . [k,(r => s)] = ((SAT (M ^\ i)) . [k,r]) => ((SAT (M ^\ i)) . [k,s]) by Def11

.= ((SAT M) . [(i + k),r]) => ((SAT (M ^\ i)) . [k,s]) by A7

.= ((SAT M) . [(i + k),r]) => ((SAT M) . [(i + k),s]) by A8

.= (SAT M) . [(i + k),(r => s)] by Def11 ; :: thesis: verum

end;thus (SAT (M ^\ i)) . [k,(r => s)] = ((SAT (M ^\ i)) . [k,r]) => ((SAT (M ^\ i)) . [k,s]) by Def11

.= ((SAT M) . [(i + k),r]) => ((SAT (M ^\ i)) . [k,s]) by A7

.= ((SAT M) . [(i + k),r]) => ((SAT M) . [(i + k),s]) by A8

.= (SAT M) . [(i + k),(r => s)] by Def11 ; :: thesis: verum

now :: thesis: for k being Element of NAT holds (SAT (M ^\ i)) . [k,TFALSUM] = (SAT M) . [(i + k),TFALSUM]

then A18:
Slet k be Element of NAT ; :: thesis: (SAT (M ^\ i)) . [k,TFALSUM] = (SAT M) . [(i + k),TFALSUM]

thus (SAT (M ^\ i)) . [k,TFALSUM] = 0 by Def11

.= (SAT M) . [(i + k),TFALSUM] by Def11 ; :: thesis: verum

end;thus (SAT (M ^\ i)) . [k,TFALSUM] = 0 by Def11

.= (SAT M) . [(i + k),TFALSUM] by Def11 ; :: thesis: verum

for r being Element of LTLB_WFF holds S

hence (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A] ; :: thesis: verum