let x, y, c be non pair set ; :: thesis: for s being State of (BitAdderWithOverflowCirc x,y,c) holds Following s,2 is stable
set S = BitAdderWithOverflowStr x,y,c;
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 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 ( 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;
then A1: ( 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' ) & 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 Th30, Th31;
Following s1,2 is stable by Th63;
then A2: Following s1,2 = Following (Following s1,2) by CIRCUIT2:def 6
.= Following s1,(2 + 1) by Th12 ;
Following s2,2 is stable by Th84;
then A3: Following s2,2 = Following (Following s2,2) by CIRCUIT2:def 6
.= Following s2,(2 + 1) by Th12 ;
A4: Following s,(2 + 1) = Following (Following s,2) by Th12;
A5: ( dom (Following s,2) = the carrier of (BitAdderWithOverflowStr x,y,c) & dom (Following s,3) = the carrier of (BitAdderWithOverflowStr x,y,c) & 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:4;
A6: 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;

now

let a be set ; :: 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 A6, 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 A1, A2, A3, A5, FUNCT_1:70;
hence (Following s,2) . a = (Following (Following s,2)) . a by A2, A3, Th12; :: thesis: verum

end;

hence Following s,2 = Following (Following s,2) by A4, A5, FUNCT_1:9; :: according to CIRCUIT2:def 6 :: thesis: verum