:: FSCIRC_2 semantic presentation

begin

definition
let n be Nat;
let x, y be FinSequence;
deffunc H1( set , Nat) ->  Element of InnerVertices (BorrowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = BorrowOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitSubtracterWithBorrowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
A1: ( 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is unsplit & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is gate`1=arity & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is gate`2isBoolean & not 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is void & not 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is empty & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is strict ) ;
funcn -BitSubtracterStr (x,y) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign  means :Def1: :: FSCIRC_2:def 1
 ex f, g being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) );
uniqueness
 for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) & ex f, g being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) holds
b1 = b2
proof
 for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = H2(S,x,n) & h . (n + 1) = H1(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = H2(S,x,n) & h . (n + 1) = H1(x,n) ) ) ) holds
S1 = S2 from CIRCCMB2:sch_9();
hence  for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) & ex f, g being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
existence
 ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) )
proof
deffunc H3( set , Nat) ->  ManySortedSign = BitSubtracterWithBorrowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1);
 ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = S +* H3(x,n) & h . (n + 1) = H1(x,n) ) ) ) from CIRCCMB2:sch_8(A1);
hence  ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines -BitSubtracterStr FSCIRC_2:def_1_:_
 for n being Nat
for x, y being FinSequence
for b4 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b4 = n -BitSubtracterStr (x,y) iff ex f, g being ManySortedSet of NAT st
( b4 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
funcn -BitSubtracterCirc (x,y) ->  strict gate`2=den Boolean Circuit of n -BitSubtracterStr (x,y) means :Def2: :: FSCIRC_2:def 2
 ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & it = g . n & 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) ) ) );
uniqueness
 for b1, b2 being strict gate`2=den Boolean Circuit of n -BitSubtracterStr (x,y) st ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & b1 = g . n & 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) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & b2 = g . n & 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
b1 = b2
proof
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set Sn = n -BitSubtracterStr (x,y);
set o0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)];
deffunc H1( set , Nat) ->  Element of InnerVertices (BorrowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = BorrowOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitSubtracterWithBorrowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H3( 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));
A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H3(S,A,z,n) is non-empty MSAlgebra over H2(S,z,n) ;
thus  for A1, A2 being strict gate`2=den Boolean Circuit of n -BitSubtracterStr (x,y) st ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & A1 = g . n & 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 x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H3(S,A,x,n) & h . (n + 1) = H1(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & A2 = g . n & 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 x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H3(S,A,x,n) & h . (n + 1) = H1(x,n) ) ) ) holds
A1 = A2 from CIRCCMB2:sch_21(A1); ::_thesis: verum
end;
existence
 ex b1 being strict gate`2=den Boolean Circuit of n -BitSubtracterStr (x,y) ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & b1 = g . n & 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) ) ) )
proof
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set Sn = n -BitSubtracterStr (x,y);
set o0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)];
deffunc H1( set , Nat) ->  Element of InnerVertices (BorrowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = BorrowOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitSubtracterWithBorrowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H3( 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));
A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for z being set
for n being Nat holds
( H2(S,z,n) is unsplit & H2(S,z,n) is gate`1=arity & H2(S,z,n) is gate`2isBoolean & not H2(S,z,n) is void & H2(S,z,n) is strict ) ;
A3: for S, S1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being strict gate`2=den Boolean Circuit of S
for z being set
for n being Nat st S1 = H2(S,z,n) holds
H3(S,A,z,n) is strict gate`2=den Boolean Circuit of S1 ;
A4: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H3(S,A,z,n) is non-empty MSAlgebra over H2(S,z,n) ;
A5: ex f, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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) = H2(S,z,n) & h . (n + 1) = H1(z,n) ) ) ) by Def1;
thus  ex A being strict gate`2=den Boolean Circuit of n -BitSubtracterStr (x,y) ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & A = g . n & 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 x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H3(S,A,x,n) & h . (n + 1) = H1(x,n) ) ) ) from CIRCCMB2:sch_19(A2, A5, A4, A3); ::_thesis: verum
end;
end;

:: deftheorem Def2 defines -BitSubtracterCirc FSCIRC_2:def_2_:_
 for n being Nat
for x, y being FinSequence
for b4 being strict gate`2=den Boolean Circuit of n -BitSubtracterStr (x,y) holds
( b4 = n -BitSubtracterCirc (x,y) iff ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr (x,y) = f . n & b4 = g . n & 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) ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
set c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)];
funcn -BitBorrowOutput (x,y) ->  Element of InnerVertices (n -BitSubtracterStr (x,y)) means :Def3: :: FSCIRC_2:def 3
 ex h being ManySortedSet of NAT st
( it = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) );
uniqueness
 for b1, b2 being Element of InnerVertices (n -BitSubtracterStr (x,y)) st ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) & ex h being ManySortedSet of NAT st
( b2 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) holds
b1 = b2
proof
let o1, o2 be Element of InnerVertices (n -BitSubtracterStr (x,y)); ::_thesis: ( ex h being ManySortedSet of NAT st
( o1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) & ex h being ManySortedSet of NAT st
( o2 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) implies o1 = o2 )
given h1 being ManySortedSet of NAT  such that A1: o1 = h1 . n and
A2: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A3: for n being Nat holds h1 . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h1 . n)) ; ::_thesis: ( for h being ManySortedSet of NAT holds
( not o2 = h . n or not h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] or ex n being Nat st not h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) or o1 = o2 )
given h2 being ManySortedSet of NAT  such that A4: o2 = h2 . n and
A5: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A6: for n being Nat holds h2 . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h2 . n)) ; ::_thesis: o1 = o2
deffunc H1( Nat, set ) ->  Element of InnerVertices (BorrowStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = BorrowOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
A7: dom h1 = NAT by PARTFUN1:def_2;
A8: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A2;
A9: for n being Nat holds h1 . (n + 1) = H1(n,h1 . n) by A3;
A10: dom h2 = NAT by PARTFUN1:def_2;
A11: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A5;
A12: for n being Nat holds h2 . (n + 1) = H1(n,h2 . n) by A6;
 h1 = h2 from NAT_1:sch_15(A7, A8, A9, A10, A11, A12);
hence  o1 = o2 by A1, A4; ::_thesis: verum
end;
existence
 ex b1 being Element of InnerVertices (n -BitSubtracterStr (x,y)) ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) )
proof
defpred S1[ set , set , set ] means verum;
deffunc H1( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitSubtracterWithBorrowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H2( set , Nat) ->  Element of InnerVertices (BorrowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = BorrowOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
consider f, g being ManySortedSet of NAT  such that
A13: n -BitSubtracterStr (x,y) = f . n and
A14: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A15: g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A16: for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = H1(S,z,n) & g . (n + 1) = H2(z,n) ) by Def1;
defpred S2[ Nat] means  ex S being non empty ManySortedSign st
( S = f . $1 & g . $1 in InnerVertices S );
 InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) = {[<*>,((0 -tuples_on BOOLEAN) --> TRUE)]} by CIRCCOMB:42;
then  [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) by TARSKI:def_1;
then A17: S2[ 0 ] by A14, A15;
A18: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] )
assume that
A19: ex S being non empty ManySortedSign st
( S = f . i & g . i in InnerVertices S ) and
A20: for S being non empty ManySortedSign st S = f . (i + 1) holds
not g . (i + 1) in InnerVertices S ; ::_thesis: contradiction
consider S being non empty ManySortedSign  such that
A21: S = f . i and
 g . i in InnerVertices S by A19;
 BorrowOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) in InnerVertices (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(g . i))) by FACIRC_1:21;
then A22: BorrowOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) in InnerVertices (S +* (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(g . i)))) by FACIRC_1:22;
A23: f . (i + 1) = S +* (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(g . i))) by A16, A21;
 g . (i + 1) = BorrowOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) by A16, A21;
hence  contradiction by A20, A22, A23; ::_thesis: verum
end;
 for i being Nat holds S2[i] from NAT_1:sch_2(A17, A18);
then  ex S being non empty ManySortedSign st
( S = f . n & g . n in InnerVertices S ) ;
then reconsider o = g . n as Element of InnerVertices (n -BitSubtracterStr (x,y)) by A13;
take  o ; ::_thesis: ex h being ManySortedSet of NAT st
( o = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) )
take  g ; ::_thesis: ( o = g . n & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(g . n)) ) )
thus  ( o = g . n & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] ) by A15; ::_thesis: for n being Nat holds g . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(g . n))
let i be Nat; ::_thesis: g . (i + 1) = BorrowOutput ((x . (i + 1)),(y . (i + 1)),(g . i))
A24: ex S being non empty ManySortedSign ex x being set st
( S = f . 0 & x = g . 0 & S1[S,x, 0 ] ) by A14;
A25: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = g . n & S1[S,x,n] holds
S1[H1(S,x,n),H2(x,n),n + 1] ;
 for n being Nat ex S being non empty ManySortedSign st
( S = f . n & S1[S,g . n,n] ) from CIRCCMB2:sch_2(A24, A16, A25);
then  ex S being non empty ManySortedSign st S = f . i ;
hence  g . (i + 1) = BorrowOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) by A16; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines -BitBorrowOutput FSCIRC_2:def_3_:_
 for n being Nat
for x, y being FinSequence
for b4 being Element of InnerVertices (n -BitSubtracterStr (x,y)) holds
( b4 = n -BitBorrowOutput (x,y) iff ex h being ManySortedSet of NAT st
( b4 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) );

