let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being V3() ManySortedSet of the carrier of S
for T being b1,S -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 a being boolean object
for t being Element of T, the bool-sort of S holds
( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )
let X be V3() ManySortedSet of the carrier of S; :: thesis: for T being X,S -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 a being boolean object
for t being Element of T, the bool-sort of S holds
( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: 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 a being boolean object
for t being Element of T, the bool-sort of S holds
( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G
for a being boolean object
for t being Element of T, the bool-sort of S holds
( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )
let G be basic GeneratorSystem over S,X,T; :: thesis: for s being Element of C -States the generators of G
for a being boolean object
for t being Element of T, the bool-sort of S holds
( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )
let s be Element of C -States the generators of G; :: thesis: for a being boolean object
for t being Element of T, the bool-sort of S holds
( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )
let a be boolean object ; :: thesis: for t being Element of T, the bool-sort of S holds
( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )
let t be Element of T, the bool-sort of S; :: thesis: ( (\not t) value_at (C,s) = 'not' a iff t value_at (C,s) = a )
hereby :: thesis: ( t value_at (C,s) = a implies (\not t) value_at (C,s) = 'not' a )
assume (\not t) value_at (C,s) = 'not' a ; :: thesis: t value_at (C,s) = a
then \not (t value_at (C,s)) = 'not' a by Th31;
then 'not' (t value_at (C,s)) = 'not' a by AOFA_A00:def 32;
hence t value_at (C,s) = a ; :: thesis: verum
end;
assume A1: t value_at (C,s) = a ; :: thesis: (\not t) value_at (C,s) = 'not' a
\not (t value_at (C,s)) = (\not t) value_at (C,s) by Th31;
hence (\not t) value_at (C,s) = 'not' a by A1, AOFA_A00:def 32; :: thesis: verum