theorem Th31: :: AOFA_A01:31

for S being non empty non void bool-correct 4,1 integer BoolSignature
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G
for t being Element of T, the bool-sort of S holds (\not t) value_at (C,s) = \not (t value_at (C,s))