let x, y, c be non pair set ; :: thesis: 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); :: thesis: 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 ; :: thesis: ( 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 A1: ( a1 = s . x & a2 = s . y & a3 = s . c ) ; :: thesis: ( (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) )
A2: ( x in the carrier of (2GatesCircStr x,y,c,'xor' ) & y in the carrier of (2GatesCircStr x,y,c,'xor' ) & c in the carrier of (2GatesCircStr x,y,c,'xor' ) ) by Th60;
A3: ( x in the carrier of (MajorityStr x,y,c) & y in the carrier of (MajorityStr x,y,c) & c in the carrier of (MajorityStr x,y,c) ) by Th72;
reconsider s1 = s | the carrier of (2GatesCircStr x,y,c,'xor' ) as State of (BitAdderCirc x,y,c) by Th26;
reconsider s2 = s | the carrier of (MajorityStr x,y,c) as State of (MajorityCirc x,y,c) by Th26;
reconsider t = s as State of ((BitAdderCirc x,y,c) +* (MajorityCirc x,y,c)) ;
( not InputVertices (2GatesCircStr x,y,c,'xor' ) is with_pair & InnerVertices (2GatesCircStr x,y,c,'xor' ) is Relation & not InputVertices (MajorityStr x,y,c) is with_pair & InnerVertices (MajorityStr x,y,c) is Relation ) by Th58, Th59, Th67, Th68;
then A4: ( InnerVertices (2GatesCircStr x,y,c,'xor' ) misses InputVertices (MajorityStr x,y,c) & InnerVertices (MajorityStr x,y,c) misses InputVertices (2GatesCircStr x,y,c,'xor' ) ) by Th5;
dom s1 = the carrier of (2GatesCircStr x,y,c,'xor' ) by CIRCUIT1:4;
then ( a1 = s1 . x & a2 = s1 . y & a3 = s1 . c ) by A1, A2, FUNCT_1:70;
then ( (Following t,2) . (2GatesCircOutput x,y,c,'xor' ) = (Following s1,2) . (2GatesCircOutput x,y,c,'xor' ) & (Following s1,2) . (2GatesCircOutput x,y,c,'xor' ) = (a1 'xor' a2) 'xor' a3 ) by A4, Th32, Th64;
hence (Following s,2) . (BitAdderOutput x,y,c) = (a1 'xor' a2) 'xor' a3 ; :: thesis: (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)
dom s2 = the carrier of (MajorityStr x,y,c) by CIRCUIT1:4;
then ( a1 = s2 . x & a2 = s2 . y & a3 = s2 . c ) by A1, A3, FUNCT_1:70;
then ( (Following t,2) . (MajorityOutput x,y,c) = (Following s2,2) . (MajorityOutput x,y,c) & (Following s2,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) ) by A4, Lm4, Th33;
hence (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) ; :: thesis: verum