theorem Th1: :: FSCIRC_2:1
for x, y being FinSequence
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 )
proof
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 H1( set , Nat) ->  Element of InnerVertices (BorrowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = BorrowOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( Nat, set ) ->  Element of InnerVertices (BorrowStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = BorrowOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
deffunc H3( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitSubtracterWithBorrowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H4( 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) = H3(S,z,n) & g . (n + 1) = H4(S,A,z,n) & h . (n + 1) = H1(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) = H3(S,z,n) & g1 . (n + 1) = H4(S,A,z,n) & h1 . (n + 1) = H1(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 H4(S,A,z,n) is non-empty MSAlgebra over H3(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) = H3(S,z,n) & h . (n + 1) = H1(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) = H1(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) = H2(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) = H2(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
end;

theorem Th2: :: FSCIRC_2:2
for a, b being FinSequence holds
( 0 -BitSubtracterStr (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitSubtracterCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitBorrowOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] )
proof
let a, b be FinSequence; ::_thesis: ( 0 -BitSubtracterStr (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitSubtracterCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitBorrowOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] )
A1: ex f, g, h being ManySortedSet of NAT st
( 0 -BitSubtracterStr (a,b) = f . 0 & 0 -BitSubtracterCirc (a,b) = g . 0 & 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 ((a . (n + 1)),(b . (n + 1)),z)) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc ((a . (n + 1)),(b . (n + 1)),z)) & h . (n + 1) = BorrowOutput ((a . (n + 1)),(b . (n + 1)),z) ) ) ) by Def2;
hence  0 -BitSubtracterStr (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) ; ::_thesis: ( 0 -BitSubtracterCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitBorrowOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] )
thus  0 -BitSubtracterCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by A1; ::_thesis: 0 -BitBorrowOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]
 InnerVertices (0 -BitSubtracterStr (a,b)) = {[<*>,((0 -tuples_on BOOLEAN) --> TRUE)]} by A1, CIRCCOMB:42;
hence  0 -BitBorrowOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by TARSKI:def_1; ::_thesis: verum
end;

theorem Th3: :: FSCIRC_2:3
for a, b being FinSequence
for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitSubtracterStr (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr ((a . 1),(b . 1),c)) & 1 -BitSubtracterCirc (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc ((a . 1),(b . 1),c)) & 1 -BitBorrowOutput (a,b) = BorrowOutput ((a . 1),(b . 1),c) )
proof
let a, b be FinSequence; ::_thesis: for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitSubtracterStr (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr ((a . 1),(b . 1),c)) & 1 -BitSubtracterCirc (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc ((a . 1),(b . 1),c)) & 1 -BitBorrowOutput (a,b) = BorrowOutput ((a . 1),(b . 1),c) )
let c be set ; ::_thesis: ( c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] implies ( 1 -BitSubtracterStr (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr ((a . 1),(b . 1),c)) & 1 -BitSubtracterCirc (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc ((a . 1),(b . 1),c)) & 1 -BitBorrowOutput (a,b) = BorrowOutput ((a . 1),(b . 1),c) ) )
assume A1: c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] ; ::_thesis: ( 1 -BitSubtracterStr (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr ((a . 1),(b . 1),c)) & 1 -BitSubtracterCirc (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc ((a . 1),(b . 1),c)) & 1 -BitBorrowOutput (a,b) = BorrowOutput ((a . 1),(b . 1),c) )
consider f, g, h being ManySortedSet of NAT  such that
A2: 1 -BitSubtracterStr (a,b) = f . 1 and
A3: 1 -BitSubtracterCirc (a,b) = g . 1 and
A4: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A5: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A6: h . 0 = c and
A7: 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 ((a . (n + 1)),(b . (n + 1)),z)) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc ((a . (n + 1)),(b . (n + 1)),z)) & h . (n + 1) = BorrowOutput ((a . (n + 1)),(b . (n + 1)),z) ) by A1, Def2;
 1 -BitBorrowOutput (a,b) = h . (0 + 1) by A1, A4, A5, A6, A7, Th1;
hence  ( 1 -BitSubtracterStr (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr ((a . 1),(b . 1),c)) & 1 -BitSubtracterCirc (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc ((a . 1),(b . 1),c)) & 1 -BitBorrowOutput (a,b) = BorrowOutput ((a . 1),(b . 1),c) ) by A2, A3, A4, A5, A6, A7; ::_thesis: verum
end;

theorem :: FSCIRC_2:4
for a, b, c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitSubtracterStr (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr (a,b,c)) & 1 -BitSubtracterCirc (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc (a,b,c)) & 1 -BitBorrowOutput (<*a*>,<*b*>) = BorrowOutput (a,b,c) )
proof
let a, b be set ; ::_thesis: for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitSubtracterStr (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr (a,b,c)) & 1 -BitSubtracterCirc (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc (a,b,c)) & 1 -BitBorrowOutput (<*a*>,<*b*>) = BorrowOutput (a,b,c) )
A1: <*a*> . 1 = a by FINSEQ_1:40;
 <*b*> . 1 = b by FINSEQ_1:40;
hence  for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitSubtracterStr (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr (a,b,c)) & 1 -BitSubtracterCirc (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc (a,b,c)) & 1 -BitBorrowOutput (<*a*>,<*b*>) = BorrowOutput (a,b,c) ) by A1, Th3; ::_thesis: verum
end;

theorem Th5: :: FSCIRC_2:5
for n being Element of NAT
for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitSubtracterStr ((p ^ p1),(q ^ q1)) = n -BitSubtracterStr ((p ^ p2),(q ^ q2)) & n -BitSubtracterCirc ((p ^ p1),(q ^ q1)) = n -BitSubtracterCirc ((p ^ p2),(q ^ q2)) & n -BitBorrowOutput ((p ^ p1),(q ^ q1)) = n -BitBorrowOutput ((p ^ p2),(q ^ q2)) )
proof
let n be Element of NAT ; ::_thesis: for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitSubtracterStr ((p ^ p1),(q ^ q1)) = n -BitSubtracterStr ((p ^ p2),(q ^ q2)) & n -BitSubtracterCirc ((p ^ p1),(q ^ q1)) = n -BitSubtracterCirc ((p ^ p2),(q ^ q2)) & n -BitBorrowOutput ((p ^ p1),(q ^ q1)) = n -BitBorrowOutput ((p ^ p2),(q ^ q2)) )
set c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)];
let p, q be FinSeqLen of n; ::_thesis: for p1, p2, q1, q2 being FinSequence holds
( n -BitSubtracterStr ((p ^ p1),(q ^ q1)) = n -BitSubtracterStr ((p ^ p2),(q ^ q2)) & n -BitSubtracterCirc ((p ^ p1),(q ^ q1)) = n -BitSubtracterCirc ((p ^ p2),(q ^ q2)) & n -BitBorrowOutput ((p ^ p1),(q ^ q1)) = n -BitBorrowOutput ((p ^ p2),(q ^ q2)) )
let p1, p2, q1, q2 be FinSequence; ::_thesis: ( n -BitSubtracterStr ((p ^ p1),(q ^ q1)) = n -BitSubtracterStr ((p ^ p2),(q ^ q2)) & n -BitSubtracterCirc ((p ^ p1),(q ^ q1)) = n -BitSubtracterCirc ((p ^ p2),(q ^ q2)) & n -BitBorrowOutput ((p ^ p1),(q ^ q1)) = n -BitBorrowOutput ((p ^ p2),(q ^ q2)) )
deffunc H1( set , Nat) ->  Element of InnerVertices (BorrowStr (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1)) = BorrowOutput (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitSubtracterWithBorrowStr (((p ^ p1) . ($3 + 1)),((q ^ q1) . ($3 + 1)),$2));
deffunc H3( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) ->  MSAlgebra over $1 +* (BitSubtracterWithBorrowStr (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)) = $2 +* (BitSubtracterWithBorrowCirc (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3));
consider f1, g1, h1 being ManySortedSet of NAT  such that
A1: n -BitSubtracterStr ((p ^ p1),(q ^ q1)) = f1 . n and
A2: n -BitSubtracterCirc ((p ^ p1),(q ^ q1)) = g1 . n and
A3: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A4: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A5: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A6: 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) = H2(S,z,n) & g1 . (n + 1) = H3(S,A,z,n) & h1 . (n + 1) = H1(z,n) ) by Def2;
consider f2, g2, h2 being ManySortedSet of NAT  such that
A7: n -BitSubtracterStr ((p ^ p2),(q ^ q2)) = f2 . n and
A8: n -BitSubtracterCirc ((p ^ p2),(q ^ q2)) = g2 . n and
A9: f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A10: g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A11: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A12: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f2 . n & A = g2 . n & z = h2 . n holds
( f2 . (n + 1) = S +* (BitSubtracterWithBorrowStr (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z)) & g2 . (n + 1) = A +* (BitSubtracterWithBorrowCirc (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z)) & h2 . (n + 1) = BorrowOutput (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z) ) by Def2;
defpred S1[ Nat] means ( $1 <= n implies ( h1 . $1 = h2 . $1 & f1 . $1 = f2 . $1 & g1 . $1 = g2 . $1 ) );
A13: S1[ 0 ] by A3, A4, A5, A9, A10, A11;
A14: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume that
A15: ( i <= n implies ( h1 . i = h2 . i & f1 . i = f2 . i & g1 . i = g2 . i ) ) and
A16: i + 1 <= n ; ::_thesis: ( h1 . (i + 1) = h2 . (i + 1) & f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) )
A17: len p = n by CARD_1:def_7;
A18: len q = n by CARD_1:def_7;
A19: dom p = Seg n by A17, FINSEQ_1:def_3;
A20: dom q = Seg n by A18, FINSEQ_1:def_3;
 0 + 1 <= i + 1 by XREAL_1:6;
