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₁[ 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₁[ prop n]

proof

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

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

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;

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;

end;

end;

A6: for r, s being Element of LTLB_WFF st S₁[r] & S₁[s] holds
( S₁[r 'U' s] & S₁[r => s] )

proof

let r, s be Element of LTLB_WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r 'U' s] & S₁[r => s] ) )
assume that
A7: S₁[r] and
A8: S₁[s] ; :: thesis: ( S₁[r 'U' s] & S₁[r => s] )
thus S₁[r 'U' s] :: thesis: S₁[r => s]

proof

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 )

proof

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)] = 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;

A13: now :: thesis: for j being Element of NAT st 1 <= j & j < m holds
(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;

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

end;

assume (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
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

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;

(SAT M) . [(i + (k + m)),s] = 1 by A15;
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;

per cases ( (SAT (M ^\ i)) . [k,(r 'U' s)] = 1 or not (SAT (M ^\ i)) . [k,(r 'U' s)] = 1 ) ;

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

hence (SAT (M ^\ i)) . [k,(r 'U' s)] = (SAT M) . [(i + k),(r 'U' s)] by A9; :: thesis: verum

end;

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

then (SAT (M ^\ i)) . [k,(r 'U' s)] = 0 by XBOOLEAN:def 3;
hence (SAT (M ^\ i)) . [k,(r 'U' s)] = (SAT M) . [(i + k),(r 'U' s)] by A9, XBOOLEAN:def 3; :: thesis: verum

end;

end;

end;

thus S₁[r => s] :: 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;

end;

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

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

then A18: S₁[ TFALSUM ] ;
for r being Element of LTLB_WFF holds S₁[r] from HILBERT2:sch 2(A18, A1, A6);
hence (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A] ; :: thesis: verum