let x, y, c be object ; ( c <> [<*x,y*>,'or'] implies for s being State of (2GatesCircuit (x,y,c,'or'))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3 )
set f = 'or' ;
assume A1:
c <> [<*x,y*>,'or']
; for s being State of (2GatesCircuit (x,y,c,'or'))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3
let s be State of (2GatesCircuit (x,y,c,'or')); for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3
let a1, a2, a3 be Element of BOOLEAN ; ( a1 = s . x & a2 = s . y & a3 = s . c implies (Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3 )
assume
( a1 = s . x & a2 = s . y & a3 = s . c )
; (Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3
hence (Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) =
'or' . <*('or' . <*a1,a2*>),a3*>
by A1, Th62
.=
'or' . <*(a1 'or' a2),a3*>
by Def4
.=
(a1 'or' a2) 'or' a3
by Def4
;
verum