let x, y, c be non pair set ; 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)); 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))) ;
A1:
dom (Following (s,3)) = the carrier of (BitSubtracterWithBorrowStr (x,y,c))
by CIRCUIT1:3;
A2:
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;
InputVertices (2GatesCircStr (x,y,c,'xor')) is without_pairs
by FACIRC_1:59;
then
InnerVertices (BorrowStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor'))
by Th1, FACIRC_1:5;
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 FACIRC_1:30;
Following (s1,2) is stable
by FACIRC_1:63;
then A4: Following (s1,2) =
Following (Following (s1,2))
.=
Following (s1,(2 + 1))
by FACIRC_1:12
;
InputVertices (BorrowStr (x,y,c)) is without_pairs
by Th2;
then
InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (BorrowStr (x,y,c))
by FACIRC_1:5, FACIRC_1:58;
then A5:
( Following (s2,2) = (Following (t,2)) | the carrier of (BorrowStr (x,y,c)) & Following (s2,3) = (Following (t,3)) | the carrier of (BorrowStr (x,y,c)) )
by FACIRC_1:31;
Following (s2,2) is stable
by Th18;
then A6: Following (s2,2) =
Following (Following (s2,2))
.=
Following (s2,(2 + 1))
by FACIRC_1:12
;
A7:
( dom (Following (s1,2)) = the carrier of (2GatesCircStr (x,y,c,'xor')) & dom (Following (s2,2)) = the carrier of (BorrowStr (x,y,c)) )
by CIRCUIT1:3;
A8:
now for a being object st a in the carrier of (BitSubtracterWithBorrowStr (x,y,c)) holds
(Following (s,2)) . a = (Following (Following (s,2))) . alet a be
object ;
( 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))
;
(Following (s,2)) . a = (Following (Following (s,2))) . athen
(
a in the
carrier of
(2GatesCircStr (x,y,c,'xor')) or
a in the
carrier of
(BorrowStr (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, FACIRC_1:12;
verum end;
( Following (s,(2 + 1)) = Following (Following (s,2)) & dom (Following (s,2)) = the carrier of (BitSubtracterWithBorrowStr (x,y,c)) )
by CIRCUIT1:3, FACIRC_1:12;
hence
Following (s,2) = Following (Following (s,2))
by A1, A8, FUNCT_1:2; CIRCUIT2:def 6 verum