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 b₁,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 holds (\false T) value_at (C,s) = FALSE
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 holds (\false T) value_at (C,s) = FALSE
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 holds (\false T) value_at (C,s) = FALSE
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 holds (\false T) value_at (C,s) = FALSE
let G be basic GeneratorSystem over S,X,T; :: thesis: for s being Element of C -States the generators of G holds (\false T) value_at (C,s) = FALSE
let s be Element of C -States the generators of G; :: thesis: (\false T) value_at (C,s) = FALSE
thus (\false T) value_at (C,s) = \not ((\true T) value_at (C,s)) by Th31
.= 'not' ((\true T) value_at (C,s)) by AOFA_A00:def 32
.= 'not' TRUE by Th30
.= FALSE ; :: thesis: verum