:: GFACIRC2 semantic presentation begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitGFA0Str"::: "(" "x" "," "y" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: GFACIRC2:def 1 (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"-BitGFA0Str"::: GFACIRC2:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" ))) ")" ) ")" )) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitGFA0Circ"::: "(" "x" "," "y" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set "n" ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" "x" "," "y" ")" ) means :: GFACIRC2:def 2 (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set "n" ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" "x" "," "y" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" ) ")" )); end; :: deftheorem defines :::"-BitGFA0Circ"::: GFACIRC2:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" ) ")" )) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitGFA0CarryOutput"::: "(" "x" "," "y" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" "n" ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" "x" "," "y" ")" ")" )) means :: GFACIRC2:def 3 (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"-BitGFA0CarryOutput"::: GFACIRC2:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" )) ")" )))); theorem :: GFACIRC2:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "n")) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" )))) ; theorem :: GFACIRC2:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ; theorem :: GFACIRC2:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Num 1) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" )) ")" ))) ; theorem :: GFACIRC2:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Num 1) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) ")" )) ; theorem :: GFACIRC2:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) & (Bool (Set (Set (Var "n")) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) & (Bool (Set (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) ")" )))) ; theorem :: GFACIRC2:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" )))) ; theorem :: GFACIRC2:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" ))) ; theorem :: GFACIRC2:8 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "m")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: GFACIRC2:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ) ")" ))))) ; definitionlet "k", "n" be ($#m1_hidden :::"Nat":::); assume that (Bool (Set (Const "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) and (Bool (Set (Const "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "n"))) ; let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "(" "k" "," "n" ")" :::"-BitGFA0AdderOutput"::: "(" "x" "," "y" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" "n" ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" "x" "," "y" ")" ")" )) means :: GFACIRC2:def 4 (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "k" ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) "k" ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) "k" ")" ) "," (Set "(" (Set (Var "i")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" "x" "," "y" ")" ")" ) ")" )) ")" )); end; :: deftheorem defines :::"-BitGFA0AdderOutput"::: GFACIRC2:def 4 : (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "k")) "," (Set (Var "n")) ")" ($#k4_gfacirc2 :::"-BitGFA0AdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "i")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" )) ")" )))); theorem :: GFACIRC2:10 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set "(" (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k4_gfacirc2 :::"-BitGFA0AdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "k")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )))) ; theorem :: GFACIRC2:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::)))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); cluster (Set "n" ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" "x" "," "y" ")" ) -> ($#v1_xtuple_0 :::"pair"::: ) ; end; theorem :: GFACIRC2:12 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "n")) ($#k3_gfacirc2 :::"-BitGFA0CarryOutput"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) ")" ))) ; theorem :: GFACIRC2:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k1_gfacirc2 :::"-BitGFA0Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "x")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "y")) ")" ))))) ; theorem :: GFACIRC2:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "n")) ($#k2_gfacirc2 :::"-BitGFA0Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitGFA1Str"::: "(" "x" "," "y" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: GFACIRC2:def 5 (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"-BitGFA1Str"::: GFACIRC2:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" ))) ")" ) ")" )) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitGFA1Circ"::: "(" "x" "," "y" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set "n" ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" "x" "," "y" ")" ) means :: GFACIRC2:def 6 (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set "n" ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" "x" "," "y" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" ) ")" )); end; :: deftheorem defines :::"-BitGFA1Circ"::: GFACIRC2:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" ) ")" )) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "n" :::"-BitGFA1CarryOutput"::: "(" "x" "," "y" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" "n" ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" "x" "," "y" ")" ")" )) means :: GFACIRC2:def 7 (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"-BitGFA1CarryOutput"::: GFACIRC2:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" )) ")" )))); theorem :: GFACIRC2:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "z")) ")" )) ")" )))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "n")) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" )))) ; theorem :: GFACIRC2:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" )) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ; theorem :: GFACIRC2:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Num 1) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set (Var "c")) ")" )) ")" ))) ; theorem :: GFACIRC2:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Num 1) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_circcomb :::"1GateCircStr"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_circcomb :::"1GateCircuit"::: ) "(" (Set ($#k1_xboole_0 :::"<*>"::: ) ) "," (Set "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ")" ) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Num 1) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) ")" )) ; theorem :: GFACIRC2:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) & (Bool (Set (Set (Var "n")) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) & (Bool (Set (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" ) ")" )) ")" )))) ; theorem :: GFACIRC2:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" )))) ; theorem :: GFACIRC2:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" ))) ; theorem :: GFACIRC2:22 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "m")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: GFACIRC2:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ")" ) ")" ))))) ; definitionlet "k", "n" be ($#m1_hidden :::"Nat":::); assume that (Bool (Set (Const "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) and (Bool (Set (Const "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "n"))) ; let "x", "y" be ($#m1_hidden :::"FinSequence":::); func "(" "k" "," "n" ")" :::"-BitGFA1AdderOutput"::: "(" "x" "," "y" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" "n" ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" "x" "," "y" ")" ")" )) means :: GFACIRC2:def 8 (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "k" ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set "(" "x" ($#k1_funct_1 :::"."::: ) "k" ")" ) "," (Set "(" "y" ($#k1_funct_1 :::"."::: ) "k" ")" ) "," (Set "(" (Set (Var "i")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" "x" "," "y" ")" ")" ) ")" )) ")" )); end; :: deftheorem defines :::"-BitGFA1AdderOutput"::: GFACIRC2:def 8 : (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "k")) "," (Set (Var "n")) ")" ($#k8_gfacirc2 :::"-BitGFA1AdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "i")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ")" )) ")" )))); theorem :: GFACIRC2:24 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set "(" (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k8_gfacirc2 :::"-BitGFA1AdderOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "k")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )))) ; theorem :: GFACIRC2:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::)))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"FinSequence":::); cluster (Set "n" ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" "x" "," "y" ")" ) -> ($#v1_xtuple_0 :::"pair"::: ) ; end; theorem :: GFACIRC2:26 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "n")) ($#k7_gfacirc2 :::"-BitGFA1CarryOutput"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) "is" ($#v1_facirc_1 :::"without_pairs"::: ) ) ")" ))) ; theorem :: GFACIRC2:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "n")) ($#k5_gfacirc2 :::"-BitGFA1Str"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "x")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "y")) ")" ))))) ; theorem :: GFACIRC2:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v2_facirc_1 :::"nonpair-yielding"::: ) ($#m1_hidden :::"FinSeqLen":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "n")) ($#k6_gfacirc2 :::"-BitGFA1Circ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))) ;