then A21: i + 1 in Seg n by A16, FINSEQ_1:1;
then A22: (p ^ p1) . (i + 1) = p . (i + 1) by A19, FINSEQ_1:def_7;
A23: (p ^ p2) . (i + 1) = p . (i + 1) by A19, A21, FINSEQ_1:def_7;
A24: (q ^ q1) . (i + 1) = q . (i + 1) by A20, A21, FINSEQ_1:def_7;
A25: (q ^ q2) . (i + 1) = q . (i + 1) by A20, A21, FINSEQ_1:def_7;
defpred S2[ set , set , set , set ] means verum;
A26: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f1 . 0 & A = g1 . 0 & x = h1 . 0 & S2[S,A,x, 0 ] ) by A3, A4;
A27: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f1 . n & A = g1 . n & x = h1 . n & S2[S,A,x,n] holds
S2[H2(S,x,n),H3(S,A,x,n),H1(x,n),n + 1] ;
A28: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H3(S,A,z,n) is non-empty MSAlgebra over H2(S,z,n) ;
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f1 . n & A = g1 . n & S2[S,A,h1 . n,n] ) from CIRCCMB2:sch_13(A26, A6, A27, A28);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A29: S = f1 . i and
A30: A = g1 . i ;
thus h1 . (i + 1) = BorrowOutput (((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i)) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.= h2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: ( f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) )
thus f1 . (i + 1) = S +* (BitSubtracterWithBorrowStr (((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i))) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.= f2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: g1 . (i + 1) = g2 . (i + 1)
thus g1 . (i + 1) = A +* (BitSubtracterWithBorrowCirc (((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i))) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.= g2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: verum
end;
A31: for i being Nat holds S1[i] from NAT_1:sch_2(A13, A14);
hence  ( n -BitSubtracterStr ((p ^ p1),(q ^ q1)) = n -BitSubtracterStr ((p ^ p2),(q ^ q2)) & n -BitSubtracterCirc ((p ^ p1),(q ^ q1)) = n -BitSubtracterCirc ((p ^ p2),(q ^ q2)) ) by A1, A2, A7, A8; ::_thesis: n -BitBorrowOutput ((p ^ p1),(q ^ q1)) = n -BitBorrowOutput ((p ^ p2),(q ^ q2))
A32: n -BitBorrowOutput ((p ^ p1),(q ^ q1)) = h1 . n by A3, A4, A5, A6, Th1;
 n -BitBorrowOutput ((p ^ p2),(q ^ q2)) = h2 . n by A9, A10, A11, A12, Th1;
hence  n -BitBorrowOutput ((p ^ p1),(q ^ q1)) = n -BitBorrowOutput ((p ^ p2),(q ^ q2)) by A31, A32; ::_thesis: verum
end;

theorem :: FSCIRC_2:6
for n being Element of NAT
for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = BorrowOutput (a,b,(n -BitBorrowOutput (x,y))) )
proof
let n be Element of NAT ; ::_thesis: for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = BorrowOutput (a,b,(n -BitBorrowOutput (x,y))) )
set c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)];
let x, y be FinSeqLen of n; ::_thesis: for a, b being set holds
( (n + 1) -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = BorrowOutput (a,b,(n -BitBorrowOutput (x,y))) )
let a, b be set ; ::_thesis: ( (n + 1) -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = BorrowOutput (a,b,(n -BitBorrowOutput (x,y))) )
set p = x ^ <*a*>;
set q = y ^ <*b*>;
consider f, g, h being ManySortedSet of NAT  such that
A1: n -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = f . n and
A2: n -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = g . n and
A3: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A4: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A5: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A6: 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 ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z)) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z)) & h . (n + 1) = BorrowOutput (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z) ) by Def2;
A7: n -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = h . n by A3, A4, A5, A6, Th1;
A8: (n + 1) -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = f . (n + 1) by A3, A4, A5, A6, Th1;
A9: (n + 1) -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = g . (n + 1) by A3, A4, A5, A6, Th1;
A10: (n + 1) -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = h . (n + 1) by A3, A4, A5, A6, Th1;
A11: len x = n by CARD_1:def_7;
A12: len y = n by CARD_1:def_7;
A13: (x ^ <*a*>) . (n + 1) = a by A11, FINSEQ_1:42;
A14: (y ^ <*b*>) . (n + 1) = b by A12, FINSEQ_1:42;
A15: x ^ <*> = x by FINSEQ_1:34;
A16: y ^ <*> = y by FINSEQ_1:34;
then A17: n -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = n -BitSubtracterStr (x,y) by A15, Th5;
A18: n -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = n -BitSubtracterCirc (x,y) by A15, A16, Th5;
 n -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = n -BitBorrowOutput (x,y) by A15, A16, Th5;
hence  ( (n + 1) -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = BorrowOutput (a,b,(n -BitBorrowOutput (x,y))) ) by A1, A2, A6, A7, A8, A9, A10, A13, A14, A17, A18; ::_thesis: verum
end;

theorem Th7: :: FSCIRC_2:7
for n being Element of NAT
for x, y being FinSequence holds
( (n + 1) -BitSubtracterStr (x,y) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc (x,y) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput (x,y) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))) )
proof
let n be Element of NAT ; ::_thesis: for x, y being FinSequence holds
( (n + 1) -BitSubtracterStr (x,y) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc (x,y) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput (x,y) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))) )
let x, y be FinSequence; ::_thesis: ( (n + 1) -BitSubtracterStr (x,y) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc (x,y) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput (x,y) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))) )
set c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)];
consider f, g, h being ManySortedSet of NAT  such that
A1: n -BitSubtracterStr (x,y) = f . n and
A2: n -BitSubtracterCirc (x,y) = g . n and
A3: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A4: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A5: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A6: 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) ) by Def2;
A7: n -BitBorrowOutput (x,y) = h . n by A3, A4, A5, A6, Th1;
A8: (n + 1) -BitSubtracterStr (x,y) = f . (n + 1) by A3, A4, A5, A6, Th1;
A9: (n + 1) -BitSubtracterCirc (x,y) = g . (n + 1) by A3, A4, A5, A6, Th1;
 (n + 1) -BitBorrowOutput (x,y) = h . (n + 1) by A3, A4, A5, A6, Th1;
hence  ( (n + 1) -BitSubtracterStr (x,y) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc (x,y) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput (x,y) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))) ) by A1, A2, A6, A7, A8, A9; ::_thesis: verum
end;

theorem Th8: :: FSCIRC_2:8
for n, m being Element of NAT st n <= m holds
for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (x,y))
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (x,y)) )
assume A1: n <= m ; ::_thesis: for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (x,y))
let x, y be FinSequence; ::_thesis: InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (x,y))
consider i being Nat such that
A2: m = n + i by A1, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
defpred S1[ Element of NAT ] means  InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices ((n + $1) -BitSubtracterStr (x,y));
A3: S1[ 0 ] ;
A4: for j being Element of NAT st S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A5: InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices ((n + j) -BitSubtracterStr (x,y)) ; ::_thesis: S1[j + 1]
A6: InnerVertices (n -BitSubtracterStr (x,y)) c= (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y))))) by XBOOLE_1:7;
 (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y))))) c= (InnerVertices ((n + j) -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y))))) by A5, XBOOLE_1:9;
then  InnerVertices (n -BitSubtracterStr (x,y)) c= (InnerVertices ((n + j) -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y))))) by A6, XBOOLE_1:1;
then  InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (((n + j) -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y))))) by FACIRC_1:27;
hence  S1[j + 1] by Th7; ::_thesis: verum
end;
A7: for j being Element of NAT holds S1[j] from NAT_1:sch_1(A3, A4);
 m = n + i by A2;
hence  InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (x,y)) by A7; ::_thesis: verum
end;

theorem :: FSCIRC_2:9
for n being Element of NAT
for x, y being FinSequence holds InnerVertices ((n + 1) -BitSubtracterStr (x,y)) = (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))))
proof
let n be Element of NAT ; ::_thesis: for x, y being FinSequence holds InnerVertices ((n + 1) -BitSubtracterStr (x,y)) = (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))))
let x, y be FinSequence; ::_thesis: InnerVertices ((n + 1) -BitSubtracterStr (x,y)) = (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))))
 InnerVertices ((n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))))) = (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))))) by FACIRC_1:27;
hence  InnerVertices ((n + 1) -BitSubtracterStr (x,y)) = (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))))) by Th7; ::_thesis: verum
end;

definition
let k, n be Element of NAT ;
assume that
B1: k >= 1 and
B2: k <= n ;
let x, y be FinSequence;
func(k,n) -BitSubtracterOutput (x,y) ->  Element of InnerVertices (n -BitSubtracterStr (x,y)) means :Def4: :: FSCIRC_2:def 4
 ex i being Element of NAT st
( k = i + 1 & it = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) );
uniqueness
 for b1, b2 being Element of InnerVertices (n -BitSubtracterStr (x,y)) st ex i being Element of NAT st
( k = i + 1 & b1 = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) ) & ex i being Element of NAT st
( k = i + 1 & b2 = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) ) holds
b1 = b2 ;
existence
 ex b1 being Element of InnerVertices (n -BitSubtracterStr (x,y)) ex i being Element of NAT st
( k = i + 1 & b1 = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) )
proof
consider i being Nat such that
A1: k = 1 + i by B1, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
set o = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y)));
A2: InnerVertices (k -BitSubtracterStr (x,y)) c= InnerVertices (n -BitSubtracterStr (x,y)) by B2, Th8;
A3: BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) in InnerVertices (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y)))) by A1, FACIRC_1:21;
A4: k -BitSubtracterStr (x,y) = (i -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y)))) by A1, Th7;
reconsider o = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) as Element of (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y)))) by A3;
 the carrier of (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y)))) \/ the carrier of (i -BitSubtracterStr (x,y)) = the carrier of (k -BitSubtracterStr (x,y)) by A4, CIRCCOMB:def_2;
then  o in the carrier of (k -BitSubtracterStr (x,y)) by XBOOLE_0:def_3;
then  o in InnerVertices (k -BitSubtracterStr (x,y)) by A3, A4, CIRCCOMB:15;
hence  ex b1 being Element of InnerVertices (n -BitSubtracterStr (x,y)) ex i being Element of NAT st
( k = i + 1 & b1 = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) ) by A1, A2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines -BitSubtracterOutput FSCIRC_2:def_4_:_
 for k, n being Element of NAT st k >= 1 & k <= n holds
