let x, y, c be non pair object ; :: 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 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) )

reconsider t = s as State of ((BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c))) ;

reconsider s1 = s | the carrier of (2GatesCircStr (x,y,c,'xor')) as State of (BitAdderCirc (x,y,c)) by Th26;

set f = 'xor' ;

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 that

A1: a1 = s . x and

A2: a2 = s . y and

A3: 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) )

A4: dom s1 = the carrier of (2GatesCircStr (x,y,c,'xor')) by CIRCUIT1:3;

y in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;

then A5: a2 = s1 . y by A2, A4, FUNCT_1:47;

InputVertices (2GatesCircStr (x,y,c,'xor')) is without_pairs by Th59;

then InnerVertices (MajorityStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by Th5, Th67;

then A6: (Following (t,2)) . (2GatesCircOutput (x,y,c,'xor')) = (Following (s1,2)) . (2GatesCircOutput (x,y,c,'xor')) by Th32;

c in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;

then A7: a3 = s1 . c by A3, A4, FUNCT_1:47;

reconsider s2 = s | the carrier of (MajorityStr (x,y,c)) as State of (MajorityCirc (x,y,c)) by Th26;

A8: dom s2 = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;

x in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;

then a1 = s1 . x by A1, A4, FUNCT_1:47;

hence (Following (s,2)) . (BitAdderOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 by A5, A7, A6, Th64; :: thesis: (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)

InputVertices (MajorityStr (x,y,c)) is without_pairs by Th68;

then InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (MajorityStr (x,y,c)) by Th5, Th58;

then A9: (Following (t,2)) . (MajorityOutput (x,y,c)) = (Following (s2,2)) . (MajorityOutput (x,y,c)) by Th33;

c in the carrier of (MajorityStr (x,y,c)) by Th72;

then A10: a3 = s2 . c by A3, A8, FUNCT_1:47;

y in the carrier of (MajorityStr (x,y,c)) by Th72;

then A11: a2 = s2 . y by A2, A8, FUNCT_1:47;

x in the carrier of (MajorityStr (x,y,c)) by Th72;

then a1 = s2 . x by A1, A8, FUNCT_1:47;

hence (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) by A11, A10, A9, Lm3; :: thesis: verum

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 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) )

reconsider t = s as State of ((BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c))) ;

reconsider s1 = s | the carrier of (2GatesCircStr (x,y,c,'xor')) as State of (BitAdderCirc (x,y,c)) by Th26;

set f = 'xor' ;

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 that

A1: a1 = s . x and

A2: a2 = s . y and

A3: 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) )

A4: dom s1 = the carrier of (2GatesCircStr (x,y,c,'xor')) by CIRCUIT1:3;

y in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;

then A5: a2 = s1 . y by A2, A4, FUNCT_1:47;

InputVertices (2GatesCircStr (x,y,c,'xor')) is without_pairs by Th59;

then InnerVertices (MajorityStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by Th5, Th67;

then A6: (Following (t,2)) . (2GatesCircOutput (x,y,c,'xor')) = (Following (s1,2)) . (2GatesCircOutput (x,y,c,'xor')) by Th32;

c in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;

then A7: a3 = s1 . c by A3, A4, FUNCT_1:47;

reconsider s2 = s | the carrier of (MajorityStr (x,y,c)) as State of (MajorityCirc (x,y,c)) by Th26;

A8: dom s2 = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;

x in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;

then a1 = s1 . x by A1, A4, FUNCT_1:47;

hence (Following (s,2)) . (BitAdderOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 by A5, A7, A6, Th64; :: thesis: (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)

InputVertices (MajorityStr (x,y,c)) is without_pairs by Th68;

then InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (MajorityStr (x,y,c)) by Th5, Th58;

then A9: (Following (t,2)) . (MajorityOutput (x,y,c)) = (Following (s2,2)) . (MajorityOutput (x,y,c)) by Th33;

c in the carrier of (MajorityStr (x,y,c)) by Th72;

then A10: a3 = s2 . c by A3, A8, FUNCT_1:47;

y in the carrier of (MajorityStr (x,y,c)) by Th72;

then A11: a2 = s2 . y by A2, A8, FUNCT_1:47;

x in the carrier of (MajorityStr (x,y,c)) by Th72;

then a1 = s2 . x by A1, A8, FUNCT_1:47;

hence (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) by A11, A10, A9, Lm3; :: thesis: verum