:: deftheorem imps defines implications LTLAXIO5:def 12 :
for f being FinSequence of LTLB_WFF
for A being Element of LTLB_WFF
for b₃ being FinSequence of LTLB_WFF holds
( ( len f > 0 implies ( b₃ = implications (f,A) iff ( len b₃ = len f & b₃ . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₃ . (i + 1) = (f /. (i + 1)) => (b₃ /. i) ) ) ) ) & ( not len f > 0 implies ( b₃ = implications (f,A) iff b₃ = <*> LTLB_WFF ) ) );