let x, b be non pair set ; :: thesis: for s being State of (BitCompCirc 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 (BitCompCirc 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 Th56
.= ('not' a1) 'xor' a2 by A1, Def14 ; :: thesis: ( (Following s) . x = a1 & (Following s) . b = a2 )
thus ( (Following s) . x = a1 & (Following s) . b = a2 ) by A1, Th56; :: thesis: verum