:: deftheorem Def6 defines Reduction HALLMAR1:def 6 :
for F being set
for A, b₃ being FinSequence of bool F holds
( b₃ is Reduction of A iff ( dom b₃ = dom A & ( for i being Element of NAT st i in dom A holds
b₃ . i c= A . i ) ) );