:: FACIRC_2 semantic presentation begin theorem :: FACIRC_2:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: FACIRC_2:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ")" )) ; registration cluster ($#v11_struct_0 :::"void"::: ) -> ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registration cluster ($#v11_struct_0 :::"void"::: ) ($#v1_msualg_1 :::"strict"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"SingleMSS"::: "x" -> ($#v11_struct_0 :::"void"::: ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: FACIRC_2:def 1 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"SingleMSS"::: FACIRC_2:def 1 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v11_struct_0 :::"void"::: ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_facirc_2 :::"SingleMSS"::: ) (Set (Var "x")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" ))); registrationlet "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_facirc_2 :::"SingleMSS"::: ) "x") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_struct_0 :::"void"::: ) ($#v1_msualg_1 :::"strict"::: ) ; end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"SingleMSA"::: "x" -> ($#v3_msualg_1 :::"strict"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k1_facirc_2 :::"SingleMSS"::: ) "x") means :: FACIRC_2:def 2 (Bool verum); end; :: deftheorem defines :::"SingleMSA"::: FACIRC_2:def 2 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k1_facirc_2 :::"SingleMSS"::: ) (Set (Var "x"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_facirc_2 :::"SingleMSA"::: ) (Set (Var "x")))) "iff" (Bool verum) ")" ))); theorem :: FACIRC_2:3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k1_facirc_2 :::"SingleMSS"::: ) (Set (Var "x"))) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S"))))) ; theorem :: FACIRC_2:4 (Bool "for" (Set (Var "x")) "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 "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set "(" ($#k1_facirc_2 :::"SingleMSS"::: ) (Set (Var "x")) ")" ) ($#k2_circcomb :::"+*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S"))) "#)" )))) ; theorem :: FACIRC_2:5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set "(" ($#k2_facirc_2 :::"SingleMSA"::: ) (Set (Var "x")) ")" ) ($#k3_circcomb :::"+*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) "#)" ))))) ; notationsynonym :::"<*>"::: for :::"{}"::: ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitAdderStr"::: "(" "x" "," "y" ")" -> ($#~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"::: ) means :: FACIRC_2:def 3 (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"-BitAdderStr"::: FACIRC_2:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#~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"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" ))) ")" ) ")" )) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitAdderCirc"::: "(" "x" "," "y" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set "n" ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" "x" "," "y" ")" ) means :: FACIRC_2:def 4 (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set "n" ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" "x" "," "y" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" ) ")" )); end; :: deftheorem defines :::"-BitAdderCirc"::: FACIRC_2:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" ) ")" )) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitMajorityOutput"::: "(" "x" "," "y" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" "n" ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" "x" "," "y" ")" ")" )) means :: FACIRC_2:def 5 (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"-BitMajorityOutput"::: FACIRC_2:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ))) ")" ) ")" )) ")" )))); theorem :: FACIRC_2:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "n")) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" )))) ; theorem :: FACIRC_2:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ; theorem :: FACIRC_2:8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Num 1) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" )) ")" ))) ; theorem :: FACIRC_2:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Num 1) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) ")" )) ; theorem :: FACIRC_2:10 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) & (Bool (Set (Set (Var "n")) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) & (Bool (Set (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) ")" )))) ; theorem :: FACIRC_2:11 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" )))) ; theorem :: FACIRC_2:12 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" ))) ; theorem :: FACIRC_2:13 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "m")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: FACIRC_2:14 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ) ")" ))))) ; definitionlet "k", "n" be ($#m1_hidden :::"Nat":::); assume that (Bool (Set (Const "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) and (Bool (Set (Const "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "n"))) ; let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "(" "k" "," "n" ")" :::"-BitAdderOutput"::: "(" "x" "," "y" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" "n" ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" "x" "," "y" ")" ")" )) means :: FACIRC_2:def 6 (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "k" ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k12_facirc_1 :::"BitAdderOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) "k" ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) "k" ")" ) "," (Set "(" (Set (Var "i")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" "x" "," "y" ")" ")" ) ")" )) ")" )); end; :: deftheorem defines :::"-BitAdderOutput"::: FACIRC_2:def 6 : (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "k")) "," (Set (Var "n")) ")" ($#k6_facirc_2 :::"-BitAdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k12_facirc_1 :::"BitAdderOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "i")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" )) ")" )))); theorem :: FACIRC_2:15 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k6_facirc_2 :::"-BitAdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_facirc_1 :::"BitAdderOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "k")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )))) ; theorem :: FACIRC_2:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::)))) ; theorem :: FACIRC_2:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k14_facirc_1 :::"MajorityIStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: FACIRC_2:18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k14_facirc_1 :::"MajorityIStr"::: ) "(" (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 :: FACIRC_2:19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (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_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FACIRC_2:20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k15_facirc_1 :::"MajorityStr"::: ) "(" (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 :: FACIRC_2:21 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r1_circcomb :::"tolerates"::: ) (Set (Var "S2"))) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2"))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "S1")) ($#k2_circcomb :::"+*"::: ) (Set (Var "S2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1"))))) ; theorem :: FACIRC_2:22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (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 :: FACIRC_2:23 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (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_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_enumset1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" ) ($#k1_tarski :::"}"::: ) )))) ; registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> ($#v2_facirc_1 :::"nonpair-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x", "y" be ($#m1_hidden :::"FinSequence":::); cluster (Set "n" ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" "x" "," "y" ")" ) -> ($#v1_xtuple_0 :::"pair"::: ) ; end; theorem :: FACIRC_2:24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) )) & (Bool (Set (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) & (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ))) ")" ) "or" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_facirc_1 :::"or3"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ))) ")" ) ")" ))) ; theorem :: FACIRC_2:25 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ($#k4_tarski :::"]"::: ) )) ")" )))) ; theorem :: FACIRC_2:26 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_facirc_1 :::"BitAdderWithOverflowStr"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "n")) ($#k5_facirc_2 :::"-BitMajorityOutput"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) ")" ))) ; theorem :: FACIRC_2:27 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k3_facirc_2 :::"-BitAdderStr"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "x")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "y")) ")" ))))) ; theorem :: FACIRC_2:28 (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 "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (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_facirc_1 :::"'&'"::: ) ) ($#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 ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k11_facirc_1 :::"."::: ) (Set "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (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 :: FACIRC_2:29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k18_facirc_1 :::"MajorityCirc"::: ) "(" (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"::: ) ))) ; theorem :: FACIRC_2:30 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (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 "(" ($#k12_facirc_1 :::"BitAdderOutput"::: ) "(" (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 "(" ($#k17_facirc_1 :::"MajorityOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (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 (Var "a3")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a1")) ")" ))) ")" )))) ; theorem :: FACIRC_2:31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_facirc_1 :::"'&'"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_facirc_1 :::"'xor'"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k20_facirc_1 :::"BitAdderWithOverflowCirc"::: ) "(" (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"::: ) ))) ; theorem :: FACIRC_2:32 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "n")) ($#k4_facirc_2 :::"-BitAdderCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; theorem :: FACIRC_2:33 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "i"))(Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FACIRC_2:34 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) (Bool "ex" (Set (Var "y")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "i"))(Bool "ex" (Set (Var "a")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FACIRC_2:35 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "N")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "N")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "N")) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Set (Var "N")) ($#k3_funct_2 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" ))) ;