let x, y, z be set ; for s being State of (GFA0CarryCirc (x,y,z))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2] & a2 = s . [<*y,z*>,and2] & a3 = s . [<*z,x*>,and2] holds
(Following s) . (GFA0CarryOutput (x,y,z)) = (a1 'or' a2) 'or' a3
set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f4 = or3 ;
let s be State of (GFA0CarryCirc (x,y,z)); for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2] & a2 = s . [<*y,z*>,and2] & a3 = s . [<*z,x*>,and2] holds
(Following s) . (GFA0CarryOutput (x,y,z)) = (a1 'or' a2) 'or' a3
set xy = [<*x,y*>,and2];
set yz = [<*y,z*>,and2];
set zx = [<*z,x*>,and2];
let a1, a2, a3 be Element of BOOLEAN ; ( a1 = s . [<*x,y*>,and2] & a2 = s . [<*y,z*>,and2] & a3 = s . [<*z,x*>,and2] implies (Following s) . (GFA0CarryOutput (x,y,z)) = (a1 'or' a2) 'or' a3 )
assume A1:
( a1 = s . [<*x,y*>,and2] & a2 = s . [<*y,z*>,and2] & a3 = s . [<*z,x*>,and2] )
; (Following s) . (GFA0CarryOutput (x,y,z)) = (a1 'or' a2) 'or' a3
set S = GFA0CarryStr (x,y,z);
reconsider xy = [<*x,y*>,and2], yz = [<*y,z*>,and2], zx = [<*z,x*>,and2] as Element of InnerVertices (GFA0CarryStr (x,y,z)) by Th17;
A2:
dom s = the carrier of (GFA0CarryStr (x,y,z))
by CIRCUIT1:3;
InnerVertices (GFA0CarryStr (x,y,z)) = the carrier' of (GFA0CarryStr (x,y,z))
by FACIRC_1:37;
hence (Following s) . (GFA0CarryOutput (x,y,z)) =
or3 . (s * <*xy,yz,zx*>)
by FACIRC_1:35
.=
or3 . <*a1,a2,a3*>
by A1, A2, FINSEQ_2:126
.=
(a1 'or' a2) 'or' a3
by TWOSCOMP:14
;
verum