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 S1[ 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 S1[ 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 S1[r] & S1[s] holds
( S1[r 'U' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r 'U' s] & S1[r => s] ) )
assume that
A7: S1[r] and
A8: S1[s] ; :: thesis: ( S1[r 'U' s] & S1[r => s] )
thus S1[r 'U' s] :: thesis: S1[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 S1[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: S1[ TFALSUM ] ;
for r being Element of LTLB_WFF holds S1[r] from HILBERT2:sch 2(A18, A1, A6);
 hence (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A] ; :: thesis: verum