let p, q be Element of LTLB_WFF ; for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
let n be Element of NAT ; for M being LTLModel holds
( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
let M be LTLModel; ( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
set sm = SAT M;
set notp = 'not' p;
set notq = 'not' q;
thus
( not (SAT M) . [n,(p 'R' q)] = 1 or ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 )
( ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) implies (SAT M) . [n,(p 'R' q)] = 1 )proof
defpred S1[
Nat]
means (
(SAT M) . [(n + $1),q] = 1 &
(SAT M) . [(n + $1),p] = 0 );
assume
(SAT M) . [n,(p 'R' q)] = 1
;
( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 )
then A1:
(SAT M) . [n,(('not' p) 'Uw' ('not' q))] = 0
by Th5;
assume that A3:
for
i being
Element of
NAT holds
( not
(SAT M) . [(n + i),p] = 1 or ex
j being
Element of
NAT st
(
j <= i & not
(SAT M) . [(n + j),q] = 1 ) )
and A4:
not for
i being
Element of
NAT holds
(SAT M) . [(n + i),q] = 1
;
contradiction
A6:
for
k being
Nat st ( for
m being
Nat st
m < k holds
S1[
m] ) holds
S1[
k]
for
i being
Nat holds
S1[
i]
from NAT_1:sch 4(A6);
hence
contradiction
by A4;
verum
end;
thus
( ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) implies (SAT M) . [n,(p 'R' q)] = 1 )
verum