let x, y, c be non pair object ; :: thesis: for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable

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: Following (s,2) is stable

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

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

set S = BitAdderWithOverflowStr (x,y,c);

A1: dom (Following (s,3)) = the carrier of (BitAdderWithOverflowStr (x,y,c)) by CIRCUIT1:3;

A2: the carrier of (BitAdderWithOverflowStr (x,y,c)) = the carrier of (2GatesCircStr (x,y,c,'xor')) \/ the carrier of (MajorityStr (x,y,c)) by CIRCCOMB:def 2;

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 A3: ( Following (s1,2) = (Following (t,2)) | the carrier of (2GatesCircStr (x,y,c,'xor')) & Following (s1,3) = (Following (t,3)) | the carrier of (2GatesCircStr (x,y,c,'xor')) ) by Th30;

Following (s1,2) is stable by Th63;

then A4: Following (s1,2) = Following (Following (s1,2))

.= Following (s1,(2 + 1)) by Th12 ;

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 A5: ( Following (s2,2) = (Following (t,2)) | the carrier of (MajorityStr (x,y,c)) & Following (s2,3) = (Following (t,3)) | the carrier of (MajorityStr (x,y,c)) ) by Th31;

Following (s2,2) is stable by Th84;

then A6: Following (s2,2) = Following (Following (s2,2))

.= Following (s2,(2 + 1)) by Th12 ;

A7: ( dom (Following (s1,2)) = the carrier of (2GatesCircStr (x,y,c,'xor')) & dom (Following (s2,2)) = the carrier of (MajorityStr (x,y,c)) ) by CIRCUIT1:3;

hence Following (s,2) = Following (Following (s,2)) by A1, A8, FUNCT_1:2; :: according to CIRCUIT2:def 6 :: thesis: verum

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: Following (s,2) is stable

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

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

set S = BitAdderWithOverflowStr (x,y,c);

A1: dom (Following (s,3)) = the carrier of (BitAdderWithOverflowStr (x,y,c)) by CIRCUIT1:3;

A2: the carrier of (BitAdderWithOverflowStr (x,y,c)) = the carrier of (2GatesCircStr (x,y,c,'xor')) \/ the carrier of (MajorityStr (x,y,c)) by CIRCCOMB:def 2;

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 A3: ( Following (s1,2) = (Following (t,2)) | the carrier of (2GatesCircStr (x,y,c,'xor')) & Following (s1,3) = (Following (t,3)) | the carrier of (2GatesCircStr (x,y,c,'xor')) ) by Th30;

Following (s1,2) is stable by Th63;

then A4: Following (s1,2) = Following (Following (s1,2))

.= Following (s1,(2 + 1)) by Th12 ;

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 A5: ( Following (s2,2) = (Following (t,2)) | the carrier of (MajorityStr (x,y,c)) & Following (s2,3) = (Following (t,3)) | the carrier of (MajorityStr (x,y,c)) ) by Th31;

Following (s2,2) is stable by Th84;

then A6: Following (s2,2) = Following (Following (s2,2))

.= Following (s2,(2 + 1)) by Th12 ;

A7: ( dom (Following (s1,2)) = the carrier of (2GatesCircStr (x,y,c,'xor')) & dom (Following (s2,2)) = the carrier of (MajorityStr (x,y,c)) ) by CIRCUIT1:3;

A8: now :: thesis: for a being object st a in the carrier of (BitAdderWithOverflowStr (x,y,c)) holds

(Following (s,2)) . a = (Following (Following (s,2))) . a

( Following (s,(2 + 1)) = Following (Following (s,2)) & dom (Following (s,2)) = the carrier of (BitAdderWithOverflowStr (x,y,c)) )
by Th12, CIRCUIT1:3;(Following (s,2)) . a = (Following (Following (s,2))) . a

let a be object ; :: thesis: ( a in the carrier of (BitAdderWithOverflowStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )

assume a in the carrier of (BitAdderWithOverflowStr (x,y,c)) ; :: thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a

then ( a in the carrier of (2GatesCircStr (x,y,c,'xor')) or a in the carrier of (MajorityStr (x,y,c)) ) by A2, XBOOLE_0:def 3;

then ( ( (Following (s,2)) . a = (Following (s1,2)) . a & (Following (s,3)) . a = (Following (s1,3)) . a ) or ( (Following (s,2)) . a = (Following (s2,2)) . a & (Following (s,3)) . a = (Following (s2,3)) . a ) ) by A3, A5, A4, A6, A7, FUNCT_1:47;

hence (Following (s,2)) . a = (Following (Following (s,2))) . a by A4, A6, Th12; :: thesis: verum

end;assume a in the carrier of (BitAdderWithOverflowStr (x,y,c)) ; :: thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a

then ( a in the carrier of (2GatesCircStr (x,y,c,'xor')) or a in the carrier of (MajorityStr (x,y,c)) ) by A2, XBOOLE_0:def 3;

then ( ( (Following (s,2)) . a = (Following (s1,2)) . a & (Following (s,3)) . a = (Following (s1,3)) . a ) or ( (Following (s,2)) . a = (Following (s2,2)) . a & (Following (s,3)) . a = (Following (s2,3)) . a ) ) by A3, A5, A4, A6, A7, FUNCT_1:47;

hence (Following (s,2)) . a = (Following (Following (s,2))) . a by A4, A6, Th12; :: thesis: verum

hence Following (s,2) = Following (Following (s,2)) by A1, A8, FUNCT_1:2; :: according to CIRCUIT2:def 6 :: thesis: verum