:: deftheorem Def11 defines SAT LTLAXIO1:def 11 :
for M being LTLModel
for b₂ being Function of [:NAT,LTLB_WFF:],BOOLEAN holds
( b₂ = SAT M iff for n being Element of NAT holds
( b₂ . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b₂ . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b₂ . [n,(p => q)] = (b₂ . [n,p]) => (b₂ . [n,q]) & ( b₂ . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b₂ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₂ . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b₂ . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b₂ . [(n + j),p] = 1 ) ) implies b₂ . [n,(p 'U' q)] = 1 ) ) ) ) );