for x, y being FinSequence
for b5 being Element of InnerVertices (n -BitSubtracterStr (x,y)) holds
( b5 = (k,n) -BitSubtracterOutput (x,y) iff ex i being Element of NAT st
( k = i + 1 & b5 = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) ) );

theorem :: FSCIRC_2:10
for n, k being Element of NAT st k < n holds
for x, y being FinSequence holds ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y)))
proof
let n, k be Element of NAT ; ::_thesis: ( k < n implies for x, y being FinSequence holds ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y))) )
assume A1: k < n ; ::_thesis: for x, y being FinSequence holds ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y)))
let x, y be FinSequence; ::_thesis: ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y)))
A2: k + 1 >= 1 by NAT_1:11;
 k + 1 <= n by A1, NAT_1:13;
then  ex i being Element of NAT st
( k + 1 = i + 1 & ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(i -BitBorrowOutput (x,y))) ) by A2, Def4;
hence  ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y))) ; ::_thesis: verum
end;

theorem :: FSCIRC_2:11
for n being Element of NAT
for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) is Relation
proof
let n be Element of NAT ; ::_thesis: for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) is Relation
let x, y be FinSequence; ::_thesis: InnerVertices (n -BitSubtracterStr (x,y)) is Relation
defpred S1[ Element of NAT ] means  InnerVertices ($1 -BitSubtracterStr (x,y)) is Relation;
 0 -BitSubtracterStr (x,y) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by Th2;
then A1: S1[ 0 ] by FACIRC_1:38;
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A3: S1[i] ; ::_thesis: S1[i + 1]
A4: (i + 1) -BitSubtracterStr (x,y) = (i -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y)))) by Th7;
 InnerVertices (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y)))) is Relation by FSCIRC_1:22;
hence  S1[i + 1] by A3, A4, FACIRC_1:3; ::_thesis: verum
end;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A1, A2);
hence  InnerVertices (n -BitSubtracterStr (x,y)) is Relation ; ::_thesis: verum
end;

theorem Th12: :: FSCIRC_2:12
for x, y, c being set holds InnerVertices (BorrowIStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}
proof
let x, y, c be set ; ::_thesis: InnerVertices (BorrowIStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}
A1: (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) tolerates 1GateCircStr (<*x,c*>,and2a) by CIRCCOMB:47;
A2: 1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,c*>,and2) by CIRCCOMB:47;
InnerVertices (BorrowIStr (x,y,c)) = (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a))) by A1, CIRCCOMB:11
.= ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a))) by A2, CIRCCOMB:11
.= ({[<*x,y*>,and2a]} \/ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a))) by CIRCCOMB:42
.= ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a))) by CIRCCOMB:42
.= ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]} by CIRCCOMB:42
.= {[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:1
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by ENUMSET1:3 ;
hence  InnerVertices (BorrowIStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} ; ::_thesis: verum
end;

theorem Th13: :: FSCIRC_2:13
for x, y, c being set st x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] holds
InputVertices (BorrowIStr (x,y,c)) = {x,y,c}
proof
let x, y, c be set ; ::_thesis: ( x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] implies InputVertices (BorrowIStr (x,y,c)) = {x,y,c} )
assume that
A1: x <> [<*y,c*>,and2] and
A2: y <> [<*x,c*>,and2a] and
A3: c <> [<*x,y*>,and2a] ; ::_thesis: InputVertices (BorrowIStr (x,y,c)) = {x,y,c}
A4: 1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,c*>,and2) by CIRCCOMB:47;
A5: y in {1,y} by TARSKI:def_2;
A6: y in {2,y} by TARSKI:def_2;
A7: {1,y} in [1,y] by TARSKI:def_2;
A8: {2,y} in [2,y] by TARSKI:def_2;
 <*y,c*> = <*y*> ^ <*c*> by FINSEQ_1:def_9;
then A9: <*y*> c= <*y,c*> by FINSEQ_6:10;
 <*y*> = {[1,y]} by FINSEQ_1:def_5;
then A10: [1,y] in <*y*> by TARSKI:def_1;
A11: <*y,c*> in {<*y,c*>} by TARSKI:def_1;
A12: {<*y,c*>} in [<*y,c*>,and2] by TARSKI:def_2;
then A13: y <> [<*y,c*>,and2] by A5, A7, A9, A10, A11, XREGULAR:9;
A14: c in {2,c} by TARSKI:def_2;
A15: {2,c} in [2,c] by TARSKI:def_2;
 dom <*y,c*> = Seg 2 by FINSEQ_1:89;
then A16: 2 in dom <*y,c*> by FINSEQ_1:1;
 <*y,c*> . 2 = c by FINSEQ_1:44;
then  [2,c] in <*y,c*> by A16, FUNCT_1:1;
then A17: c <> [<*y,c*>,and2] by A11, A12, A14, A15, XREGULAR:9;
 dom <*x,y*> = Seg 2 by FINSEQ_1:89;
then A18: 2 in dom <*x,y*> by FINSEQ_1:1;
 <*x,y*> . 2 = y by FINSEQ_1:44;
then A19: [2,y] in <*x,y*> by A18, FUNCT_1:1;
A20: <*x,y*> in {<*x,y*>} by TARSKI:def_1;
 {<*x,y*>} in [<*x,y*>,and2a] by TARSKI:def_2;
then  y <> [<*x,y*>,and2a] by A6, A8, A19, A20, XREGULAR:9;
then A21: not [<*x,y*>,and2a] in {y,c} by A3, TARSKI:def_2;
A22: x in {1,x} by TARSKI:def_2;
A23: {1,x} in [1,x] by TARSKI:def_2;
 <*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def_9;
then A24: <*x*> c= <*x,y*> by FINSEQ_6:10;
 <*x*> = {[1,x]} by FINSEQ_1:def_5;
then A25: [1,x] in <*x*> by TARSKI:def_1;
A26: <*x,y*> in {<*x,y*>} by TARSKI:def_1;
 {<*x,y*>} in [<*x,y*>,and2a] by TARSKI:def_2;
then A27: x <> [<*x,y*>,and2a] by A22, A23, A24, A25, A26, XREGULAR:9;
A28: not c in {[<*x,y*>,and2a],[<*y,c*>,and2]} by A3, A17, TARSKI:def_2;
A29: not x in {[<*x,y*>,and2a],[<*y,c*>,and2]} by A1, A27, TARSKI:def_2;
A30: c in {2,c} by TARSKI:def_2;
A31: {2,c} in [2,c] by TARSKI:def_2;
 dom <*x,c*> = Seg 2 by FINSEQ_1:89;
then A32: 2 in dom <*x,c*> by FINSEQ_1:1;
 <*x,c*> . 2 = c by FINSEQ_1:44;
then A33: [2,c] in <*x,c*> by A32, FUNCT_1:1;
A34: <*x,c*> in {<*x,c*>} by TARSKI:def_1;
 {<*x,c*>} in [<*x,c*>,and2a] by TARSKI:def_2;
then A35: c <> [<*x,c*>,and2a] by A30, A31, A33, A34, XREGULAR:9;
A36: x in {1,x} by TARSKI:def_2;
A37: {1,x} in [1,x] by TARSKI:def_2;
 <*x,c*> = <*x*> ^ <*c*> by FINSEQ_1:def_9;
then A38: <*x*> c= <*x,c*> by FINSEQ_6:10;
 <*x*> = {[1,x]} by FINSEQ_1:def_5;
then A39: [1,x] in <*x*> by TARSKI:def_1;
A40: <*x,c*> in {<*x,c*>} by TARSKI:def_1;
 {<*x,c*>} in [<*x,c*>,and2a] by TARSKI:def_2;
