:: FSCIRC_1 semantic presentation begin definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BitSubtracterOutput"::: "(" "x" "," "y" "," "c" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" )) equals :: FSCIRC_1:def 1 (Set ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ); end; :: deftheorem defines :::"BitSubtracterOutput"::: FSCIRC_1:def 1 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_fscirc_1 :::"BitSubtracterOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BitSubtracterCirc"::: "(" "x" "," "y" "," "c" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ) equals :: FSCIRC_1:def 2 (Set ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ); end; :: deftheorem defines :::"BitSubtracterCirc"::: FSCIRC_1:def 2 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_fscirc_1 :::"BitSubtracterCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_facirc_1 :::"2GatesCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BorrowIStr"::: "(" "x" "," "y" "," "c" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FSCIRC_1:def 3 (Set (Set "(" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "y" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ")" ")" ) ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ")" )); end; :: deftheorem defines :::"BorrowIStr"::: FSCIRC_1:def 3 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_fscirc_1 :::"BorrowIStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ")" ")" ) ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ")" )))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BorrowStr"::: "(" "x" "," "y" "," "c" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FSCIRC_1:def 4 (Set (Set "(" ($#k3_fscirc_1 :::"BorrowIStr"::: ) "(" "x" "," "y" "," "c" ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "y" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ")" ")" )); end; :: deftheorem defines :::"BorrowStr"::: FSCIRC_1:def 4 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_fscirc_1 :::"BorrowIStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ")" ")" )))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BorrowICirc"::: "(" "x" "," "y" "," "c" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k3_fscirc_1 :::"BorrowIStr"::: ) "(" "x" "," "y" "," "c" ")" ) equals :: FSCIRC_1:def 5 (Set (Set "(" (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "x" "," "y" "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "y" "," "c" "," (Set ($#k2_twoscomp :::"and2"::: ) ) ")" ")" ) ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "x" "," "c" "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ")" )); end; :: deftheorem defines :::"BorrowICirc"::: FSCIRC_1:def 5 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_fscirc_1 :::"BorrowICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ")" ")" ) ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "c")) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ")" )))); theorem :: FSCIRC_1:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FSCIRC_1:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; theorem :: FSCIRC_1:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k5_fscirc_1 :::"BorrowICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "b"))))))) ; theorem :: FSCIRC_1:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k5_fscirc_1 :::"BorrowICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "b"))))))) ; theorem :: FSCIRC_1:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k5_fscirc_1 :::"BorrowICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "b"))))))) ; definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BorrowOutput"::: "(" "x" "," "y" "," "c" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" "x" "," "y" "," "c" ")" ")" )) equals :: FSCIRC_1:def 6 (Set ($#k4_tarski :::"["::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "y" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"BorrowOutput"::: FSCIRC_1:def 6 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_fscirc_1 :::"BorrowOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ($#k4_tarski :::"]"::: ) ))); definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BorrowCirc"::: "(" "x" "," "y" "," "c" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" "x" "," "y" "," "c" ")" ) equals :: FSCIRC_1:def 7 (Set (Set "(" ($#k5_fscirc_1 :::"BorrowICirc"::: ) "(" "x" "," "y" "," "c" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k7_facirc_1 :::"1GateCircuit"::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "y" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "y" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "c" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ")" ")" )); end; :: deftheorem defines :::"BorrowCirc"::: FSCIRC_1:def 7 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_fscirc_1 :::"BorrowICirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k7_facirc_1 :::"1GateCircuit"::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_facirc_1 :::"or3"::: ) ) ")" ")" )))); theorem :: FSCIRC_1:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) ")" )) ; theorem :: FSCIRC_1:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) ")" )) ; theorem :: FSCIRC_1:8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ))) ")" )) ; theorem :: FSCIRC_1:9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_fscirc_1 :::"BorrowOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k1_tarski :::"}"::: ) ))) ")" )) ; theorem :: FSCIRC_1:10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2"))))))) ; theorem :: FSCIRC_1:11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3"))))))) ; theorem :: FSCIRC_1:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3"))))))) ; theorem :: FSCIRC_1:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k6_fscirc_1 :::"BorrowOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_binarith :::"'or'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "a3"))))))) ; theorem :: FSCIRC_1:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2"))))))) ; theorem :: FSCIRC_1:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3"))))))) ; theorem :: FSCIRC_1:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3"))))))) ; theorem :: FSCIRC_1:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k6_fscirc_1 :::"BorrowOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3")) ")" )))))) ; theorem :: FSCIRC_1:18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))) ; begin definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BitSubtracterWithBorrowStr"::: "(" "x" "," "y" "," "c" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FSCIRC_1:def 8 (Set (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" "x" "," "y" "," "c" "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" "x" "," "y" "," "c" ")" ")" )); end; :: deftheorem defines :::"BitSubtracterWithBorrowStr"::: FSCIRC_1:def 8 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_fscirc_1 :::"BitSubtracterWithBorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_facirc_1 :::"2GatesCircStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k4_fscirc_1 :::"BorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )))); theorem :: FSCIRC_1:19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k8_fscirc_1 :::"BitSubtracterWithBorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: FSCIRC_1:20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k8_fscirc_1 :::"BitSubtracterWithBorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k9_facirc_1 :::"2GatesCircOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_enumset1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_fscirc_1 :::"BorrowOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FSCIRC_1:21 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k8_fscirc_1 :::"BitSubtracterWithBorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ))) ; definitionlet "x", "y", "c" be ($#m1_hidden :::"set"::: ) ; func :::"BitSubtracterWithBorrowCirc"::: "(" "x" "," "y" "," "c" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k8_fscirc_1 :::"BitSubtracterWithBorrowStr"::: ) "(" "x" "," "y" "," "c" ")" ) equals :: FSCIRC_1:def 9 (Set (Set "(" ($#k2_fscirc_1 :::"BitSubtracterCirc"::: ) "(" "x" "," "y" "," "c" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" "x" "," "y" "," "c" ")" ")" )); end; :: deftheorem defines :::"BitSubtracterWithBorrowCirc"::: FSCIRC_1:def 9 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_fscirc_1 :::"BitSubtracterWithBorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_fscirc_1 :::"BitSubtracterCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k7_fscirc_1 :::"BorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )))); theorem :: FSCIRC_1:22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k8_fscirc_1 :::"BitSubtracterWithBorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FSCIRC_1:23 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k8_fscirc_1 :::"BitSubtracterWithBorrowStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; theorem :: FSCIRC_1:24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k9_fscirc_1 :::"BitSubtracterWithBorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_fscirc_1 :::"BitSubtracterOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_fscirc_1 :::"BorrowOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3")) ")" ))) ")" )))) ; theorem :: FSCIRC_1:25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k9_fscirc_1 :::"BitSubtracterWithBorrowCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) ))) ;