let x, y, c be set ; ( 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))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) ) )
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']
; for s being State of (BitSubtracterWithBorrowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) )
set f = 'xor' ;
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)); for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) )
let a1, a2, a3 be Element of BOOLEAN ; ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) ) )
assume that
A5:
a1 = s . x
and
A6:
a2 = s . y
and
A7:
a3 = s . c
; ( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) )
A8:
x in the carrier of (2GatesCircStr (x,y,c,'xor'))
by FACIRC_1:60;
A9:
y in the carrier of (2GatesCircStr (x,y,c,'xor'))
by FACIRC_1:60;
A10:
c in the carrier of (2GatesCircStr (x,y,c,'xor'))
by FACIRC_1:60;
A11:
x in the carrier of (BorrowStr (x,y,c))
by FSCIRC_1:6;
A12:
y in the carrier of (BorrowStr (x,y,c))
by FSCIRC_1:6;
A13:
c in the carrier of (BorrowStr (x,y,c))
by FSCIRC_1:6;
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))) ;
A14:
InputVertices (BorrowStr (x,y,c)) = {x,y,c}
by A1, A2, A3, Th15;
A15:
InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (2GatesCircStr (x,y,c,'xor'))
by XBOOLE_1:79;
A16:
InnerVertices (BorrowStr (x,y,c)) misses InputVertices (BorrowStr (x,y,c))
by XBOOLE_1:79;
A17:
InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (BorrowStr (x,y,c))
by A4, A14, A15, FACIRC_1:57;
A18:
InnerVertices (BorrowStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor'))
by A4, A14, A16, FACIRC_1:57;
A19:
dom s1 = the carrier of (2GatesCircStr (x,y,c,'xor'))
by CIRCUIT1:3;
then A20:
a1 = s1 . x
by A5, A8, FUNCT_1:47;
A21:
a2 = s1 . y
by A6, A9, A19, FUNCT_1:47;
A22:
a3 = s1 . c
by A7, A10, A19, FUNCT_1:47;
(Following (t,2)) . (2GatesCircOutput (x,y,c,'xor')) = (Following (s1,2)) . (2GatesCircOutput (x,y,c,'xor'))
by A18, FACIRC_1:32;
hence
(Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3
by A4, A20, A21, A22, FACIRC_1:64; (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3)
A23:
dom s2 = the carrier of (BorrowStr (x,y,c))
by CIRCUIT1:3;
then A24:
a1 = s2 . x
by A5, A11, FUNCT_1:47;
A25:
a2 = s2 . y
by A6, A12, A23, FUNCT_1:47;
A26:
a3 = s2 . c
by A7, A13, A23, FUNCT_1:47;
(Following (t,2)) . (BorrowOutput (x,y,c)) = (Following (s2,2)) . (BorrowOutput (x,y,c))
by A17, FACIRC_1:33;
hence
(Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3)
by A1, A2, A3, A24, A25, A26, Lm2; verum