then  x <> [<*x,c*>,and2a] by A36, A37, A38, A39, A40, XREGULAR:9;
then A41: not [<*x,c*>,and2a] in {x,y,c} by A2, A35, ENUMSET1:def_1;
InputVertices (BorrowIStr (x,y,c)) = ((InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))) by CIRCCMB2:5, CIRCCOMB:47
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))) by CIRCCMB2:5, CIRCCOMB:47
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by A4, CIRCCOMB:11
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ({[<*x,y*>,and2a]} \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by CIRCCOMB:42
.= ((({x,y} \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ({x,c} \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by ENUMSET1:1
.= (({x,y} \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by A1, A13, FACIRC_2:1
.= (({x,y} \/ {y,c}) \ {[<*x,c*>,and2a]}) \/ ({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by A21, ZFMISC_1:57
.= (({x,y} \/ {y,c}) \ {[<*x,c*>,and2a]}) \/ {x,c} by A28, A29, ZFMISC_1:63
.= ({x,y,y,c} \ {[<*x,c*>,and2a]}) \/ {x,c} by ENUMSET1:5
.= ({y,y,x,c} \ {[<*x,c*>,and2a]}) \/ {x,c} by ENUMSET1:67
.= ({y,x,c} \ {[<*x,c*>,and2a]}) \/ {x,c} by ENUMSET1:31
.= ({x,y,c} \ {[<*x,c*>,and2a]}) \/ {x,c} by ENUMSET1:58
.= {x,y,c} \/ {x,c} by A41, ZFMISC_1:57
.= {x,y,c,c,x} by ENUMSET1:9
.= {x,y,c,c} \/ {x} by ENUMSET1:10
.= {c,c,x,y} \/ {x} by ENUMSET1:73
.= {c,x,y} \/ {x} by ENUMSET1:31
.= {c,x,y,x} by ENUMSET1:6
.= {x,x,y,c} by ENUMSET1:70
.= {x,y,c} by ENUMSET1:31 ;
hence  InputVertices (BorrowIStr (x,y,c)) = {x,y,c} ; ::_thesis: verum
end;

theorem Th14: :: FSCIRC_2:14
for x, y, c being set holds InnerVertices (BorrowStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))}
proof
let x, y, c be set ; ::_thesis: InnerVertices (BorrowStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))}
set xy = [<*x,y*>,and2a];
set yc = [<*y,c*>,and2];
set xc = [<*x,c*>,and2a];
set Cxy = 1GateCircStr (<*x,y*>,and2a);
set Cyc = 1GateCircStr (<*y,c*>,and2);
set Cxc = 1GateCircStr (<*x,c*>,and2a);
set Cxyc = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3);
A1: 1GateCircStr (<*x,y*>,and2a) tolerates ((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a))) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) by CIRCCOMB:47;
A2: 1GateCircStr (<*y,c*>,and2) tolerates (1GateCircStr (<*x,c*>,and2a)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) by CIRCCOMB:47;
A3: 1GateCircStr (<*x,c*>,and2a) tolerates 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) by CIRCCOMB:47;
A4: InnerVertices ((1GateCircStr (<*y,c*>,and2)) +* ((1GateCircStr (<*x,c*>,and2a)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) = (InnerVertices (1GateCircStr (<*y,c*>,and2))) \/ (InnerVertices ((1GateCircStr (<*x,c*>,and2a)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) by A2, CIRCCOMB:11;
A5: InnerVertices ((1GateCircStr (<*x,c*>,and2a)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) = (InnerVertices (1GateCircStr (<*x,c*>,and2a))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by A3, CIRCCOMB:11;
thus  InnerVertices (BorrowStr (x,y,c)) = InnerVertices (((1GateCircStr (<*x,y*>,and2a)) +* ((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a)))) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by CIRCCOMB:6
.= InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a))) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) by CIRCCOMB:6
.= (InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a))) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) by A1, CIRCCOMB:11
.= (InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices ((1GateCircStr (<*y,c*>,and2)) +* ((1GateCircStr (<*x,c*>,and2a)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))))) by CIRCCOMB:6
.= ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ ((InnerVertices (1GateCircStr (<*x,c*>,and2a))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) by A4, A5, XBOOLE_1:4
.= (((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by XBOOLE_1:4
.= (({[<*x,y*>,and2a]} \/ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by CIRCCOMB:42
.= (({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by CIRCCOMB:42
.= (({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by CIRCCOMB:42
.= ({[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by ENUMSET1:1
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by ENUMSET1:3
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} by CIRCCOMB:42 ; ::_thesis: verum
end;

theorem Th15: :: FSCIRC_2:15
for x, y, c being set st x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] holds
InputVertices (BorrowStr (x,y,c)) = {x,y,c}
proof
let x, y, c be set ; ::_thesis: ( x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] implies InputVertices (BorrowStr (x,y,c)) = {x,y,c} )
set xy = [<*x,y*>,and2a];
set yc = [<*y,c*>,and2];
set xc = [<*x,c*>,and2a];
set S = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3);
A1: InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) = {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} by CIRCCOMB:42;
A2: InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) = rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by CIRCCOMB:42
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by FINSEQ_2:128 ;
set BI = BorrowIStr (x,y,c);
assume that
A3: x <> [<*y,c*>,and2] and
A4: y <> [<*x,c*>,and2a] and
A5: c <> [<*x,y*>,and2a] ; ::_thesis: InputVertices (BorrowStr (x,y,c)) = {x,y,c}
 rng <*x,c*> = {x,c} by FINSEQ_2:127;
then A6: x in rng <*x,c*> by TARSKI:def_2;
 len <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> = 3 by FINSEQ_1:45;
then A7: Seg 3 = dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by FINSEQ_1:def_3;
then A8: 3 in dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by FINSEQ_1:1;
 <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 3 = [<*x,c*>,and2a] by FINSEQ_1:45;
then  [3,[<*x,c*>,and2a]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A8, FUNCT_1:1;
then  [<*x,c*>,and2a] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by XTUPLE_0:def_13;
then A9: the_rank_of [<*x,c*>,and2a] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] by CLASSES1:82;
 rng <*x,y*> = {x,y} by FINSEQ_2:127;
then A10: y in rng <*x,y*> by TARSKI:def_2;
A11: 1 in dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A7, FINSEQ_1:1;
 <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 1 = [<*x,y*>,and2a] by FINSEQ_1:45;
then  [1,[<*x,y*>,and2a]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A11, FUNCT_1:1;
then  [<*x,y*>,and2a] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by XTUPLE_0:def_13;
then A12: the_rank_of [<*x,y*>,and2a] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] by CLASSES1:82;
 rng <*y,c*> = {y,c} by FINSEQ_2:127;
then A13: c in rng <*y,c*> by TARSKI:def_2;
A14: 2 in dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A7, FINSEQ_1:1;
 <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 2 = [<*y,c*>,and2] by FINSEQ_1:45;
then  [2,[<*y,c*>,and2]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A14, FUNCT_1:1;
then  [<*y,c*>,and2] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by XTUPLE_0:def_13;
then A15: the_rank_of [<*y,c*>,and2] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] by CLASSES1:82;
A16: {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} = {} by XBOOLE_1:37;
A17: {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} = {x,y,c}
proof
thus  {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} c= {x,y,c} ; :: according to XBOOLE_0:def_10 ::_thesis: {x,y,c} c= {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]}
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y,c} or a in {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} )
assume A18: a in {x,y,c} ; ::_thesis: a in {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]}
then  ( a = x or a = y or a = c ) by ENUMSET1:def_1;
then  a <> [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] by A6, A9, A10, A12, A13, A15, CLASSES1:82;
then  not a in {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} by TARSKI:def_1;
hence  a in {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} by A18, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  InputVertices (BorrowStr (x,y,c)) = ((InputVertices (BorrowIStr (x,y,c))) \ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (BorrowIStr (x,y,c)))) by CIRCCMB2:5, CIRCCOMB:47
.= {x,y,c} \/ ({[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \ (InnerVertices (BorrowIStr (x,y,c)))) by A1, A2, A3, A4, A5, A17, Th13
.= {x,y,c} \/ {} by A16, Th12
.= {x,y,c} ; ::_thesis: verum
end;

theorem Th16: :: FSCIRC_2:16
for x, y, c being set st x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] & c <> [<*x,y*>,'xor'] holds
InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c}
proof
let x, y, c be set ; ::_thesis: ( x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] & c <> [<*x,y*>,'xor'] implies InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} )
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'] ; ::_thesis: InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c}
A5: InputVertices (2GatesCircStr (x,y,c,'xor')) = {x,y,c} by A4, FACIRC_1:57;
 InputVertices (BorrowStr (x,y,c)) = {x,y,c} by A1, A2, A3, Th15;
hence  InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} by A5, CIRCCOMB:47, FACIRC_2:21; ::_thesis: verum
end;

theorem Th17: :: FSCIRC_2:17
for x, y, c being set holds InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))}
proof
let x, y, c be set ; ::_thesis: InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))}
 2GatesCircStr (x,y,c,'xor') tolerates BorrowStr (x,y,c) by CIRCCOMB:47;
then  InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = (InnerVertices (2GatesCircStr (x,y,c,'xor'))) \/ (InnerVertices (BorrowStr (x,y,c))) by CIRCCOMB:11
.= {[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ (InnerVertices (BorrowStr (x,y,c))) by FACIRC_1:56
.= {[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ ({[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))}) by Th14
.= ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} by XBOOLE_1:4 ;
hence  InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} ; ::_thesis: verum
end;

registration
let n be Element of NAT ;
let x, y be FinSequence;
clustern -BitBorrowOutput (x,y) ->  pair ;
coherence
 n -BitBorrowOutput (x,y) is pair
proof
A1: ex h being ManySortedSet of NAT st
( 0 -BitBorrowOutput (x,y) = h . 0 & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) by Def3;
defpred S1[ Element of NAT ] means n -BitBorrowOutput (x,y) is pair ;
A2: S1[ 0 ] by A1;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
(n + 1) -BitBorrowOutput (x,y) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))) by Th7
.= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2a],[<*(y . (n + 1)),(n -BitBorrowOutput (x,y))*>,and2],[<*(x . (n + 1)),(n -BitBorrowOutput (x,y))*>,and2a]*>,or3] ;
hence  ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A3);
hence  n -BitBorrowOutput (x,y) is pair ; ::_thesis: verum
end;
end;

