:: CIRCUIT1 semantic presentation begin definitionlet "S" 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"::: ) ; mode Circuit of "S" is ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; 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")); func :::"Set-Constants"::: "SCS" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) "IIG") means :: CIRCUIT1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "IIG" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_msualg_2 :::"Constants"::: ) "(" "SCS" "," (Set (Var "x")) ")" ))); end; :: deftheorem defines :::"Set-Constants"::: CIRCUIT1: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"::: ) ($#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 "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_circuit1 :::"Set-Constants"::: ) (Set (Var "SCS")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_msualg_2 :::"Constants"::: ) "(" (Set (Var "SCS")) "," (Set (Var "x")) ")" ))) ")" )))); theorem :: CIRCUIT1: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"::: ) ($#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 "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "SCS"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG")))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k1_msualg_2 :::"Constants"::: ) "(" (Set (Var "SCS")) "," (Set (Var "v")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_circuit1 :::"Set-Constants"::: ) (Set (Var "SCS")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))))))) ; 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 "CS" be ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); mode InputFuncs of "CS" is ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) "IIG" ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "," (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "CS") ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) "IIG" ")" )); end; theorem :: CIRCUIT1: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"::: ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "IIG")) "is" ($#v1_msafree2 :::"with_input_V"::: ) )) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_msafree2 :::"InputValues"::: ) "of" (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"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; assume (Bool (Set (Const "IIG")) "is" ($#v1_msafree2 :::"with_input_V"::: ) ) ; 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 "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "n" :::"-th_InputValues"::: "InpFs" -> ($#m1_msafree2 :::"InputValues"::: ) "of" "SCS" equals :: CIRCUIT1:def 2 (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) "InpFs" ")" ) ($#k1_funct_1 :::"."::: ) "n"); end; :: deftheorem defines :::"-th_InputValues"::: CIRCUIT1: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"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "IIG")) "is" ($#v1_msafree2 :::"with_input_V"::: ) )) "holds" (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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k2_circuit1 :::"-th_InputValues"::: ) (Set (Var "InpFs"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))))); 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 ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); mode State of "SCS" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "SCS")); end; theorem :: CIRCUIT1: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"::: ) ($#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")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))))))) ; theorem :: CIRCUIT1: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"::: ) ($#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 "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "SCS"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))))))) ; 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")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "IIG")); func "o" :::"depends_on_in"::: "s" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" "o" "," "SCS" ")" ) equals :: CIRCUIT1:def 3 (Set "s" ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) "o" ")" )); end; :: deftheorem defines :::"depends_on_in"::: CIRCUIT1: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"::: ) ($#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 "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "IIG")) "holds" (Bool (Set (Set (Var "o")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))))))); theorem :: CIRCUIT1: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 "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "e1")) "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"))) (Bool "for" (Set (Var "q1")) "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 "e1")) ($#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 "q1"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "q1")))) & (Bool (Set (Set (Var "q1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "SCS")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "w"))))) "holds" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")))))))))) ; registrationlet "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"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "IIG")); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "IIG")); cluster -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "SCS" ")" )) ($#k1_funct_1 :::"."::: ) "v"); end; registrationlet "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"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "IIG")); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "IIG")); cluster -> ($#v3_trees_2 :::"DecoratedTree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "SCS" ")" )) ($#k1_funct_1 :::"."::: ) "v"); end; theorem :: CIRCUIT1: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 "SCS")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "e1")) "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"))) (Bool "for" (Set (Var "e2")) "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 "w"))) (Bool "for" (Set (Var "q1")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "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 "e1")) ($#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 "q1")))) & (Bool (Set (Set (Var "k1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "q1")))) & (Bool (Set (Set (Var "q1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "SCS")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "w"))))) "holds" (Bool (Set (Set (Var "e1")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "e2")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Var "SCS")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))))))))))) ; theorem :: CIRCUIT1: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"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "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 (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e"))))) "holds" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "IIG")) "st" (Bool (Set (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ))))))) ; theorem :: CIRCUIT1: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"::: ) ($#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 "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "IIG")) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "SCS")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "o")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "SCS"))) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ))))))) ; theorem :: CIRCUIT1: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 "A")) "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 "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 (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (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"))))))))) ; begin registrationlet "IIG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "IIG")); let "v" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "IIG")); cluster (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "A" ")" )) ($#k1_funct_1 :::"."::: ) "v") -> ($#v1_finset_1 :::"finite"::: ) ; 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"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "IIG")); let "v" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "IIG")); func :::"size"::: "(" "v" "," "A" ")" -> ($#m1_hidden :::"Nat":::) means :: CIRCUIT1:def 4 (Bool "ex" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "t")) ")" ) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "A" ")" )) ($#k1_funct_1 :::"."::: ) "v") : (Bool verum) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "s")))) ")" )); end; :: deftheorem defines :::"size"::: CIRCUIT1: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" )) "iff" (Bool "ex" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "t")) ")" ) where t "is" ($#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 verum) "}" ) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "s")))) ")" )) ")" ))))); theorem :: CIRCUIT1: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IIG")) "holds" (Bool "(" (Bool (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG")) ")" ))) ")" )))) ; theorem :: CIRCUIT1: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"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "e1")) "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"))) (Bool "for" (Set (Var "e2")) "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 "w"))) (Bool "for" (Set (Var "q1")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "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 ($#k5_card_1 :::"card"::: ) (Set (Var "e1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "SCS")) ")" )) & (Bool (Set (Var "e1")) ($#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 "q1")))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q1"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "w")) "," (Set (Var "SCS")) ")" )))))))) ; theorem :: CIRCUIT1: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (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 (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG")) ")" ))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (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 "q"))))))))) ; theorem :: CIRCUIT1: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (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 (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG")) ")" ))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ))) "holds" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "IIG")) "st" (Bool (Set (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG"))) ($#k4_tarski :::"]"::: ) ))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "v" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) (Set (Const "A")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Const "v"))); func :::"depth"::: "e" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: CIRCUIT1:def 5 (Bool "ex" (Set (Var "e9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ")" )) ($#k1_funct_1 :::"."::: ) "v") "st" (Bool "(" (Bool "e" ($#r1_hidden :::"="::: ) (Set (Var "e9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k8_msafree2 :::"depth"::: ) (Set (Var "e9")))) ")" )); end; :: deftheorem defines :::"depth"::: CIRCUIT1:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (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 "b5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_circuit1 :::"depth"::: ) (Set (Var "e")))) "iff" (Bool "ex" (Set (Var "e9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Var "e9"))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_msafree2 :::"depth"::: ) (Set (Var "e9")))) ")" )) ")" )))))); theorem :: CIRCUIT1:14 (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"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IIG")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" )))) "holds" (Bool (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "w")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ))))) ; theorem :: CIRCUIT1:15 (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"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "IIG")) "holds" (Bool (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: CIRCUIT1:16 (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 "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")) "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 "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "ek")) "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 "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" )) "st" (Bool "(" (Bool (Set (Var "ek")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "ek"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) "," (Set (Var "A")) ")" )) ")" )) ")" )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k4_circuit1 :::"size"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ))))))) ; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "v" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); func :::"depth"::: "(" "v" "," "A" ")" -> ($#m1_hidden :::"Nat":::) means :: CIRCUIT1:def 6 (Bool "ex" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k5_circuit1 :::"depth"::: ) (Set (Var "t")) ")" ) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k5_msafree2 :::"FreeEnv"::: ) "A" ")" )) ($#k1_funct_1 :::"."::: ) "v") : (Bool verum) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "s")))) ")" )); end; :: deftheorem defines :::"depth"::: CIRCUIT1:def 6 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v5_msafree2 :::"monotonic"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" )) "iff" (Bool "ex" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k5_circuit1 :::"depth"::: ) (Set (Var "t")) ")" ) where t "is" ($#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 verum) "}" ) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "s")))) ")" )) ")" ))))); definitionlet "IIG" be ($#~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"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "IIG")); func :::"depth"::: "A" -> ($#m1_hidden :::"Nat":::) means :: CIRCUIT1:def 7 (Bool "ex" (Set (Var "Ds")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "Ds")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v")) "," "A" ")" ")" ) where v "is" ($#m1_subset_1 :::"Element":::) "of" "IIG" : (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IIG")) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "Ds")))) ")" )); end; :: deftheorem defines :::"depth"::: CIRCUIT1:def 7 : (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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "IIG")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_circuit1 :::"depth"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "Ds")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "Ds")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ")" ) where v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IIG")) : (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IIG")))) "}" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "Ds")))) ")" )) ")" )))); theorem :: CIRCUIT1: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 "A")) "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")) "holds" (Bool (Set ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_circuit1 :::"depth"::: ) (Set (Var "A"))))))) ; theorem :: CIRCUIT1:18 (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 "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "IIG")) "holds" (Bool "(" (Bool (Set ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "IIG")))) "or" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_msafree2 :::"SortsWithConstants"::: ) (Set (Var "IIG")))) ")" ) ")" )))) ; theorem :: CIRCUIT1:19 (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"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "IIG")) (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "IIG")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "IIG")))) & (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v")) ")" ) ")" )))) "holds" (Bool (Set ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v1")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_circuit1 :::"depth"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ))))) ;