let x, b be non pair set ; :: thesis: for s being State of (IncrementCirc x,b)
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . b holds
( (Following s) . (IncrementOutput x,b) = ('not' a1) '&' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
let s be State of (IncrementCirc x,b); :: thesis: for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . b holds
( (Following s) . (IncrementOutput x,b) = ('not' a1) '&' 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) . (IncrementOutput x,b) = ('not' a1) '&' a2 & (Following s) . x = a1 & (Following s) . b = a2 ) )
assume A1: ( a1 = s . x & a2 = s . b ) ; :: thesis: ( (Following s) . (IncrementOutput x,b) = ('not' a1) '&' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
thus (Following s) . (IncrementOutput x,b) = and2a . <*(s . x),(s . b)*> by Th58
.= ('not' a1) '&' a2 by A1, Def2 ; :: thesis: ( (Following s) . x = a1 & (Following s) . b = a2 )
thus ( (Following s) . x = a1 & (Following s) . b = a2 ) by A1, Th58; :: thesis: verum