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

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

.= 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:3;

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

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

A20: dom (Following (s2,2)) = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3;

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;

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

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

.= 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:3;

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

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

A20: dom (Following (s2,2)) = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3;

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 :: thesis: for a being object st a in the carrier of (BitSubtracterWithBorrowStr (x,y,c)) holds

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

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

let a be object ; :: 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:47;

hence (Following (s,2)) . a = (Following (Following (s,2))) . a by A14, A15, FACIRC_1:12; :: thesis: verum

end;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:47;

hence (Following (s,2)) . a = (Following (Following (s,2))) . a by A14, A15, FACIRC_1:12; :: thesis: verum