:: deftheorem defines impg LTLAXIO2:def 3 :
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₃ = impg (f,A) iff ( len b₃ = len f & b₃ . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₃ . (i + 1) = ('G' (f /. (i + 1))) => (b₃ /. i) ) ) ) ) & ( not len f > 0 implies ( b₃ = impg (f,A) iff b₃ = <*> LTLB_WFF ) ) );