let x, y, c be set ; ( x <> [<*y,c*>,'&' ] & y <> [<*c,x*>,'&' ] & c <> [<*x,y*>,'&' ] & c <> [<*x,y*>,'xor' ] implies for s being State of (BitAdderWithOverflowCirc x,y,c)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s,2) . (BitAdderOutput x,y,c) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) ) )
assume that
A1:
x <> [<*y,c*>,'&' ]
and
A2:
y <> [<*c,x*>,'&' ]
and
A3:
c <> [<*x,y*>,'&' ]
and
A4:
c <> [<*x,y*>,'xor' ]
; for s being State of (BitAdderWithOverflowCirc x,y,c)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s,2) . (BitAdderOutput x,y,c) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )
set f = 'xor' ;
set S1 = 2GatesCircStr x,y,c,'xor' ;
set S2 = MajorityStr x,y,c;
set A = BitAdderWithOverflowCirc x,y,c;
set A1 = BitAdderCirc x,y,c;
set A2 = MajorityCirc x,y,c;
let s be State of (BitAdderWithOverflowCirc x,y,c); for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s,2) . (BitAdderOutput x,y,c) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )
let a1, a2, a3 be Element of BOOLEAN ; ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following s,2) . (BitAdderOutput x,y,c) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) ) )
assume that
A5:
a1 = s . x
and
A6:
a2 = s . y
and
A7:
a3 = s . c
; ( (Following s,2) . (BitAdderOutput x,y,c) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )
A8:
x in the carrier of (2GatesCircStr x,y,c,'xor' )
by FACIRC_1:60;
A9:
y in the carrier of (2GatesCircStr x,y,c,'xor' )
by FACIRC_1:60;
A10:
c in the carrier of (2GatesCircStr x,y,c,'xor' )
by FACIRC_1:60;
A11:
x in the carrier of (MajorityStr x,y,c)
by FACIRC_1:72;
A12:
y in the carrier of (MajorityStr x,y,c)
by FACIRC_1:72;
A13:
c in the carrier of (MajorityStr x,y,c)
by FACIRC_1:72;
reconsider s1 = s | the carrier of (2GatesCircStr x,y,c,'xor' ) as State of (BitAdderCirc x,y,c) by FACIRC_1:26;
reconsider s2 = s | the carrier of (MajorityStr x,y,c) as State of (MajorityCirc x,y,c) by FACIRC_1:26;
reconsider t = s as State of ((BitAdderCirc x,y,c) +* (MajorityCirc x,y,c)) ;
InputVertices (2GatesCircStr x,y,c,'xor' ) = {x,y,c}
by A4, FACIRC_1:57;
then A14:
InputVertices (2GatesCircStr x,y,c,'xor' ) = InputVertices (MajorityStr x,y,c)
by A1, A2, A3, Th21;
A15:
InnerVertices (2GatesCircStr x,y,c,'xor' ) misses InputVertices (2GatesCircStr x,y,c,'xor' )
by XBOOLE_1:79;
A16:
InnerVertices (MajorityStr x,y,c) misses InputVertices (MajorityStr x,y,c)
by XBOOLE_1:79;
A17:
dom s1 = the carrier of (2GatesCircStr x,y,c,'xor' )
by CIRCUIT1:4;
then A18:
a1 = s1 . x
by A5, A8, FUNCT_1:70;
A19:
a2 = s1 . y
by A6, A9, A17, FUNCT_1:70;
A20:
a3 = s1 . c
by A7, A10, A17, FUNCT_1:70;
(Following t,2) . (2GatesCircOutput x,y,c,'xor' ) = (Following s1,2) . (2GatesCircOutput x,y,c,'xor' )
by A14, A16, FACIRC_1:32;
hence
(Following s,2) . (BitAdderOutput x,y,c) = (a1 'xor' a2) 'xor' a3
by A4, A18, A19, A20, FACIRC_1:64; (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)
A21:
dom s2 = the carrier of (MajorityStr x,y,c)
by CIRCUIT1:4;
then A22:
a1 = s2 . x
by A5, A11, FUNCT_1:70;
A23:
a2 = s2 . y
by A6, A12, A21, FUNCT_1:70;
A24:
a3 = s2 . c
by A7, A13, A21, FUNCT_1:70;
(Following t,2) . (MajorityOutput x,y,c) = (Following s2,2) . (MajorityOutput x,y,c)
by A14, A15, FACIRC_1:33;
hence
(Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)
by A1, A2, A3, A22, A23, A24, Lm4; verum