set f = 'xor' ;
let x, y, c be non pair set ; :: thesis: 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 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: 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 ; :: thesis: ( 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
A1: a1 = s . x and
A2: a2 = s . y and
A3: a3 = s . c ; :: thesis: ( (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) )
reconsider s1 = s | the carrier of (2GatesCircStr (x,y,c,'xor')) as State of (BitSubtracterCirc (x,y,c)) by FACIRC_1:26;
A4: dom s1 = the carrier of (2GatesCircStr (x,y,c,'xor')) by CIRCUIT1:3;
c in the carrier of (2GatesCircStr (x,y,c,'xor')) by FACIRC_1:60;
then A5: a3 = s1 . c by A3, A4, FUNCT_1:47;
y in the carrier of (2GatesCircStr (x,y,c,'xor')) by FACIRC_1:60;
then A6: a2 = s1 . y by A2, A4, FUNCT_1:47;
reconsider t = s as State of ((BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c))) ;
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 A7: (Following (t,2)) . (2GatesCircOutput (x,y,c,'xor')) = (Following (s1,2)) . (2GatesCircOutput (x,y,c,'xor')) by FACIRC_1:32;
reconsider s2 = s | the carrier of (BorrowStr (x,y,c)) as State of (BorrowCirc (x,y,c)) by FACIRC_1:26;
A8: dom s2 = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3;
x in the carrier of (2GatesCircStr (x,y,c,'xor')) by FACIRC_1:60;
then a1 = s1 . x by A1, A4, FUNCT_1:47;
hence (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 by A6, A5, A7, FACIRC_1:64; :: thesis: (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3)
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 A9: (Following (t,2)) . (BorrowOutput (x,y,c)) = (Following (s2,2)) . (BorrowOutput (x,y,c)) by FACIRC_1:33;
c in the carrier of (BorrowStr (x,y,c)) by Th6;
then A10: a3 = s2 . c by A3, A8, FUNCT_1:47;
y in the carrier of (BorrowStr (x,y,c)) by Th6;
then A11: a2 = s2 . y by A2, A8, FUNCT_1:47;
x in the carrier of (BorrowStr (x,y,c)) by Th6;
then a1 = s2 . x by A1, A8, FUNCT_1:47;
hence (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) by A11, A10, A9, Lm2; :: thesis: verum