:: 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;