let x, b be non pair set ; 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)); 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 ; ( 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 )
; ( (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 Th47
.=
('not' a1) '&' a2
by A1, Def1
; ( (Following s) . x = a1 & (Following s) . b = a2 )
thus
( (Following s) . x = a1 & (Following s) . b = a2 )
by A1, Th47; verum