let p, q be Element of LTLB_WFF ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( (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 ) :: thesis: ( ( 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 ; :: thesis: ( 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;
A2: now :: thesis: for i being Nat holds
( not (SAT M) . [(n + i),('not' q)] = 1 or ex j being Nat st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) )
let i be Nat; :: thesis: ( not (SAT M) . [(n + b1),('not' q)] = 1 or ex j being Nat st
( b2 < j & not (SAT M) . [(n + b2),('not' p)] = 1 ) )
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
per cases ( not (SAT M) . [(n + ii),('not' q)] = 1 or ex j being Element of NAT st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) by A1, Th12;
suppose not (SAT M) . [(n + ii),('not' q)] = 1 ; :: thesis: ( not (SAT M) . [(n + b1),('not' q)] = 1 or ex j being Nat st
( b2 < j & not (SAT M) . [(n + b2),('not' p)] = 1 ) )
hence ( not (SAT M) . [(n + i),('not' q)] = 1 or ex j being Nat st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) ; :: thesis: verum
end;
suppose ex j being Element of NAT st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ; :: thesis: ( not (SAT M) . [(n + b1),('not' q)] = 1 or ex j being Nat st
( b2 < j & not (SAT M) . [(n + b2),('not' p)] = 1 ) )
hence ( not (SAT M) . [(n + i),('not' q)] = 1 or ex j being Nat st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) ; :: thesis: verum
end;
end;
end;
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 ; :: thesis: contradiction
A5: now :: thesis: for i being Nat holds
( not (SAT M) . [(n + i),p] = 1 or ex j being Nat st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) )
let i be Nat; :: thesis: ( not (SAT M) . [(n + i),p] = 1 or ex j being Nat st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) )
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
( not (SAT M) . [(n + ii),p] = 1 or ex j being Element of NAT st
( j <= ii & not (SAT M) . [(n + j),q] = 1 ) ) by A3;
hence ( not (SAT M) . [(n + i),p] = 1 or ex j being Nat st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) ) ; :: thesis: verum
end;
A6: for k being Nat st ( for m being Nat st m < k holds
S1[m] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( ( for m being Nat st m < k holds
S1[m] ) implies S1[k] )
assume A7: for m being Nat st m < k holds
S1[m] ; :: thesis: S1[k]
reconsider nk = n + k as Element of NAT by ORDINAL1:def 12;
now :: thesis: for j being Nat holds
( not j < k or (SAT M) . [(n + j),('not' p)] = 1 )
assume ex j being Nat st
( j < k & not (SAT M) . [(n + j),('not' p)] = 1 ) ; :: thesis: contradiction
then consider j being Nat such that
A8: j < k and
A9: not (SAT M) . [(n + j),('not' p)] = 1 ;
reconsider nj = n + j as Element of NAT by ORDINAL1:def 12;
not (SAT M) . [nj,p] = 0 by A9, Th5;
hence contradiction by A7, A8; :: thesis: verum
end;
then not (SAT M) . [(n + k),('not' q)] = 1 by A2;
then not (SAT M) . [nk,q] = 0 by Th5;
then A10: (SAT M) . [(n + k),q] = 1 by XBOOLEAN:def 3;
now :: thesis: for j being Nat holds
( not j <= k or (SAT M) . [(n + j),q] = 1 )
assume ex j being Nat st
( j <= k & not (SAT M) . [(n + j),q] = 1 ) ; :: thesis: contradiction
then consider j being Nat such that
A11: j <= k and
A12: not (SAT M) . [(n + j),q] = 1 ;
end;
hence S1[k] by XBOOLEAN:def 3, A5; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 4(A6);
 hence contradiction by A4; :: thesis: 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 ) :: thesis: verum
proof
assume A13: ( 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 ) ; :: thesis: (SAT M) . [n,(p 'R' q)] = 1
assume not (SAT M) . [n,(p 'R' q)] = 1 ; :: thesis: contradiction
then A14: (SAT M) . [n,(('not' p) 'Uw' ('not' q))] = 1 by XBOOLEAN:def 3, Th5;
per cases ( 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 ) by A13;
suppose 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 ) ) ; :: thesis: contradiction
then consider i being Element of NAT such that
A15: (SAT M) . [(n + i),p] = 1 and
A16: for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ;
consider k being Element of NAT such that
A17: (SAT M) . [(n + k),('not' q)] = 1 and
A18: for j being Element of NAT st j < k holds
(SAT M) . [(n + j),('not' p)] = 1 by A14, Th12;
per cases ( k <= i or not k <= i ) ;
suppose k <= i ; :: thesis: contradiction
then (SAT M) . [(n + k),q] = 1 by A16;
hence contradiction by A17, Th5; :: thesis: verum
end;
suppose not k <= i ; :: thesis: contradiction
then (SAT M) . [(n + i),('not' p)] = 1 by A18;
hence contradiction by A15, Th5; :: thesis: verum
end;
end;
end;
suppose A19: for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ; :: thesis: contradiction
consider i being Element of NAT such that
A20: (SAT M) . [(n + i),('not' q)] = 1 and
for j being Element of NAT st j < i holds
(SAT M) . [(n + j),('not' p)] = 1 by A14, Th12;
(SAT M) . [(n + i),q] = 0 by A20, Th5;
hence contradiction by A19; :: thesis: verum
end;
end;
end;