:: TWOSCOMP semantic presentation begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_circcomb :::"unsplit"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "A")); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "S")); :: original: :::"."::: redefine func "s" :::"."::: "v" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; definitionfunc :::"and2"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y"))))); func :::"and2a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y"))))); func :::"and2b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"and2"::: TWOSCOMP:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_twoscomp :::"and2"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"and2a"::: TWOSCOMP:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_twoscomp :::"and2a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"and2b"::: TWOSCOMP:def 3 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_twoscomp :::"and2b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" )))) ")" )); definitionfunc :::"nand2"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" )))); func :::"nand2a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" )))); func :::"nand2b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" )))); end; :: deftheorem defines :::"nand2"::: TWOSCOMP:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k5_twoscomp :::"nand2"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" )))) ")" )); :: deftheorem defines :::"nand2a"::: TWOSCOMP:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_twoscomp :::"nand2a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" )))) ")" )); :: deftheorem defines :::"nand2b"::: TWOSCOMP:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k7_twoscomp :::"nand2b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" )))) ")" )); definitionfunc :::"or2"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y"))))); func :::"or2a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y"))))); func :::"or2b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"or2"::: TWOSCOMP:def 7 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k8_twoscomp :::"or2"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"or2a"::: TWOSCOMP:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k9_twoscomp :::"or2a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"or2b"::: TWOSCOMP:def 9 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k10_twoscomp :::"or2b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" )))) ")" )); definitionfunc :::"nor2"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" )))); func :::"nor2a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" )))); func :::"nor2b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" )))); end; :: deftheorem defines :::"nor2"::: TWOSCOMP:def 10 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k11_twoscomp :::"nor2"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" )))) ")" )); :: deftheorem defines :::"nor2a"::: TWOSCOMP:def 11 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k12_twoscomp :::"nor2a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" )))) ")" )); :: deftheorem defines :::"nor2b"::: TWOSCOMP:def 12 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k13_twoscomp :::"nor2b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" )))) ")" )); definitionfunc :::"xor2"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y"))))); func :::"xor2a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y"))))); func :::"xor2b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"xor2"::: TWOSCOMP:def 13 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k14_twoscomp :::"xor2"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"xor2a"::: TWOSCOMP:def 14 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k15_twoscomp :::"xor2a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"xor2b"::: TWOSCOMP:def 15 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k16_twoscomp :::"xor2b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" )))) ")" )); theorem :: TWOSCOMP:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")))) & (Bool (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")))) & (Bool (Set (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ))) ")" )) ; theorem :: TWOSCOMP:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k5_twoscomp :::"nand2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set ($#k6_twoscomp :::"nand2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set ($#k7_twoscomp :::"nand2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ))) ")" )) ; theorem :: TWOSCOMP:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k8_twoscomp :::"or2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")))) & (Bool (Set (Set ($#k9_twoscomp :::"or2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")))) & (Bool (Set (Set ($#k10_twoscomp :::"or2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ))) ")" )) ; theorem :: TWOSCOMP:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k11_twoscomp :::"nor2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set ($#k12_twoscomp :::"nor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set ($#k13_twoscomp :::"nor2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ))) ")" )) ; theorem :: TWOSCOMP:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y")))) & (Bool (Set (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y")))) & (Bool (Set (Set ($#k16_twoscomp :::"xor2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ))) ")" )) ; theorem :: TWOSCOMP:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k13_twoscomp :::"nor2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_twoscomp :::"nor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k11_twoscomp :::"nor2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ))) ")" )) ; theorem :: TWOSCOMP:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k8_twoscomp :::"or2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_twoscomp :::"nand2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k9_twoscomp :::"or2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_twoscomp :::"nand2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k10_twoscomp :::"or2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_twoscomp :::"nand2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ))) ")" )) ; theorem :: TWOSCOMP:8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set ($#k16_twoscomp :::"xor2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )))) ; theorem :: TWOSCOMP:9 (Bool "(" (Bool (Set (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: TWOSCOMP:10 (Bool "(" (Bool (Set (Set ($#k8_twoscomp :::"or2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k8_twoscomp :::"or2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k8_twoscomp :::"or2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k8_twoscomp :::"or2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k9_twoscomp :::"or2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k9_twoscomp :::"or2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k9_twoscomp :::"or2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k9_twoscomp :::"or2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k10_twoscomp :::"or2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k10_twoscomp :::"or2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k10_twoscomp :::"or2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k10_twoscomp :::"or2b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: TWOSCOMP:11 (Bool "(" (Bool (Set (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; definitionfunc :::"and3"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z"))))); func :::"and3a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z"))))); func :::"and3b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z"))))); func :::"and3c"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" )))); end; :: deftheorem defines :::"and3"::: TWOSCOMP:def 16 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k17_twoscomp :::"and3"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z"))))) ")" )); :: deftheorem defines :::"and3a"::: TWOSCOMP:def 17 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k18_twoscomp :::"and3a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z"))))) ")" )); :: deftheorem defines :::"and3b"::: TWOSCOMP:def 18 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k19_twoscomp :::"and3b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z"))))) ")" )); :: deftheorem defines :::"and3c"::: TWOSCOMP:def 19 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k20_twoscomp :::"and3c"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" )))) ")" )); definitionfunc :::"nand3"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" )))); func :::"nand3a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 21 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" )))); func :::"nand3b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" )))); func :::"nand3c"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 23 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" ) ")" )))); end; :: deftheorem defines :::"nand3"::: TWOSCOMP:def 20 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k21_twoscomp :::"nand3"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" )))) ")" )); :: deftheorem defines :::"nand3a"::: TWOSCOMP:def 21 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k22_twoscomp :::"nand3a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" )))) ")" )); :: deftheorem defines :::"nand3b"::: TWOSCOMP:def 22 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k23_twoscomp :::"nand3b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" )))) ")" )); :: deftheorem defines :::"nand3c"::: TWOSCOMP:def 23 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k24_twoscomp :::"nand3c"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" ) ")" )))) ")" )); definitionfunc :::"or3"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z"))))); func :::"or3a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z"))))); func :::"or3b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 26 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z"))))); func :::"or3c"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 27 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" )))); end; :: deftheorem defines :::"or3"::: TWOSCOMP:def 24 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k25_twoscomp :::"or3"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z"))))) ")" )); :: deftheorem defines :::"or3a"::: TWOSCOMP:def 25 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k26_twoscomp :::"or3a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z"))))) ")" )); :: deftheorem defines :::"or3b"::: TWOSCOMP:def 26 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k27_twoscomp :::"or3b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z"))))) ")" )); :: deftheorem defines :::"or3c"::: TWOSCOMP:def 27 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k28_twoscomp :::"or3c"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" )))) ")" )); definitionfunc :::"nor3"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 28 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" )))); func :::"nor3a"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" )))); func :::"nor3b"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 30 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" )))); func :::"nor3c"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" ) ")" )))); end; :: deftheorem defines :::"nor3"::: TWOSCOMP:def 28 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k29_twoscomp :::"nor3"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" )))) ")" )); :: deftheorem defines :::"nor3a"::: TWOSCOMP:def 29 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k30_twoscomp :::"nor3a"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" )))) ")" )); :: deftheorem defines :::"nor3b"::: TWOSCOMP:def 30 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k31_twoscomp :::"nor3b"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" )))) ")" )); :: deftheorem defines :::"nor3c"::: TWOSCOMP:def 31 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k32_twoscomp :::"nor3c"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" ) ")" )))) ")" )); definitionfunc :::"xor3"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: TWOSCOMP:def 32 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "z"))))); end; :: deftheorem defines :::"xor3"::: TWOSCOMP:def 32 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k33_twoscomp :::"xor3"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "y")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "z"))))) ")" )); theorem :: TWOSCOMP:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")))) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")))) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")))) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" ))) ")" )) ; theorem :: TWOSCOMP:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k21_twoscomp :::"nand3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set ($#k22_twoscomp :::"nand3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set ($#k23_twoscomp :::"nand3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set ($#k24_twoscomp :::"nand3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" ) ")" ))) ")" )) ; theorem :: TWOSCOMP:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")))) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")))) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")))) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" ))) ")" )) ; theorem :: TWOSCOMP:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k29_twoscomp :::"nor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set ($#k30_twoscomp :::"nor3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set ($#k31_twoscomp :::"nor3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set ($#k32_twoscomp :::"nor3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "z")) ")" ) ")" ))) ")" )) ; theorem :: TWOSCOMP:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_twoscomp :::"nor3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k31_twoscomp :::"nor3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) ($#k11_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k30_twoscomp :::"nor3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) ($#k11_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_twoscomp :::"nor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ))) ")" )) ; theorem :: TWOSCOMP:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_twoscomp :::"nand3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_twoscomp :::"nand3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) ($#k11_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k22_twoscomp :::"nand3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) ($#k11_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k21_twoscomp :::"nand3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ))) ")" )) ; theorem :: TWOSCOMP:18 (Bool "(" (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k17_twoscomp :::"and3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; theorem :: TWOSCOMP:19 (Bool "(" (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k18_twoscomp :::"and3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: TWOSCOMP:20 (Bool "(" (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_twoscomp :::"and3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: TWOSCOMP:21 (Bool "(" (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k20_twoscomp :::"and3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: TWOSCOMP:22 (Bool "(" (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k25_twoscomp :::"or3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; theorem :: TWOSCOMP:23 (Bool "(" (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k26_twoscomp :::"or3a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; theorem :: TWOSCOMP:24 (Bool "(" (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k27_twoscomp :::"or3b"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; theorem :: TWOSCOMP:25 (Bool "(" (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k28_twoscomp :::"or3c"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: TWOSCOMP:26 (Bool "(" (Bool (Set (Set ($#k33_twoscomp :::"xor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k33_twoscomp :::"xor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k33_twoscomp :::"xor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k33_twoscomp :::"xor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k33_twoscomp :::"xor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k33_twoscomp :::"xor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k33_twoscomp :::"xor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k33_twoscomp :::"xor3"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; begin definitionlet "x", "b" be ($#m1_hidden :::"set"::: ) ; func :::"CompStr"::: "(" "x" "," "b" ")" -> ($#~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 :: TWOSCOMP:def 33 (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ")" ); end; :: deftheorem defines :::"CompStr"::: TWOSCOMP:def 33 : (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k34_twoscomp :::"CompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ")" ))); definitionlet "x", "b" be ($#m1_hidden :::"set"::: ) ; func :::"CompCirc"::: "(" "x" "," "b" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k34_twoscomp :::"CompStr"::: ) "(" "x" "," "b" ")" ) equals :: TWOSCOMP:def 34 (Set ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "x" "," "b" "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ")" ); end; :: deftheorem defines :::"CompCirc"::: TWOSCOMP:def 34 : (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k35_twoscomp :::"CompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ")" ))); definitionlet "x", "b" be ($#m1_hidden :::"set"::: ) ; func :::"CompOutput"::: "(" "x" "," "b" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k34_twoscomp :::"CompStr"::: ) "(" "x" "," "b" ")" ")" )) equals :: TWOSCOMP:def 35 (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"CompOutput"::: TWOSCOMP:def 35 : (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k36_twoscomp :::"CompOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k4_tarski :::"]"::: ) ))); definitionlet "x", "b" be ($#m1_hidden :::"set"::: ) ; func :::"IncrementStr"::: "(" "x" "," "b" ")" -> ($#~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 :: TWOSCOMP:def 36 (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ); end; :: deftheorem defines :::"IncrementStr"::: TWOSCOMP:def 36 : (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k37_twoscomp :::"IncrementStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ))); definitionlet "x", "b" be ($#m1_hidden :::"set"::: ) ; func :::"IncrementCirc"::: "(" "x" "," "b" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k37_twoscomp :::"IncrementStr"::: ) "(" "x" "," "b" ")" ) equals :: TWOSCOMP:def 37 (Set ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" "x" "," "b" "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ); end; :: deftheorem defines :::"IncrementCirc"::: TWOSCOMP:def 37 : (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k38_twoscomp :::"IncrementCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_facirc_1 :::"1GateCircuit"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ")" ))); definitionlet "x", "b" be ($#m1_hidden :::"set"::: ) ; func :::"IncrementOutput"::: "(" "x" "," "b" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k37_twoscomp :::"IncrementStr"::: ) "(" "x" "," "b" ")" ")" )) equals :: TWOSCOMP:def 38 (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "x" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"IncrementOutput"::: TWOSCOMP:def 38 : (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k39_twoscomp :::"IncrementOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ))); definitionlet "x", "b" be ($#m1_hidden :::"set"::: ) ; func :::"BitCompStr"::: "(" "x" "," "b" ")" -> ($#~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 :: TWOSCOMP:def 39 (Set (Set "(" ($#k34_twoscomp :::"CompStr"::: ) "(" "x" "," "b" ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k37_twoscomp :::"IncrementStr"::: ) "(" "x" "," "b" ")" ")" )); end; :: deftheorem defines :::"BitCompStr"::: TWOSCOMP:def 39 : (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k34_twoscomp :::"CompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k37_twoscomp :::"IncrementStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )))); definitionlet "x", "b" be ($#m1_hidden :::"set"::: ) ; func :::"BitCompCirc"::: "(" "x" "," "b" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k40_twoscomp :::"BitCompStr"::: ) "(" "x" "," "b" ")" ) equals :: TWOSCOMP:def 40 (Set (Set "(" ($#k35_twoscomp :::"CompCirc"::: ) "(" "x" "," "b" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k38_twoscomp :::"IncrementCirc"::: ) "(" "x" "," "b" ")" ")" )); end; :: deftheorem defines :::"BitCompCirc"::: TWOSCOMP:def 40 : (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k41_twoscomp :::"BitCompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k35_twoscomp :::"CompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k38_twoscomp :::"IncrementCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )))); theorem :: TWOSCOMP:27 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k34_twoscomp :::"CompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: TWOSCOMP:28 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k34_twoscomp :::"CompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )))) ; theorem :: TWOSCOMP:29 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "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 "(" ($#k34_twoscomp :::"CompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k34_twoscomp :::"CompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) ")" )) ; theorem :: TWOSCOMP:30 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k34_twoscomp :::"CompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; theorem :: TWOSCOMP:31 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k37_twoscomp :::"IncrementStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: TWOSCOMP:32 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k37_twoscomp :::"IncrementStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )))) ; theorem :: TWOSCOMP:33 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "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 "(" ($#k37_twoscomp :::"IncrementStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k37_twoscomp :::"IncrementStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) ")" )) ; theorem :: TWOSCOMP:34 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k37_twoscomp :::"IncrementStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; theorem :: TWOSCOMP:35 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: TWOSCOMP:36 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) ")" )) ; theorem :: TWOSCOMP:37 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )))) ; theorem :: TWOSCOMP:38 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: TWOSCOMP:39 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) ")" )) ; theorem :: TWOSCOMP:40 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: TWOSCOMP:41 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "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 "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ))) ")" )) ; theorem :: TWOSCOMP:42 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k40_twoscomp :::"BitCompStr"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) )) ; theorem :: TWOSCOMP:43 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k35_twoscomp :::"CompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k36_twoscomp :::"CompOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ))) ; theorem :: TWOSCOMP:44 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k35_twoscomp :::"CompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) (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 "b"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k36_twoscomp :::"CompOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) ")" )))) ; theorem :: TWOSCOMP:45 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k41_twoscomp :::"BitCompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k36_twoscomp :::"CompOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ))) ; theorem :: TWOSCOMP:46 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k41_twoscomp :::"BitCompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) (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 "b"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k36_twoscomp :::"CompOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) ")" )))) ; theorem :: TWOSCOMP:47 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k38_twoscomp :::"IncrementCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k39_twoscomp :::"IncrementOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ))) ; theorem :: TWOSCOMP:48 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k38_twoscomp :::"IncrementCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) (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 "b"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k39_twoscomp :::"IncrementOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) ")" )))) ; theorem :: TWOSCOMP:49 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k41_twoscomp :::"BitCompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k39_twoscomp :::"IncrementOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ))) ; theorem :: TWOSCOMP:50 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k41_twoscomp :::"BitCompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) (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 "b"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k39_twoscomp :::"IncrementOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) ")" )))) ; theorem :: TWOSCOMP:51 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k41_twoscomp :::"BitCompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k36_twoscomp :::"CompOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k15_twoscomp :::"xor2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k39_twoscomp :::"IncrementOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ))) ; theorem :: TWOSCOMP:52 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k41_twoscomp :::"BitCompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) (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 "b"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k36_twoscomp :::"CompOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k39_twoscomp :::"IncrementOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) ")" )))) ; theorem :: TWOSCOMP:53 (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k41_twoscomp :::"BitCompCirc"::: ) "(" (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s"))) "is" ($#v1_circuit2 :::"stable"::: ) ))) ;