:: CIRCUIT2 semantic presentation begin theorem :: CIRCUIT2:1 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) (Bool "for" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "HH")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")))) & (Bool (Set (Var "H")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X"))) "," (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")))) & (Bool (Set (Var "HH")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" )))) "holds" (Bool "ex" (Set (Var "HHp")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "HHp")) ($#r1_hidden :::"="::: ) (Set (Set (Var "HH")) ($#k15_pralg_1 :::".."::: ) (Set (Var "p")))) & (Bool (Set (Set "(" (Set (Var "H")) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "HHp")))) ")" ))))))))) ; definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "SCS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "SCS")); let "iv" be ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Const "SCS")); :: original: :::"+*"::: redefine func "s" :::"+*"::: "iv" -> ($#m1_subset_1 :::"State":::) "of" "SCS"; end; definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "iv" be ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Const "A")); func :::"Fix_inp"::: "iv" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k13_msafree :::"FreeGen"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "A" ")" )) means :: CIRCUIT2:def 1 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "IIG" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) "IIG"))) "implies" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "v"))) ($#r1_funct_2 :::"="::: ) (Set (Set "(" ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "v")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ")" ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" "iv" ($#k1_funct_1 :::"."::: ) (Set (Var "v")) ")" ) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) "IIG"))) "implies" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "v"))) ($#r1_funct_2 :::"="::: ) (Set (Set "(" ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "v")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ")" ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IIG") ($#k4_tarski :::"]"::: ) ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) "IIG" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_msafree2 :::"SortsWithConstants"::: ) "IIG" ")" )))) "implies" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "v")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ")" ")" ))) ")" ")" )); end; :: deftheorem defines :::"Fix_inp"::: CIRCUIT2:def 1 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k13_msafree :::"FreeGen"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A")))) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_circuit2 :::"Fix_inp"::: ) (Set (Var "iv")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_msualg_3 :::"."::: ) (Set (Var "v"))) ($#r1_funct_2 :::"="::: ) (Set (Set "(" ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "v")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ")" ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "iv")) ($#k1_funct_1 :::"."::: ) (Set (Var "v")) ")" ) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_msualg_3 :::"."::: ) (Set (Var "v"))) ($#r1_funct_2 :::"="::: ) (Set (Set "(" ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "v")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ")" ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG")) ")" )))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_msualg_3 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k12_msafree :::"FreeGen"::: ) "(" (Set (Var "v")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ")" ")" ))) ")" ")" )) ")" ))))); definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "iv" be ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Const "A")); func :::"Fix_inp_ext"::: "iv" -> ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "A" ")" ) "," (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "A" ")" ) means :: CIRCUIT2:def 2 (Bool "(" (Bool it ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k5_msafree2 :::"FreeEnv"::: ) "A") "," (Set ($#k5_msafree2 :::"FreeEnv"::: ) "A")) & (Bool (Set ($#k2_circuit2 :::"Fix_inp"::: ) "iv") ($#r2_pboole :::"c="::: ) it) ")" ); end; :: deftheorem defines :::"Fix_inp_ext"::: CIRCUIT2:def 2 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")))) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A"))) "," (Set ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")))) & (Bool (Set ($#k2_circuit2 :::"Fix_inp"::: ) (Set (Var "iv"))) ($#r2_pboole :::"c="::: ) (Set (Var "b4"))) ")" ) ")" ))))); theorem :: CIRCUIT2:2 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG")) ")" ))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))))))))) ; theorem :: CIRCUIT2:3 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "iv")) ($#k1_funct_1 :::"."::: ) (Set (Var "v")) ")" ) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )))))))) ; theorem :: CIRCUIT2:4 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "q")))))))))) ; theorem :: CIRCUIT2:5 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) )))))))) ; theorem :: CIRCUIT2:6 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "e")) "," (Set (Var "e1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) (Bool "for" (Set (Var "t")) "," (Set (Var "t1")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Var "t1")) ($#r1_hidden :::"="::: ) (Set (Var "e1"))) & (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "e"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t1")))))))))) ; theorem :: CIRCUIT2:7 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "e")) "," (Set (Var "e1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "A")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "e"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e1"))))))))) ; definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "SCS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "IIG")); let "iv" be ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Const "SCS")); func :::"IGTree"::: "(" "v" "," "iv" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "SCS" ")" )) ($#k1_funct_1 :::"."::: ) "v") means :: CIRCUIT2:def 3 (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "SCS" ")" )) ($#k1_funct_1 :::"."::: ) "v") "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" "v" "," "SCS" ")" )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) "iv" ")" ) ($#k1_msualg_3 :::"."::: ) "v" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "e")))) ")" )); end; :: deftheorem defines :::"IGTree"::: CIRCUIT2:def 3 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "SCS")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit2 :::"IGTree"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" )) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "SCS")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "SCS")) ")" )) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "e")))) ")" )) ")" )))))); theorem :: CIRCUIT2:8 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "holds" (Bool (Set ($#k4_circuit2 :::"IGTree"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_circuit2 :::"Fix_inp_ext"::: ) (Set (Var "iv")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_circuit2 :::"IGTree"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ")" ))))))) ; theorem :: CIRCUIT2:9 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit2 :::"IGTree"::: ) "(" (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) "," (Set (Var "iv")) ")" )) ")" )) "holds" (Bool (Set ($#k4_circuit2 :::"IGTree"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p"))))))))) ; definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "SCS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "IIG")); let "iv" be ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Const "SCS")); func :::"IGValue"::: "(" "v" "," "iv" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "SCS") ($#k1_funct_1 :::"."::: ) "v") equals :: CIRCUIT2:def 4 (Set (Set "(" (Set "(" ($#k6_msafree2 :::"Eval"::: ) "SCS" ")" ) ($#k1_msualg_3 :::"."::: ) "v" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_circuit2 :::"IGTree"::: ) "(" "v" "," "iv" ")" ")" )); end; :: deftheorem defines :::"IGValue"::: CIRCUIT2:def 4 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "holds" (Bool (Set ($#k5_circuit2 :::"IGValue"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_msafree2 :::"Eval"::: ) (Set (Var "SCS")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_circuit2 :::"IGTree"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ")" ))))))); theorem :: CIRCUIT2:10 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))))) "holds" (Bool (Set ($#k5_circuit2 :::"IGValue"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "iv")) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))))))) ; theorem :: CIRCUIT2:11 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG"))))) "holds" (Bool (Set ($#k5_circuit2 :::"IGValue"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_circuit1 :::"Set-Constants"::: ) (Set (Var "SCS")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))))))) ; begin definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "SCS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "SCS")); func :::"Following"::: "s" -> ($#m1_subset_1 :::"State":::) "of" "SCS" means :: CIRCUIT2:def 5 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "IIG" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) "IIG"))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" & "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) "IIG"))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," "SCS" ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ($#k3_circuit1 :::"depends_on_in"::: ) "s" ")" ))) ")" ")" )); end; :: deftheorem defines :::"Following"::: CIRCUIT2:def 5 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "s")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" & "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set (Var "SCS")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s")) ")" ))) ")" ")" )) ")" )))); theorem :: CIRCUIT2:12 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set (Var "iv")) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set (Var "iv")) ($#r1_tarski :::"c="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")))))))) ; definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "SCS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "IT" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "SCS")); attr "IT" is :::"stable"::: means :: CIRCUIT2:def 6 (Bool "IT" ($#r8_pboole :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) "IT")); end; :: deftheorem defines :::"stable"::: CIRCUIT2:def 6 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_circuit2 :::"stable"::: ) ) "iff" (Bool (Set (Var "IT")) ($#r8_pboole :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "IT")))) ")" )))); definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "SCS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "SCS")); let "iv" be ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Const "SCS")); func :::"Following"::: "(" "s" "," "iv" ")" -> ($#m1_subset_1 :::"State":::) "of" "SCS" equals :: CIRCUIT2:def 7 (Set ($#k6_circuit2 :::"Following"::: ) (Set "(" "s" ($#k1_circuit2 :::"+*"::: ) "iv" ")" )); end; :: deftheorem defines :::"Following"::: CIRCUIT2:def 7 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "holds" (Bool (Set ($#k7_circuit2 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "iv")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit2 :::"Following"::: ) (Set "(" (Set (Var "s")) ($#k1_circuit2 :::"+*"::: ) (Set (Var "iv")) ")" ))))))); definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "SCS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "InpFs" be ($#m2_pboole :::"InputFuncs":::) "of" (Set (Const "SCS")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "SCS")); func :::"InitialComp"::: "(" "s" "," "InpFs" ")" -> ($#m1_subset_1 :::"State":::) "of" "SCS" equals :: CIRCUIT2:def 8 (Set (Set "(" "s" ($#k1_circuit2 :::"+*"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k2_circuit1 :::"-th_InputValues"::: ) "InpFs" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_circuit1 :::"Set-Constants"::: ) "SCS" ")" )); end; :: deftheorem defines :::"InitialComp"::: CIRCUIT2:def 8 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"InputFuncs":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) "holds" (Bool (Set ($#k8_circuit2 :::"InitialComp"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_circuit2 :::"+*"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k2_circuit1 :::"-th_InputValues"::: ) (Set (Var "InpFs")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_circuit1 :::"Set-Constants"::: ) (Set (Var "SCS")) ")" ))))))); definitionlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "SCS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); let "InpFs" be ($#m2_pboole :::"InputFuncs":::) "of" (Set (Const "SCS")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "SCS")); func :::"Computation"::: "(" "s" "," "InpFs" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "SCS") ")" ) means :: CIRCUIT2:def 9 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r8_pboole :::"="::: ) (Set ($#k8_circuit2 :::"InitialComp"::: ) "(" "s" "," "InpFs" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k7_circuit2 :::"Following"::: ) "(" (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_circuit1 :::"-th_InputValues"::: ) "InpFs" ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Computation"::: CIRCUIT2:def 9 : (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"InputFuncs":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "SCS"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r8_pboole :::"="::: ) (Set ($#k8_circuit2 :::"InitialComp"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k7_circuit2 :::"Following"::: ) "(" (Set "(" (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_circuit1 :::"-th_InputValues"::: ) (Set (Var "InpFs")) ")" ) ")" )) ")" ) ")" ) ")" )))))); theorem :: CIRCUIT2:13 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "st" (Bool (Bool (Set ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v")) "," (Set (Var "SCS")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k5_circuit2 :::"IGValue"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" )) ")" )) "holds" (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "st" (Bool (Bool (Set ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v1")) "," (Set (Var "SCS")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_circuit2 :::"IGValue"::: ) "(" (Set (Var "v1")) "," (Set (Var "iv")) ")" )))))))) ; theorem :: CIRCUIT2:14 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"InputFuncs":::) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Bool "not" (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set (Var "iv")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "iv")) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))))))))) ; theorem :: CIRCUIT2:15 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"InputFuncs":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Bool "not" (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))))))))) ; theorem :: CIRCUIT2:16 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"InputFuncs":::) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Bool "not" (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set (Var "iv")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "st" (Bool (Bool (Set ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v")) "," (Set (Var "SCS")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k5_circuit2 :::"IGValue"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ))))))))) ; theorem :: CIRCUIT2:17 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"InputFuncs":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "iv")) "being" ($#m1_msafree2 :::"InputValues"::: ) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Bool "not" (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "iv")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k7_circuit1 :::"depth"::: ) (Set (Var "SCS"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k5_circuit2 :::"IGValue"::: ) "(" (Set (Var "v")) "," (Set (Var "iv")) ")" ))))))))) ; theorem :: CIRCUIT2:18 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"InputFuncs":::) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Bool "not" (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k7_circuit1 :::"depth"::: ) (Set (Var "SCS"))))) "holds" (Bool (Set (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_circuit2 :::"stable"::: ) )))))) ; theorem :: CIRCUIT2:19 (Bool "for" (Set (Var "IIG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"InputFuncs":::) "of" (Set (Var "SCS")) "st" (Bool (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs"))) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Bool "not" (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "SCS")) "holds" (Bool (Set (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s1")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k7_circuit1 :::"depth"::: ) (Set (Var "SCS")) ")" )) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k9_circuit2 :::"Computation"::: ) "(" (Set (Var "s2")) "," (Set (Var "InpFs")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k7_circuit1 :::"depth"::: ) (Set (Var "SCS")) ")" ))))))) ;