theorem Th18: :: FSCIRC_2:18
for x, y being FinSequence
for n being Element of NAT holds
( ( (n -BitBorrowOutput (x,y)) `1 = <*> & (n -BitBorrowOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> TRUE & proj1 ((n -BitBorrowOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitBorrowOutput (x,y)) `1) = 3 & (n -BitBorrowOutput (x,y)) `2 = or3 & proj1 ((n -BitBorrowOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) )
proof
let x, y be FinSequence; ::_thesis: for n being Element of NAT holds
( ( (n -BitBorrowOutput (x,y)) `1 = <*> & (n -BitBorrowOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> TRUE & proj1 ((n -BitBorrowOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitBorrowOutput (x,y)) `1) = 3 & (n -BitBorrowOutput (x,y)) `2 = or3 & proj1 ((n -BitBorrowOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) )
defpred S1[ Element of NAT ] means ( ( ($1 -BitBorrowOutput (x,y)) `1 = <*> & ($1 -BitBorrowOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> TRUE & proj1 (($1 -BitBorrowOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card (($1 -BitBorrowOutput (x,y)) `1) = 3 & ($1 -BitBorrowOutput (x,y)) `2 = or3 & proj1 (($1 -BitBorrowOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) );
A1: dom ((0 -tuples_on BOOLEAN) --> TRUE) = 0 -tuples_on BOOLEAN by FUNCOP_1:13;
 0 -BitBorrowOutput (x,y) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by Th2;
then A2: S1[ 0 ] by A1, MCART_1:7;
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
set c = n -BitBorrowOutput (x,y);
A4: (n + 1) -BitBorrowOutput (x,y) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))) by Th7
.= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2a],[<*(y . (n + 1)),(n -BitBorrowOutput (x,y))*>,and2],[<*(x . (n + 1)),(n -BitBorrowOutput (x,y))*>,and2a]*>,or3] ;
A5: dom or3 = 3 -tuples_on BOOLEAN by FUNCT_2:def_1;
 ((n + 1) -BitBorrowOutput (x,y)) `1 = <*[<*(x . (n + 1)),(y . (n + 1))*>,and2a],[<*(y . (n + 1)),(n -BitBorrowOutput (x,y))*>,and2],[<*(x . (n + 1)),(n -BitBorrowOutput (x,y))*>,and2a]*> by A4, MCART_1:7;
hence  S1[n + 1] by A4, A5, FINSEQ_1:45, MCART_1:7; ::_thesis: verum
end;
thus  for i being Element of NAT holds S1[i] from NAT_1:sch_1(A2, A3); ::_thesis: verum
end;

theorem Th19: :: FSCIRC_2:19
for n being Element of NAT
for x, y being FinSequence
for p being set holds
( n -BitBorrowOutput (x,y) <> [p,and2] & n -BitBorrowOutput (x,y) <> [p,and2a] & n -BitBorrowOutput (x,y) <> [p,'xor'] )
proof
let n be Element of NAT ; ::_thesis: for x, y being FinSequence
for p being set holds
( n -BitBorrowOutput (x,y) <> [p,and2] & n -BitBorrowOutput (x,y) <> [p,and2a] & n -BitBorrowOutput (x,y) <> [p,'xor'] )
let x, y be FinSequence; ::_thesis: for p being set holds
( n -BitBorrowOutput (x,y) <> [p,and2] & n -BitBorrowOutput (x,y) <> [p,and2a] & n -BitBorrowOutput (x,y) <> [p,'xor'] )
let p be set ; ::_thesis: ( n -BitBorrowOutput (x,y) <> [p,and2] & n -BitBorrowOutput (x,y) <> [p,and2a] & n -BitBorrowOutput (x,y) <> [p,'xor'] )
A1: dom and2 = 2 -tuples_on BOOLEAN by FUNCT_2:def_1;
A2: dom and2a = 2 -tuples_on BOOLEAN by FUNCT_2:def_1;
A3: dom 'xor' = 2 -tuples_on BOOLEAN by FUNCT_2:def_1;
A4: proj1 ([p,and2] `2) = 2 -tuples_on BOOLEAN by A1;
A5: proj1 ([p,and2a] `2) = 2 -tuples_on BOOLEAN by A2;
A6: proj1 ([p,'xor'] `2) = 2 -tuples_on BOOLEAN by A3;
 ( proj1 ((n -BitBorrowOutput (x,y)) `2) = 0 -tuples_on BOOLEAN or proj1 ((n -BitBorrowOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) by Th18;
hence  ( n -BitBorrowOutput (x,y) <> [p,and2] & n -BitBorrowOutput (x,y) <> [p,and2a] & n -BitBorrowOutput (x,y) <> [p,'xor'] ) by A4, A5, A6, FINSEQ_2:110; ::_thesis: verum
end;

theorem Th20: :: FSCIRC_2:20
for f, g being nonpair-yielding FinSequence
for n being Element of NAT holds
( InputVertices ((n + 1) -BitSubtracterStr (f,g)) = (InputVertices (n -BitSubtracterStr (f,g))) \/ ((InputVertices (BitSubtracterWithBorrowStr ((f . (n + 1)),(g . (n + 1)),(n -BitBorrowOutput (f,g))))) \ {(n -BitBorrowOutput (f,g))}) & InnerVertices (n -BitSubtracterStr (f,g)) is Relation & InputVertices (n -BitSubtracterStr (f,g)) is without_pairs )
proof
let f, g be nonpair-yielding FinSequence; ::_thesis: for n being Element of NAT holds
( InputVertices ((n + 1) -BitSubtracterStr (f,g)) = (InputVertices (n -BitSubtracterStr (f,g))) \/ ((InputVertices (BitSubtracterWithBorrowStr ((f . (n + 1)),(g . (n + 1)),(n -BitBorrowOutput (f,g))))) \ {(n -BitBorrowOutput (f,g))}) & InnerVertices (n -BitSubtracterStr (f,g)) is Relation & InputVertices (n -BitSubtracterStr (f,g)) is without_pairs )
deffunc H1( Nat) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitSubtracterStr (f,g);
deffunc H2( set , Nat) ->  ManySortedSign = BitSubtracterWithBorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H3( Nat) ->  Element of InnerVertices ($1 -BitSubtracterStr (f,g)) = $1 -BitBorrowOutput (f,g);
consider h being ManySortedSet of NAT  such that
A1: for n being Element of NAT holds h . n = H3(n) from PBOOLE:sch_5();
deffunc H4( Nat) ->  set = h . $1;
deffunc H5( set , Nat) ->  Element of InnerVertices (BorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = BorrowOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1);
set k = (0 -tuples_on BOOLEAN) --> TRUE;
A2: 0 -BitSubtracterStr (f,g) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by Th2;
then A3: InnerVertices H1( 0 ) is Relation by FACIRC_1:38;
A4: InputVertices H1( 0 ) is without_pairs by A2, FACIRC_1:39;
 H4( 0 ) = 0 -BitBorrowOutput (f,g) by A1;
then A5: h . 0 in InnerVertices H1( 0 ) ;
A6: for n being Nat
for x being set holds InnerVertices H2(x,n) is Relation by FSCIRC_1:22;
A7: now__::_thesis:_for_n_being_Element_of_NAT_
for_x_being_set_st_x_=_H4(n)_holds_
InputVertices_H2(x,n)_=_{(f_._(n_+_1)),(g_._(n_+_1)),x}
let n be Element of NAT ; ::_thesis: for x being set st x = H4(n) holds
InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x}
let x be set ; ::_thesis: ( x = H4(n) implies InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} )
assume A8: x = H4(n) ; ::_thesis: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x}
A9: H4(n) = n -BitBorrowOutput (f,g) by A1;
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  InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A10, Th16; ::_thesis: verum
end;
A11: for n being Nat
for x being set st x = h . n holds
(InputVertices H2(x,n)) \ {x} is without_pairs
proof
let n be Nat; ::_thesis: for x being set st x = h . n holds
(InputVertices H2(x,n)) \ {x} is without_pairs
let x be set ; ::_thesis: ( x = h . n implies (InputVertices H2(x,n)) \ {x} is without_pairs )
assume A12: x = H4(n) ; ::_thesis: (InputVertices H2(x,n)) \ {x} is without_pairs
 n in NAT by ORDINAL1:def_12;
then A13: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7, A12;
thus  (InputVertices H2(x,n)) \ {x} is without_pairs ::_thesis: verum
proof
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in (InputVertices H2(x,n)) \ {x}
assume A14: a in (InputVertices H2(x,n)) \ {x} ; ::_thesis: contradiction
then  a in InputVertices H2(x,n) by XBOOLE_0:def_5;
then A15: ( a = f . (n + 1) or a = g . (n + 1) or a = x ) by A13, ENUMSET1:def_1;
 not a in {x} by A14, XBOOLE_0:def_5;
hence  contradiction by A15, TARSKI:def_1; ::_thesis: verum
end;
end;
A16: now__::_thesis:_for_n_being_Nat
for_S_being_non_empty_ManySortedSign_
for_x_being_set_st_S_=_H1(n)_&_x_=_h_._n_holds_
(_H1(n_+_1)_=_S_+*_H2(x,n)_&_h_._(n_+_1)_=_H5(x,n)_&_x_in_InputVertices_H2(x,n)_&_H5(x,n)_in_InnerVertices_H2(x,n)_)
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for x being set st S = H1(n) & x = h . n holds
( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
let S be non empty ManySortedSign ; ::_thesis: for x being set st S = H1(n) & x = h . n holds
( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
let x be set ; ::_thesis: ( S = H1(n) & x = h . n implies ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) )
A17: n in NAT by ORDINAL1:def_12;
assume that
A18: S = H1(n) and
A19: x = h . n ; ::_thesis: ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
A20: x = n -BitBorrowOutput (f,g) by A1, A17, A19;
A21: H4(n + 1) = (n + 1) -BitBorrowOutput (f,g) by A1;
thus  H1(n + 1) = S +* H2(x,n) by A17, A18, A20, Th7; ::_thesis: ( h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
thus  h . (n + 1) = H5(x,n) by A17, A20, A21, Th7; ::_thesis: ( x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
 InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7, A17, A19;
hence  x in InputVertices H2(x,n) by ENUMSET1:def_1; ::_thesis: H5(x,n) in InnerVertices H2(x,n)
A22: InnerVertices H2(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;
 H5(x,n) in {H5(x,n)} by TARSKI:def_1;
hence  H5(x,n) in InnerVertices H2(x,n) by A22, XBOOLE_0:def_3; ::_thesis: verum
end;
A23: for n being Nat holds
( InputVertices H1(n + 1) = (InputVertices H1(n)) \/ ((InputVertices H2(h . n,n)) \ {(h . n)}) & InnerVertices H1(n) is Relation & InputVertices H1(n) is without_pairs ) from CIRCCMB2:sch_11(A3, A4, A5, A6, A11, A16);
let n be Element of NAT ; ::_thesis: ( InputVertices ((n + 1) -BitSubtracterStr (f,g)) = (InputVertices (n -BitSubtracterStr (f,g))) \/ ((InputVertices (BitSubtracterWithBorrowStr ((f . (n + 1)),(g . (n + 1)),(n -BitBorrowOutput (f,g))))) \ {(n -BitBorrowOutput (f,g))}) & InnerVertices (n -BitSubtracterStr (f,g)) is Relation & InputVertices (n -BitSubtracterStr (f,g)) is without_pairs )
 h . n = n -BitBorrowOutput (f,g) by A1;
hence  ( InputVertices ((n + 1) -BitSubtracterStr (f,g)) = (InputVertices (n -BitSubtracterStr (f,g))) \/ ((InputVertices (BitSubtracterWithBorrowStr ((f . (n + 1)),(g . (n + 1)),(n -BitBorrowOutput (f,g))))) \ {(n -BitBorrowOutput (f,g))}) & InnerVertices (n -BitSubtracterStr (f,g)) is Relation & InputVertices (n -BitSubtracterStr (f,g)) is without_pairs ) by A23; ::_thesis: verum
end;

theorem :: FSCIRC_2:21
for n being Element of NAT
for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitSubtracterStr (x,y)) = (rng x) \/ (rng y)
proof
defpred S1[ Element of NAT ] means  for x, y being nonpair-yielding FinSeqLen of $1 holds InputVertices ($1 -BitSubtracterStr (x,y)) = (rng x) \/ (rng y);
A1: S1[ 0 ]
proof
let x, y be nonpair-yielding FinSeqLen of 0 ; ::_thesis: InputVertices (0 -BitSubtracterStr (x,y)) = (rng x) \/ (rng y)
set f = (0 -tuples_on BOOLEAN) --> TRUE;
 0 -BitSubtracterStr (x,y) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by Th2;
hence  InputVertices (0 -BitSubtracterStr (x,y)) = rng <*> by CIRCCOMB:42
.= (rng x) \/ (rng y) ;
::_thesis: verum
end;
A2: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A3: S1[i] ; ::_thesis: S1[i + 1]
let x, y be nonpair-yielding FinSeqLen of i + 1; ::_thesis: InputVertices ((i + 1) -BitSubtracterStr (x,y)) = (rng x) \/ (rng y)
consider x9 being nonpair-yielding FinSeqLen of i, z1 being non pair set  such that
A4: x = x9 ^ <*z1*> by FACIRC_2:34;
consider y9 being nonpair-yielding FinSeqLen of i, z2 being non pair set  such that
A5: y = y9 ^ <*z2*> by FACIRC_2:34;
set S = (i + 1) -BitSubtracterStr (x,y);
A6: 1 in Seg 1 by FINSEQ_1:1;
then A7: 1 in dom <*z1*> by FINSEQ_1:def_8;
 len x9 = i by CARD_1:def_7;
then A8: x . (i + 1) = <*z1*> . 1 by A4, A7, FINSEQ_1:def_7
.= z1 by FINSEQ_1:def_8 ;
A9: 1 in dom <*z2*> by A6, FINSEQ_1:def_8;
 len y9 = i by CARD_1:def_7;
then A10: y . (i + 1) = <*z2*> . 1 by A5, A9, FINSEQ_1:def_7
.= z2 by FINSEQ_1:def_8 ;
A11: {z1,z2,(i -BitBorrowOutput (x,y))} = {(i -BitBorrowOutput (x,y)),z1,z2} by ENUMSET1:59;
A12: rng x = (rng x9) \/ (rng <*z1*>) by A4, FINSEQ_1:31
.= (rng x9) \/ {z1} by FINSEQ_1:38 ;
A13: rng y = (rng y9) \/ (rng <*z2*>) by A5, FINSEQ_1:31
.= (rng y9) \/ {z2} by FINSEQ_1:38 ;
A14: i -BitBorrowOutput (x,y) <> [<*z1,z2*>,and2a] by Th19;
A15: i -BitBorrowOutput (x,y) <> [<*z1,z2*>,'xor'] by Th19;
A16: x9 = x9 ^ {} by FINSEQ_1:34;
 y9 = y9 ^ {} by FINSEQ_1:34;
then  i -BitSubtracterStr (x,y) = i -BitSubtracterStr (x9,y9) by A4, A5, A16, Th5;
hence  InputVertices ((i + 1) -BitSubtracterStr (x,y)) = (InputVertices (i -BitSubtracterStr (x9,y9))) \/ ((InputVertices (BitSubtracterWithBorrowStr (z1,z2,(i -BitBorrowOutput (x,y))))) \ {(i -BitBorrowOutput (x,y))}) by A8, A10, Th20
.= ((rng x9) \/ (rng y9)) \/ ((InputVertices (BitSubtracterWithBorrowStr (z1,z2,(i -BitBorrowOutput (x,y))))) \ {(i -BitBorrowOutput (x,y))}) by A3
.= ((rng x9) \/ (rng y9)) \/ ({z1,z2,(i -BitBorrowOutput (x,y))} \ {(i -BitBorrowOutput (x,y))}) by A14, A15, Th16
.= ((rng x9) \/ (rng y9)) \/ {z1,z2} by A11, ENUMSET1:86
.= ((rng x9) \/ (rng y9)) \/ ({z1} \/ {z2}) by ENUMSET1:1
.= (((rng x9) \/ (rng y9)) \/ {z1}) \/ {z2} by XBOOLE_1:4
.= (((rng x9) \/ {z1}) \/ (rng y9)) \/ {z2} by XBOOLE_1:4
.= (rng x) \/ (rng y) by A12, A13, XBOOLE_1:4 ;
::_thesis: verum
end;
thus  for i being Element of NAT holds S1[i] from NAT_1:sch_1(A1, A2); ::_thesis: verum
end;

Lm1:  for x, y, c being set
for s being State of (BorrowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
proof
let x, y, c be set ; ::_thesis: for s being State of (BorrowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
let s be State of (BorrowCirc (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) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) )
assume that
A1: a1 = s . x and
A2: a2 = s . y and
A3: a3 = s . c ; ::_thesis: ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
set S = BorrowStr (x,y,c);
A4: InnerVertices (BorrowStr (x,y,c)) = the carrier' of (BorrowStr (x,y,c)) by FACIRC_1:37;
A5: dom s = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3;
A6: x in the carrier of (BorrowStr (x,y,c)) by FSCIRC_1:6;
A7: y in the carrier of (BorrowStr (x,y,c)) by FSCIRC_1:6;
A8: c in the carrier of (BorrowStr (x,y,c)) by FSCIRC_1:6;
 [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) by FSCIRC_1:7;
hence (Following s) . [<*x,y*>,and2a] = and2a . (s * <*x,y*>) by A4, FACIRC_1:35
.= and2a . <*a1,a2*> by A1, A2, A5, A6, A7, FINSEQ_2:125
.= ('not' a1) '&' a2 by TWOSCOMP:def_2 ;
::_thesis: ( (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
 [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) by FSCIRC_1:7;
hence (Following s) . [<*y,c*>,and2] = and2 . (s * <*y,c*>) by A4, FACIRC_1:35
.= and2 . <*a2,a3*> by A2, A3, A5, A7, A8, FINSEQ_2:125
.= a2 '&' a3 by TWOSCOMP:def_1 ;
::_thesis: (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3
 [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) by FSCIRC_1:7;
hence (Following s) . [<*x,c*>,and2a] = and2a . (s * <*x,c*>) by A4, FACIRC_1:35
.= and2a . <*a1,a3*> by A1, A3, A5, A6, A8, FINSEQ_2:125
.= ('not' a1) '&' a3 by TWOSCOMP:def_2 ;
::_thesis: verum
end;

theorem Th22: :: FSCIRC_2:22
for x, y, c being set
for s being State of (BorrowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] holds
(Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3
proof
let x, y, c be set ; ::_thesis: for s being State of (BorrowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] holds
(Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3
let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] holds
(Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] implies (Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3 )
assume that
A1: a1 = s . [<*x,y*>,and2a] and
A2: a2 = s . [<*y,c*>,and2] and
A3: a3 = s . [<*x,c*>,and2a] ; ::_thesis: (Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3
set xy = [<*x,y*>,and2a];
set yc = [<*y,c*>,and2];
set cx = [<*x,c*>,and2a];
set S = BorrowStr (x,y,c);
A4: InnerVertices (BorrowStr (x,y,c)) = the carrier' of (BorrowStr (x,y,c)) by FACIRC_1:37;
A5: dom s = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3;
reconsider xy = [<*x,y*>,and2a], yc = [<*y,c*>,and2], cx = [<*x,c*>,and2a] as Element of InnerVertices (BorrowStr (x,y,c)) by FSCIRC_1:7;
thus (Following s) . (BorrowOutput (x,y,c)) = or3 . (s * <*xy,yc,cx*>) by A4, FACIRC_1:35
.= or3 . <*a1,a2,a3*> by A1, A2, A3, A5, FINSEQ_2:126
.= (a1 'or' a2) 'or' a3 by FACIRC_1:def_7 ; ::_thesis: verum
end;

Lm2:  for x, y, c being set st x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] holds
for s being State of (BorrowCirc (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)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
proof
let x, y, c be set ; ::_thesis: ( x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] implies for s being State of (BorrowCirc (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)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) )
assume that
A1: x <> [<*y,c*>,and2] and
A2: y <> [<*x,c*>,and2a] and
A3: c <> [<*x,y*>,and2a] ; ::_thesis: for s being State of (BorrowCirc (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)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
let s be State of (BorrowCirc (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)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('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)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) )
assume that
A4: a1 = s . x and
A5: a2 = s . y and
A6: a3 = s . c ; ::_thesis: ( (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
set xy = [<*x,y*>,and2a];
set yc = [<*y,c*>,and2];
set cx = [<*x,c*>,and2a];
set S = BorrowStr (x,y,c);
reconsider x9 = x, y9 = y, c9 = c as Vertex of (BorrowStr (x,y,c)) by FSCIRC_1:6;
A7: InputVertices (BorrowStr (x,y,c)) = {x,y,c} by A1, A2, A3, Th15;
then A8: x in InputVertices (BorrowStr (x,y,c)) by ENUMSET1:def_1;
A9: y in InputVertices (BorrowStr (x,y,c)) by A7, ENUMSET1:def_1;
A10: c in InputVertices (BorrowStr (x,y,c)) by A7, ENUMSET1:def_1;
A11: (Following s) . x9 = s . x by A8, CIRCUIT2:def_5;
A12: (Following s) . y9 = s . y by A9, CIRCUIT2:def_5;
A13: (Following s) . c9 = s . c by A10, CIRCUIT2:def_5;
A14: Following (s,2) = Following (Following s) by FACIRC_1:15;
A15: (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 by A4, A5, A6, Lm1;
A16: (Following s) . [<*y,c*>,and2] = a2 '&' a3 by A4, A5, A6, Lm1;
 (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 by A4, A5, A6, Lm1;
hence  (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) by A14, A15, A16, Th22; ::_thesis: ( (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
thus  ( (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) by A4, A5, A6, A11, A12, A13, A14, Lm1; ::_thesis: verum
end;

theorem Th23: :: FSCIRC_2:23
for x, y, c being set st x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] holds
for s being State of (BorrowCirc (x,y,c)) holds Following (s,2) is stable
proof
let x, y, c be set ; ::_thesis: ( x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] implies for s being State of (BorrowCirc (x,y,c)) holds Following (s,2) is stable )
set S = BorrowStr (x,y,c);
assume that
A1: x <> [<*y,c*>,and2] and
A2: y <> [<*x,c*>,and2a] and
A3: c <> [<*x,y*>,and2a] ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) holds Following (s,2) is stable
let s be State of (BorrowCirc (x,y,c)); ::_thesis: Following (s,2) is stable
A4: dom (Following (Following (s,2))) = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3;
A5: dom (Following (s,2)) = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3;
reconsider xx = x, yy = y, cc = c as Vertex of (BorrowStr (x,y,c)) by FSCIRC_1:6;
set a1 = s . xx;
set a2 = s . yy;
set a3 = s . cc;
set ffs = Following (s,2);
set fffs = Following (Following (s,2));
A6: s . xx = s . x ;
A7: s . yy = s . y ;
A8: s . cc = s . c ;
A9: (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' (s . xx)) '&' (s . yy)) 'or' ((s . yy) '&' (s . cc))) 'or' (('not' (s . xx)) '&' (s . cc)) by A1, A2, A3, Lm2;
A10: (Following (s,2)) . [<*x,y*>,and2a] = ('not' (s . xx)) '&' (s . yy) by A1, A2, A3, A8, Lm2;
A11: (Following (s,2)) . [<*y,c*>,and2] = (s . yy) '&' (s . cc) by A1, A2, A3, A6, Lm2;
A12: (Following (s,2)) . [<*x,c*>,and2a] = ('not' (s . xx)) '&' (s . cc) by A1, A2, A3, A7, Lm2;
A13: Following (s,2) = Following (Following s) by FACIRC_1:15;
A14: InputVertices (BorrowStr (x,y,c)) = {x,y,c} by A1, A2, A3, Th15;
then A15: x in InputVertices (BorrowStr (x,y,c)) by ENUMSET1:def_1;
A16: y in InputVertices (BorrowStr (x,y,c)) by A14, ENUMSET1:def_1;
A17: c in InputVertices (BorrowStr (x,y,c)) by A14, ENUMSET1:def_1;
A18: (Following s) . x = s . xx by A15, CIRCUIT2:def_5;
A19: (Following s) . y = s . yy by A16, CIRCUIT2:def_5;
A20: (Following s) . c = s . cc by A17, CIRCUIT2:def_5;
A21: (Following (s,2)) . x = s . xx by A13, A15, A18, CIRCUIT2:def_5;
A22: (Following (s,2)) . y = s . yy by A13, A16, A19, CIRCUIT2:def_5;
A23: (Following (s,2)) . c = s . cc by A13, A17, A20, CIRCUIT2:def_5;
now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(BorrowStr_(x,y,c))_holds_
(Following_(s,2))_._a_=_(Following_(Following_(s,2)))_._a
let a be set ; ::_thesis: ( a in the carrier of (BorrowStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )
assume A24: a in the carrier of (BorrowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then reconsider v = a as Vertex of (BorrowStr (x,y,c)) ;
A25: v in (InputVertices (BorrowStr (x,y,c))) \/ (InnerVertices (BorrowStr (x,y,c))) by A24, XBOOLE_1:45;
thus  (Following (s,2)) . a = (Following (Following (s,2))) . a ::_thesis: verum
proof
percases ( v in InputVertices (BorrowStr (x,y,c)) or v in InnerVertices (BorrowStr (x,y,c)) ) by A25, XBOOLE_0:def_3;
suppose v in InputVertices (BorrowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
hence  (Following (s,2)) . a = (Following (Following (s,2))) . a by CIRCUIT2:def_5; ::_thesis: verum
end;
suppose v in InnerVertices (BorrowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then  v in {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} by Th14;
then  ( v in {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} or v in {(BorrowOutput (x,y,c))} ) by XBOOLE_0:def_3;
then  ( v = [<*x,y*>,and2a] or v = [<*y,c*>,and2] or v = [<*x,c*>,and2a] or v = BorrowOutput (x,y,c) ) by ENUMSET1:def_1, TARSKI:def_1;
hence  (Following (s,2)) . a = (Following (Following (s,2))) . a by A9, A10, A11, A12, A21, A22, A23, Lm1, Th22; ::_thesis: verum
end;
end;
end;
end;
hence  Following (s,2) = Following (Following (s,2)) by A4, A5, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem :: FSCIRC_2:24
for x, y, c being set st x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] & c <> [<*x,y*>,'xor'] holds
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) )
proof
let x, y, c be set ; ::_thesis: ( 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'] ; ::_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 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)); ::_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
A5: a1 = s . x and
A6: a2 = s . y and
A7: 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) )
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; ::_thesis: (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; ::_thesis: verum
end;

theorem Th25: :: FSCIRC_2:25
for x, y, c being set st x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] & c <> [<*x,y*>,'xor'] holds
for s being State of (BitSubtracterWithBorrowCirc (x,y,c)) holds Following (s,2) is stable
proof
let x, y, c be set ; ::_thesis: ( 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)) holds Following (s,2) is stable )
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'] ; ::_thesis: 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)); ::_thesis: 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))) ;
A5: InputVertices (BorrowStr (x,y,c)) = {x,y,c} by A1, A2, A3, Th15;
A6: InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by XBOOLE_1:79;
A7: InnerVertices (BorrowStr (x,y,c)) misses InputVertices (BorrowStr (x,y,c)) by XBOOLE_1:79;
A8: InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (BorrowStr (x,y,c)) by A4, A5, A6, FACIRC_1:57;
A9: InnerVertices (BorrowStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by A4, A5, A7, FACIRC_1:57;
then A10: Following (s1,2) = (Following (t,2)) | the carrier of (2GatesCircStr (x,y,c,'xor')) by FACIRC_1:30;
A11: Following (s1,3) = (Following (t,3)) | the carrier of (2GatesCircStr (x,y,c,'xor')) by A9, FACIRC_1:30;
A12: Following (s2,2) = (Following (t,2)) | the carrier of (BorrowStr (x,y,c)) by A8, FACIRC_1:31;
A13: Following (s2,3) = (Following (t,3)) | the carrier of (BorrowStr (x,y,c)) by A8, FACIRC_1:31;
 Following (s1,2) is stable by A4, FACIRC_1:63;
then A14: Following (s1,2) = Following (Following (s1,2)) by CIRCUIT2:def_6
.= Following (s1,(2 + 1)) by FACIRC_1:12 ;
 Following (s2,2) is stable by A1, A2, A3, Th23;
then A15: Following (s2,2) = Following (Following (s2,2)) by CIRCUIT2:def_6
.= Following (s2,(2 + 1)) by FACIRC_1:12 ;
A16: Following (s,(2 + 1)) = Following (Following (s,2)) by FACIRC_1:12;
A17: dom (Following (s,2)) = the carrier of (BitSubtracterWithBorrowStr (x,y,c)) by CIRCUIT1:3;
A18: dom (Following (s,3)) = the carrier of (BitSubtracterWithBorrowStr (x,y,c)) by CIRCUIT1:3;
A19: dom (Following (s1,2)) = the carrier of (2GatesCircStr (x,y,c,'xor')) by CIRCUIT1:3;
A20: dom (Following (s2,2)) = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3;
A21: 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;
now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(BitSubtracterWithBorrowStr_(x,y,c))_holds_
(Following_(s,2))_._a_=_(Following_(Following_(s,2)))_._a
let a be set ; ::_thesis: ( 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)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then  ( a in the carrier of (2GatesCircStr (x,y,c,'xor')) or a in the carrier of (BorrowStr (x,y,c)) ) by A21, 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 A10, A11, A12, A13, A14, A15, A19, A20, FUNCT_1:47;
hence  (Following (s,2)) . a = (Following (Following (s,2))) . a by A14, A15, FACIRC_1:12; ::_thesis: verum
end;
hence  Following (s,2) = Following (Following (s,2)) by A16, A17, A18, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem :: FSCIRC_2:26
for n being Element of NAT
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
proof
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 over 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__::_thesis:_for_s_being_State_of_(1GateCircuit_(<*>,((0_-tuples_on_BOOLEAN)_-->_TRUE)))_holds_Following_(s,H4(_0_))_is_stable
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 over 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__::_thesis:_for_i_being_set_st_i_in_NAT_holds_
h1_._i_=_h_._i
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 over S
for x being set
for A2 being non-empty MSAlgebra over 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 over S
for x being set
for A2 being non-empty MSAlgebra over 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 over S
for x being set
for A2 being non-empty MSAlgebra over 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 over S
for x being set
for A2 being non-empty MSAlgebra over 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 & InputVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) is without_pairs ) 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
(InputVertices H1(x,n)) \ {x} is without_pairs
proof
let n be Nat; ::_thesis: for x being set st x = h . n holds
(InputVertices H1(x,n)) \ {x} is without_pairs
let x be set ; ::_thesis: ( x = h . n implies (InputVertices H1(x,n)) \ {x} is without_pairs )
assume A24: x = h . n ; ::_thesis: (InputVertices H1(x,n)) \ {x} is without_pairs
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
end;