let x, y, c be set ; :: thesis: ( x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] & c <> [<*x,y*>,'xor' ] implies for s being State of (BitSubtracterWithBorrowCirc x,y,c) holds Following s,2 is stable )
assume that
A1: x <> [<*y,c*>,and2 ] and
A2: y <> [<*x,c*>,and2a ] and
A3: c <> [<*x,y*>,and2a ] and
A4: c <> [<*x,y*>,'xor' ] ; :: thesis: for s being State of (BitSubtracterWithBorrowCirc x,y,c) holds Following s,2 is stable
set S = BitSubtracterWithBorrowStr x,y,c;
set S1 = 2GatesCircStr x,y,c,'xor' ;
set S2 = BorrowStr x,y,c;
set A = BitSubtracterWithBorrowCirc x,y,c;
set A1 = BitSubtracterCirc x,y,c;
set A2 = BorrowCirc x,y,c;
let s be State of (BitSubtracterWithBorrowCirc x,y,c); :: thesis: Following s,2 is stable
reconsider s1 = s | the carrier of (2GatesCircStr x,y,c,'xor' ) as State of (BitSubtracterCirc x,y,c) by FACIRC_1:26;
reconsider s2 = s | the carrier of (BorrowStr x,y,c) as State of (BorrowCirc x,y,c) by FACIRC_1:26;
reconsider t = s as State of ((BitSubtracterCirc x,y,c) +* (BorrowCirc x,y,c)) ;
A5: InputVertices (BorrowStr x,y,c) = {x,y,c} by A1, A2, A3, Th15;
A6: InnerVertices (2GatesCircStr x,y,c,'xor' ) misses InputVertices (2GatesCircStr x,y,c,'xor' ) by XBOOLE_1:79;
A7: InnerVertices (BorrowStr x,y,c) misses InputVertices (BorrowStr x,y,c) by XBOOLE_1:79;
A8: InnerVertices (2GatesCircStr x,y,c,'xor' ) misses InputVertices (BorrowStr x,y,c) by A4, A5, A6, FACIRC_1:57;
A9: InnerVertices (BorrowStr x,y,c) misses InputVertices (2GatesCircStr x,y,c,'xor' ) by A4, A5, A7, FACIRC_1:57;
then A10: Following s1,2 = (Following t,2) | the carrier of (2GatesCircStr x,y,c,'xor' ) by FACIRC_1:30;
A11: Following s1,3 = (Following t,3) | the carrier of (2GatesCircStr x,y,c,'xor' ) by A9, FACIRC_1:30;
A12: Following s2,2 = (Following t,2) | the carrier of (BorrowStr x,y,c) by A8, FACIRC_1:31;
A13: Following s2,3 = (Following t,3) | the carrier of (BorrowStr x,y,c) by A8, FACIRC_1:31;
Following s1,2 is stable by A4, FACIRC_1:63;
then A14: Following s1,2 = Following (Following s1,2) by CIRCUIT2:def 6
.= Following s1,(2 + 1) by FACIRC_1:12 ;
Following s2,2 is stable by A1, A2, A3, Th23;
then A15: Following s2,2 = Following (Following s2,2) by CIRCUIT2:def 6
.= Following s2,(2 + 1) by FACIRC_1:12 ;
A16: Following s,(2 + 1) = Following (Following s,2) by FACIRC_1:12;
A17: dom (Following s,2) = the carrier of (BitSubtracterWithBorrowStr x,y,c) by CIRCUIT1:4;
A18: dom (Following s,3) = the carrier of (BitSubtracterWithBorrowStr x,y,c) by CIRCUIT1:4;
A19: dom (Following s1,2) = the carrier of (2GatesCircStr x,y,c,'xor' ) by CIRCUIT1:4;
A20: dom (Following s2,2) = the carrier of (BorrowStr x,y,c) by CIRCUIT1:4;
A21: the carrier of (BitSubtracterWithBorrowStr x,y,c) = the carrier of (2GatesCircStr x,y,c,'xor' ) \/ the carrier of (BorrowStr x,y,c) by CIRCCOMB:def 2;

now

let a be set ; :: thesis: ( a in the carrier of (BitSubtracterWithBorrowStr x,y,c) implies (Following s,2) . a = (Following (Following s,2)) . a )
assume a in the carrier of (BitSubtracterWithBorrowStr 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 (BorrowStr x,y,c) ) by A21, 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 A10, A11, A12, A13, A14, A15, A19, A20, FUNCT_1:70;
hence (Following s,2) . a = (Following (Following s,2)) . a by A14, A15, FACIRC_1:12; :: thesis: verum

end;

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