let x, b be non pair set ; :: thesis: for s being State of (CompCirc (x,b))
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . b holds
( (Following s) . (CompOutput (x,b)) = ('not' a1) 'xor' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
let s be State of (CompCirc (x,b)); :: thesis: for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . b holds
( (Following s) . (CompOutput (x,b)) = ('not' a1) 'xor' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
let a1, a2 be Element of BOOLEAN ; :: thesis: ( a1 = s . x & a2 = s . b implies ( (Following s) . (CompOutput (x,b)) = ('not' a1) 'xor' a2 & (Following s) . x = a1 & (Following s) . b = a2 ) )
assume A1: ( a1 = s . x & a2 = s . b ) ; :: thesis: ( (Following s) . (CompOutput (x,b)) = ('not' a1) 'xor' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
thus (Following s) . (CompOutput (x,b)) = xor2a . <*(s . x),(s . b)*> by Th43
.= ('not' a1) 'xor' a2 by A1, Def7 ; :: thesis: ( (Following s) . x = a1 & (Following s) . b = a2 )
thus ( (Following s) . x = a1 & (Following s) . b = a2 ) by A1, Th43; :: thesis: verum