let a, b be set ; :: thesis: for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitGFA1Str (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str (a,b,c)) & 1 -BitGFA1Circ (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ (a,b,c)) & 1 -BitGFA1CarryOutput (<*a*>,<*b*>) = GFA1CarryOutput (a,b,c) )
A1: <*a*> . 1 = a ;
<*b*> . 1 = b ;
hence for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitGFA1Str (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str (a,b,c)) & 1 -BitGFA1Circ (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ (a,b,c)) & 1 -BitGFA1CarryOutput (<*a*>,<*b*>) = GFA1CarryOutput (a,b,c) ) by A1, Th17; :: thesis: verum