let n be Element of NAT ; :: thesis: for x, y being nonpair-yielding FinSeqLen of n
for s being State of (n -BitSubtracterCirc (x,y)) holds Following (s,(1 + (2 * n))) is stable
let f, g be nonpair-yielding FinSeqLen of n; :: thesis: for s being State of (n -BitSubtracterCirc (f,g)) holds Following (s,(1 + (2 * n))) is stable
deffunc H1( set , Nat) -> ManySortedSign = BitSubtracterWithBorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H2( set , Nat) -> MSAlgebra of BitSubtracterWithBorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1) = BitSubtracterWithBorrowCirc ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H3( set , Nat) -> Element of InnerVertices (BorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = BorrowOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1);
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
consider N being Function of NAT,NAT such that
A1: N . 0 = 1 and
A2: N . 1 = 2 and
A3: N . 2 = n by FACIRC_2:35;
deffunc H4( Element of NAT ) -> Element of NAT = N . $1;
A4: for x being set
for n being Nat holds H2(x,n) is strict gate`2=den Boolean Circuit of H1(x,n) ;
A5: now
let s be State of (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))); :: thesis: Following (s,H4( 0 )) is stable
Following (s,1) = Following s by FACIRC_1:14;
hence Following (s,H4( 0 )) is stable by A1, CIRCCMB2:2; :: thesis: verum
end;
deffunc H5( Element of NAT ) -> Element of InnerVertices ($1 -BitSubtracterStr (f,g)) = $1 -BitBorrowOutput (f,g);
consider h being ManySortedSet of NAT such that
A6: for n being Element of NAT holds h . n = H5(n) from PBOOLE:sch 5();
 A7: for n being Nat
for x being set
for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable
proof
let n be Nat; :: thesis: for x being set
for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable
let x be set ; :: thesis: for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable
let A be non-empty Circuit of H1(x,n); :: thesis: ( x = h . n & A = H2(x,n) implies for s being State of A holds Following (s,H4(1)) is stable )
A8: n in NAT by ORDINAL1:def 12;
assume x = h . n ; :: thesis: ( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable )
then A9: x = n -BitBorrowOutput (f,g) by A6, A8;
then A10: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2a] by A8, Th19;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor'] by A8, A9, Th19;
hence ( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable ) by A2, A10, Th25; :: thesis: verum
end;
set Sn = n -BitSubtracterStr (f,g);
set An = n -BitSubtracterCirc (f,g);
set o0 = 0 -BitBorrowOutput (f,g);
consider f1, g1, h1 being ManySortedSet of NAT such that
A11: n -BitSubtracterStr (f,g) = f1 . n and
A12: n -BitSubtracterCirc (f,g) = g1 . n and
A13: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A14: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A15: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A16: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds
( f1 . (n + 1) = S +* (BitSubtracterWithBorrowStr ((f . (n + 1)),(g . (n + 1)),z)) & g1 . (n + 1) = A +* (BitSubtracterWithBorrowCirc ((f . (n + 1)),(g . (n + 1)),z)) & h1 . (n + 1) = BorrowOutput ((f . (n + 1)),(g . (n + 1)),z) ) by Def2;
now
let i be set ; :: thesis: ( i in NAT implies h1 . i = h . i )
assume i in NAT ; :: thesis: h1 . i = h . i
then reconsider j = i as Element of NAT ;
thus h1 . i = j -BitBorrowOutput (f,g) by A13, A14, A15, A16, Th1
.= h . i by A6 ; :: thesis: verum
end;
then A17: h1 = h by PBOOLE:3;
A18: ex u, v being ManySortedSet of NAT st
( n -BitSubtracterStr (f,g) = u . H4(2) & n -BitSubtracterCirc (f,g) = v . H4(2) & u . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitBorrowOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S
for x being set
for A2 being non-empty MSAlgebra of H1(x,n) st S = u . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds
( u . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
proof
take f1 ; :: thesis: ex v being ManySortedSet of NAT st
( n -BitSubtracterStr (f,g) = f1 . H4(2) & n -BitSubtracterCirc (f,g) = v . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitBorrowOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S
for x being set
for A2 being non-empty MSAlgebra of H1(x,n) st S = f1 . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds
( f1 . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
take g1 ; :: thesis: ( n -BitSubtracterStr (f,g) = f1 . H4(2) & n -BitSubtracterCirc (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitBorrowOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S
for x being set
for A2 being non-empty MSAlgebra of H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds
( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
thus ( n -BitSubtracterStr (f,g) = f1 . H4(2) & n -BitSubtracterCirc (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitBorrowOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S
for x being set
for A2 being non-empty MSAlgebra of H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds
( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) by A3, A6, A11, A12, A13, A14, A16, A17; :: thesis: verum
end;
A19: ( InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) is Relation & not InputVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) is with_pair ) by FACIRC_1:38, FACIRC_1:39;
A20: [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] = 0 -BitBorrowOutput (f,g) by Th2;
InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) = {[<*>,((0 -tuples_on BOOLEAN) --> TRUE)]} by CIRCCOMB:42;
then A21: ( h . 0 = 0 -BitBorrowOutput (f,g) & 0 -BitBorrowOutput (f,g) in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) ) by A6, A20, TARSKI:def 1;
A22: for n being Nat
for x being set holds InnerVertices H1(x,n) is Relation by FSCIRC_1:22;
A23: for n being Nat
for x being set st x = h . n holds
not (InputVertices H1(x,n)) \ {x} is with_pair
proof
let n be Nat; :: thesis: for x being set st x = h . n holds
not (InputVertices H1(x,n)) \ {x} is with_pair
let x be set ; :: thesis: ( x = h . n implies not (InputVertices H1(x,n)) \ {x} is with_pair )
assume A24: x = h . n ; :: thesis: not (InputVertices H1(x,n)) \ {x} is with_pair
A25: n in NAT by ORDINAL1:def 12;
then A26: x = n -BitBorrowOutput (f,g) by A6, A24;
then A27: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2a] by A25, Th19;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor'] by A25, A26, Th19;
then A28: InputVertices H1(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A27, Th16;
let a be pair set ; :: according to FACIRC_1:def 2 :: thesis: not a in (InputVertices H1(x,n)) \ {x}
assume A29: a in (InputVertices H1(x,n)) \ {x} ; :: thesis: contradiction
then A30: a in {(f . (n + 1)),(g . (n + 1)),x} by A28, XBOOLE_0:def 5;
A31: not a in {x} by A29, XBOOLE_0:def 5;
( a = f . (n + 1) or a = g . (n + 1) or a = x ) by A30, ENUMSET1:def 1;
hence contradiction by A31, TARSKI:def 1; :: thesis: verum
end;
A32: for n being Nat
for x being set st x = h . n holds
( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
proof
let n be Nat; :: thesis: for x being set st x = h . n holds
( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
let x be set ; :: thesis: ( x = h . n implies ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) )
assume A33: x = h . n ; :: thesis: ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
A34: n in NAT by ORDINAL1:def 12;
then A35: x = n -BitBorrowOutput (f,g) by A6, A33;
h . (n + 1) = (n + 1) -BitBorrowOutput (f,g) by A6;
hence h . (n + 1) = H3(x,n) by A34, A35, Th7; :: thesis: ( x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
A36: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2a] by A34, A35, Th19;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor'] by A34, A35, Th19;
then InputVertices H1(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A36, Th16;
hence x in InputVertices H1(x,n) by ENUMSET1:def 1; :: thesis: H3(x,n) in InnerVertices H1(x,n)
set xx = f . (n + 1);
set xy = g . (n + 1);
A37: H3(x,n) in {H3(x,n)} by TARSKI:def 1;
InnerVertices H1(x,n) = ({[<*(f . (n + 1)),(g . (n + 1))*>,'xor'],(2GatesCircOutput ((f . (n + 1)),(g . (n + 1)),x,'xor'))} \/ {[<*(f . (n + 1)),(g . (n + 1))*>,and2a],[<*(g . (n + 1)),x*>,and2],[<*(f . (n + 1)),x*>,and2a]}) \/ {(BorrowOutput ((f . (n + 1)),(g . (n + 1)),x))} by Th17;
hence H3(x,n) in InnerVertices H1(x,n) by A37, XBOOLE_0:def 3; :: thesis: verum
end;
for s being State of (n -BitSubtracterCirc (f,g)) holds Following (s,(H4( 0 ) + (H4(2) * H4(1)))) is stable from CIRCCMB2:sch 22(A4, A5, A7, A18, A19, A21, A22, A23, A32);
 hence for s being State of (n -BitSubtracterCirc (f,g)) holds Following (s,(1 + (2 * n))) is stable by A1, A2, A3; :: thesis: verum