let x, y be FinSequence; :: thesis: for f, g, h being ManySortedSet of NAT st f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) holds
for n being Nat holds
( n -BitSubtracterStr (x,y) = f . n & n -BitSubtracterCirc (x,y) = g . n & n -BitBorrowOutput (x,y) = h . n )
let f, g, h be ManySortedSet of NAT ; :: thesis: ( f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) implies for n being Nat holds
( n -BitSubtracterStr (x,y) = f . n & n -BitSubtracterCirc (x,y) = g . n & n -BitBorrowOutput (x,y) = h . n ) )
deffunc H₁( set , Nat) -> Element of InnerVertices (BorrowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = BorrowOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H₂( Nat, set ) -> Element of InnerVertices (BorrowStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = BorrowOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
deffunc H₃( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitSubtracterWithBorrowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H₄( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitSubtracterWithBorrowStr ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitSubtracterWithBorrowCirc ((x . ($4 + 1)),(y . ($4 + 1)),$3));
assume that
A1: ( f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) ) and
A2: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A3: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = H₃(S,z,n) & g . (n + 1) = H₄(S,A,z,n) & h . (n + 1) = H₁(z,n) ) ; :: thesis: for n being Nat holds
( n -BitSubtracterStr (x,y) = f . n & n -BitSubtracterCirc (x,y) = g . n & n -BitBorrowOutput (x,y) = h . n )
let n be Nat; :: thesis: ( n -BitSubtracterStr (x,y) = f . n & n -BitSubtracterCirc (x,y) = g . n & n -BitBorrowOutput (x,y) = h . n )
consider f1, g1, h1 being ManySortedSet of NAT such that
A4: n -BitSubtracterStr (x,y) = f1 . n and
A5: n -BitSubtracterCirc (x,y) = g1 . n and
A6: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A7: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A8: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A9: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds
( f1 . (n + 1) = H₃(S,z,n) & g1 . (n + 1) = H₄(S,A,z,n) & h1 . (n + 1) = H₁(z,n) ) by Def2;
A10: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . 0 & A = g . 0 ) by A1;
A11: ( f . 0 = f1 . 0 & g . 0 = g1 . 0 & h . 0 = h1 . 0 ) by A1, A2, A6, A7, A8;
A12: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H₄(S,A,z,n) is non-empty MSAlgebra over H₃(S,z,n) ;
( f = f1 & g = g1 & h = h1 ) from CIRCCMB2:sch 14(A10, A11, A3, A9, A12);
hence ( n -BitSubtracterStr (x,y) = f . n & n -BitSubtracterCirc (x,y) = g . n ) by A4, A5; :: thesis: n -BitBorrowOutput (x,y) = h . n
A13: for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = H₃(S,z,n) & h . (n + 1) = H₁(z,n) ) from CIRCCMB2:sch 15(A1, A3, A12);
A14: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by A1;
A15: for n being Nat
for z being set st z = h . n holds
h . (n + 1) = H₁(z,n) from CIRCCMB2:sch 3(A14, A13);
A16: dom h = NAT by PARTFUN1:def 2;
A17: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A2;
A18: for n being Nat holds h . (n + 1) = H₂(n,h . n) by A15;
consider h1 being ManySortedSet of NAT such that
A19: n -BitBorrowOutput (x,y) = h1 . n and
A20: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A21: for n being Nat holds h1 . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h1 . n)) by Def3;
A22: dom h1 = NAT by PARTFUN1:def 2;
A23: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A20;
A24: for n being Nat holds h1 . (n + 1) = H₂(n,h1 . n) by A21;
h = h1 from NAT_1:sch 15(A16, A17, A18, A22, A23, A24);
hence n -BitBorrowOutput (x,y) = h . n by A19; :: thesis: verum