:: ABCMIZ_A semantic presentation begin theorem :: ABCMIZ_A:1 (Bool "for" (Set (Var "x")) "being" ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ))) ; scheme :: ABCMIZ_A:sch 1 MinimalElement{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "not" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))])) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool "not" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "z"))])) proof end; scheme :: ABCMIZ_A:sch 2 FiniteC{ F1() -> ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F1 "(" ")" )]) provided (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "A")))) "holds" (Bool P1[(Set (Var "B"))]) ")" )) "holds" (Bool P1[(Set (Var "A"))])) proof end; scheme :: ABCMIZ_A:sch 3 Numeration{ F1() -> ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "s")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s")))) & (Bool P1[(Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))])) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool "not" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "z"))])) proof end; theorem :: ABCMIZ_A:2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"variable":::) "holds" (Bool (Set ($#k1_abcmiz_1 :::"varcl"::: ) (Set "(" ($#k3_abcmiz_1 :::"vars"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_abcmiz_1 :::"vars"::: ) (Set (Var "x"))))) ; theorem :: ABCMIZ_A:3 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "e")) "is" ($#v5_abcmiz_1 :::"compound"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "holds" (Bool (Bool "not" (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k35_abcmiz_1 :::"-term"::: ) (Set (Var "C")))))) ")" ))) ; begin registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_abcmiz_1 :::"QuasiLoci"::: ) ); end; definitionlet "C" be ($#l1_msualg_1 :::"ConstructorSignature":::); attr "C" is :::"standardized"::: means :: ABCMIZ_A:def 1 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "C" "st" (Bool (Bool (Set (Var "o")) "is" ($#v2_abcmiz_1 :::"constructor"::: ) )) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) & (Bool (Set (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "o")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) ")" )); end; :: deftheorem defines :::"standardized"::: ABCMIZ_A:def 1 : (Bool "for" (Set (Var "C")) "being" ($#l1_msualg_1 :::"ConstructorSignature":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_abcmiz_a :::"standardized"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o")) "is" ($#v2_abcmiz_1 :::"constructor"::: ) )) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) & (Bool (Set (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "o")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) ")" )) ")" )); theorem :: ABCMIZ_A:4 (Bool "for" (Set (Var "C")) "being" ($#l1_msualg_1 :::"ConstructorSignature":::) "st" (Bool (Bool (Set (Var "C")) "is" ($#v1_abcmiz_a :::"standardized"::: ) )) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v2_abcmiz_1 :::"constructor"::: ) ) "iff" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) ")" ))) ; registration cluster (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) -> ($#v1_abcmiz_a :::"standardized"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_msualg_1 :::"strict"::: ) bbbadV1_INSTALG1() ($#v1_abcmiz_1 :::"constructor"::: ) ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "c" be ($#v2_abcmiz_1 :::"constructor"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "C")); func :::"loci_of"::: "c" -> ($#m2_finseq_2 :::"quasi-loci":::) equals :: ABCMIZ_A:def 2 (Set (Set "(" "c" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); end; :: deftheorem defines :::"loci_of"::: ABCMIZ_A:def 2 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "c")) "being" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_abcmiz_a :::"loci_of"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )))); registrationlet "C" be ($#l1_msualg_1 :::"ConstructorSignature":::); cluster bbbadV1_INSTALG1() ($#v1_abcmiz_1 :::"constructor"::: ) for ($#m1_instalg1 :::"Subsignature"::: ) "of" "C"; end; registrationlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() bbbadV1_INSTALG1() ($#v1_abcmiz_1 :::"constructor"::: ) ($#v3_abcmiz_1 :::"initialized"::: ) for ($#m1_instalg1 :::"Subsignature"::: ) "of" "C"; end; registrationlet "C" be ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#v1_abcmiz_1 :::"constructor"::: ) -> ($#v1_abcmiz_1 :::"constructor"::: ) ($#v1_abcmiz_a :::"standardized"::: ) for ($#m1_instalg1 :::"Subsignature"::: ) "of" "C"; end; theorem :: ABCMIZ_A:5 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) "st" (Bool (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S2"))))) "holds" (Bool (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S2"))) "#)" ))) ; theorem :: ABCMIZ_A:6 (Bool "for" (Set (Var "C")) "being" ($#l1_msualg_1 :::"ConstructorSignature":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_abcmiz_a :::"standardized"::: ) ) "iff" (Bool (Set (Var "C")) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )) ")" )) ; registrationlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) ($#v3_trees_9 :::"finite-branching"::: ) ($#~v5_abcmiz_1 "non" ($#v5_abcmiz_1 :::"compound"::: ) ) for ($#m1_abcmiz_1 :::"expression"::: ) "of" "C" "," (Set ($#k14_abcmiz_1 :::"a_Term"::: ) "C"); end; registration cluster -> ($#v1_xtuple_0 :::"pair"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ); end; theorem :: ABCMIZ_A:7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "st" (Bool (Bool (Set ($#k3_abcmiz_1 :::"vars"::: ) (Set (Var "x"))) "is" ($#v7_ordinal1 :::"natural"::: ) )) "holds" (Bool (Set ($#k3_abcmiz_1 :::"vars"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ABCMIZ_A:8 (Bool (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) ; theorem :: ABCMIZ_A:9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_abcmiz_1 :::"*"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k10_abcmiz_1 :::"non_op"::: ) )) ")" )) ; theorem :: ABCMIZ_A:10 (Bool "for" (Set (Var "C")) "being" ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) "holds" (Bool (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))))) ; theorem :: ABCMIZ_A:11 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k35_abcmiz_1 :::"-term"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k8_abcmiz_1 :::"a_Term"::: ) ) ($#k4_tarski :::"]"::: ) )) ")" )) "or" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "st" (Bool "(" (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 "C"))) ($#k4_tarski :::"]"::: ) )) & (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) "or" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k9_abcmiz_1 :::"*"::: ) )) "or" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k10_abcmiz_1 :::"non_op"::: ) )) ")" ) ")" )) ")" ))) ; registrationlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "e" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); cluster (Set "e" ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) -> ($#v1_xtuple_0 :::"pair"::: ) ; end; theorem :: ABCMIZ_A:12 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "st" (Bool (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 "C"))) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "e")) "is" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))))))) ; theorem :: ABCMIZ_A:13 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_abcmiz_1 :::"*"::: ) ))) "implies" (Bool (Set (Var "e")) "is" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k12_abcmiz_1 :::"a_Type"::: ) (Set (Var "C")))) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_abcmiz_1 :::"non_op"::: ) ))) "implies" (Bool (Set (Var "e")) "is" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k13_abcmiz_1 :::"an_Adj"::: ) (Set (Var "C")))) ")" ")" ))) ; theorem :: ABCMIZ_A:14 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool "(" (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_abcmiz_1 :::"Vars"::: ) )) & (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_abcmiz_1 :::"a_Term"::: ) )) & (Bool (Set (Var "e")) "is" ($#m1_abcmiz_1 :::"quasi-term":::) "of" (Set (Var "C"))) ")" ) "or" (Bool "(" (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) & (Bool "(" (Bool "(" (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) & (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C")))) ")" ) "or" (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_abcmiz_1 :::"*"::: ) )) "or" (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_abcmiz_1 :::"non_op"::: ) )) ")" ) ")" ) ")" ))) ; theorem :: ABCMIZ_A:15 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ))) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "C")) "," (Set "(" ($#k28_abcmiz_1 :::"MSVars"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ))))) ; theorem :: ABCMIZ_A:16 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Bool "not" (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_abcmiz_1 :::"Vars"::: ) ))) "iff" (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) "is" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C"))) ")" ))) ; theorem :: ABCMIZ_A:17 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_abcmiz_1 :::"Vars"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k35_abcmiz_1 :::"-term"::: ) (Set (Var "C")))) ")" )))) ; theorem :: ABCMIZ_A:18 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_abcmiz_1 :::"*"::: ) ))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k13_abcmiz_1 :::"an_Adj"::: ) (Set (Var "C")))(Bool "ex" (Set (Var "q")) "being" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k12_abcmiz_1 :::"a_Type"::: ) (Set (Var "C"))) "st" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k9_abcmiz_1 :::"*"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "a")) "," (Set (Var "q")) ")" )))))) ; theorem :: ABCMIZ_A:19 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_abcmiz_1 :::"non_op"::: ) ))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k13_abcmiz_1 :::"an_Adj"::: ) (Set (Var "C"))) "st" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k10_abcmiz_1 :::"non_op"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) ) ($#k5_trees_4 :::"-tree"::: ) (Set (Var "a"))))))) ; theorem :: ABCMIZ_A:20 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ))) "holds" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "e")) "is" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")))) ")" )))) ; theorem :: ABCMIZ_A:21 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t")) "being" ($#m1_abcmiz_1 :::"quasi-term":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t")) "is" ($#v5_abcmiz_1 :::"compound"::: ) ) "iff" (Bool "(" (Bool (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_abcmiz_1 :::"a_Term"::: ) )) ")" ) ")" ))) ; theorem :: ABCMIZ_A:22 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t")) "is" ($#~v5_abcmiz_1 "non" ($#v5_abcmiz_1 :::"compound"::: ) ) ($#m1_abcmiz_1 :::"quasi-term":::) "of" (Set (Var "C"))) "iff" (Bool (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_abcmiz_1 :::"Vars"::: ) )) ")" ))) ; theorem :: ABCMIZ_A:23 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t")) "is" ($#m1_abcmiz_1 :::"quasi-term":::) "of" (Set (Var "C"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_abcmiz_1 :::"a_Term"::: ) )) ")" ) "or" (Bool (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_abcmiz_1 :::"Vars"::: ) )) ")" ) ")" ))) ; theorem :: ABCMIZ_A:24 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v6_abcmiz_1 :::"positive"::: ) ($#m1_abcmiz_1 :::"quasi-adjective":::) "of" (Set (Var "C"))) "iff" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_abcmiz_1 :::"an_Adj"::: ) )) ")" ) ")" ))) ; theorem :: ABCMIZ_A:25 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "a")) "being" ($#m1_abcmiz_1 :::"quasi-adjective":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v7_abcmiz_1 :::"negative"::: ) ) "iff" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_abcmiz_1 :::"non_op"::: ) )) ")" ))) ; theorem :: ABCMIZ_A:26 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#v1_abcmiz_a :::"standardized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t")) "is" ($#v9_abcmiz_1 :::"pure"::: ) ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k12_abcmiz_1 :::"a_Type"::: ) (Set (Var "C")))) "iff" (Bool "(" (Bool (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_abcmiz_1 :::"a_Type"::: ) )) ")" ) ")" ))) ; begin definitionmode expression is ($#m1_subset_1 :::"expression":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ); mode valuation is ($#m1_subset_1 :::"valuation":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ); mode quasi-adjective is ($#m1_abcmiz_1 :::"quasi-adjective":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ); func :::"QuasiAdjs"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) "," (Set "(" ($#k28_abcmiz_1 :::"MSVars"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) ")" ) ")" ")" ) equals :: ABCMIZ_A:def 3 (Set ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )); mode quasi-term is ($#m1_abcmiz_1 :::"quasi-term":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ); func :::"QuasiTerms"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) "," (Set "(" ($#k28_abcmiz_1 :::"MSVars"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) ")" ) ")" ")" ) equals :: ABCMIZ_A:def 4 (Set ($#k34_abcmiz_1 :::"QuasiTerms"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )); mode quasi-type is ($#m3_abcmiz_1 :::"quasi-type"::: ) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ); func :::"QuasiTypes"::: -> ($#m1_hidden :::"set"::: ) equals :: ABCMIZ_A:def 5 (Set ($#k39_abcmiz_1 :::"QuasiTypes"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )); end; :: deftheorem defines :::"QuasiAdjs"::: ABCMIZ_A:def 3 : (Bool (Set ($#k2_abcmiz_a :::"QuasiAdjs"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ))); :: deftheorem defines :::"QuasiTerms"::: ABCMIZ_A:def 4 : (Bool (Set ($#k3_abcmiz_a :::"QuasiTerms"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k34_abcmiz_1 :::"QuasiTerms"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ))); :: deftheorem defines :::"QuasiTypes"::: ABCMIZ_A:def 5 : (Bool (Set ($#k4_abcmiz_a :::"QuasiTypes"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k39_abcmiz_1 :::"QuasiTypes"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ))); registration cluster (Set ($#k2_abcmiz_a :::"QuasiAdjs"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k3_abcmiz_a :::"QuasiTerms"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k4_abcmiz_a :::"QuasiTypes"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definition:: original: :::"Modes"::: redefine func :::"Modes"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ); :: original: :::"Attrs"::: redefine func :::"Attrs"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ); :: original: :::"Funcs"::: redefine func :::"Funcs"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ); end; definitionfunc :::"set-constr"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_abcmiz_a :::"Modes"::: ) ) equals :: ABCMIZ_A:def 6 (Set ($#k4_tarski :::"["::: ) (Set ($#k6_abcmiz_1 :::"a_Type"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"set-constr"::: ABCMIZ_A:def 6 : (Bool (Set ($#k8_abcmiz_a :::"set-constr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_abcmiz_1 :::"a_Type"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )); theorem :: ABCMIZ_A:27 (Bool "(" (Bool (Set ($#k23_abcmiz_1 :::"kind_of"::: ) (Set ($#k8_abcmiz_a :::"set-constr"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_abcmiz_1 :::"a_Type"::: ) )) & (Bool (Set ($#k25_abcmiz_1 :::"loci_of"::: ) (Set ($#k8_abcmiz_a :::"set-constr"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k26_abcmiz_1 :::"index_of"::: ) (Set ($#k8_abcmiz_a :::"set-constr"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: ABCMIZ_A:28 (Bool (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_abcmiz_1 :::"a_Type"::: ) ) "," (Set ($#k7_abcmiz_1 :::"an_Adj"::: ) ) "," (Set ($#k8_abcmiz_1 :::"a_Term"::: ) ) ($#k1_enumset1 :::"}"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_abcmiz_1 :::"QuasiLoci"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ; theorem :: ABCMIZ_A:29 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_2 :::"quasi-loci":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "l")) ")" ) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_abcmiz_1 :::"Vars"::: ) )) & (Bool (Set (Set (Var "l")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "l")) ")" ) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) )) "is" ($#m2_finseq_2 :::"quasi-loci":::)) ")" ))) ; theorem :: ABCMIZ_A:30 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "l")) "being" ($#m2_finseq_2 :::"quasi-loci":::) "st" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))))) ; theorem :: ABCMIZ_A:31 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) (Bool "ex" (Set (Var "l")) "being" ($#m2_finseq_2 :::"quasi-loci":::) "st" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k1_abcmiz_1 :::"varcl"::: ) (Set (Var "X")))))) ; theorem :: ABCMIZ_A:32 (Bool "for" (Set (Var "X")) "," (Set (Var "o")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "ex" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "C")) "," (Set "(" ($#k28_abcmiz_1 :::"MSVars"::: ) (Set (Var "C")) ")" ) ")" ")" ))))) & (Bool (Set (Set (Var "o")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "p")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X"))))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "e" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); mode :::"subexpression"::: "of" "e" -> ($#m1_subset_1 :::"expression":::) "of" "C" means :: ABCMIZ_A:def 7 (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_9 :::"Subtrees"::: ) "e")); func :::"constrs"::: "e" -> ($#m1_hidden :::"set"::: ) equals :: ABCMIZ_A:def 8 (Set (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "e" ")" ) ")" ) ($#k3_xboole_0 :::"/\"::: ) "{" (Set (Var "o")) where o "is" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" "C" : (Bool verum) "}" ); func :::"main-constr"::: "e" -> ($#m1_hidden :::"set"::: ) equals :: ABCMIZ_A:def 9 (Set (Set "(" "e" ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) if (Bool "e" "is" ($#v5_abcmiz_1 :::"compound"::: ) ) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); func :::"args"::: "e" -> ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" "C" "," (Set "(" ($#k28_abcmiz_1 :::"MSVars"::: ) "C" ")" ) ")" ")" ) means :: ABCMIZ_A:def 10 (Bool "e" ($#r1_hidden :::"="::: ) (Set (Set "(" "e" ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k4_trees_4 :::"-tree"::: ) it)); end; :: deftheorem defines :::"subexpression"::: ABCMIZ_A:def 7 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_abcmiz_a :::"subexpression"::: ) "of" (Set (Var "e"))) "iff" (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_9 :::"Subtrees"::: ) (Set (Var "e")))) ")" ))); :: deftheorem defines :::"constrs"::: ABCMIZ_A:def 8 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k9_abcmiz_a :::"constrs"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "e")) ")" ) ")" ) ($#k3_xboole_0 :::"/\"::: ) "{" (Set (Var "o")) where o "is" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) : (Bool verum) "}" )))); :: deftheorem defines :::"main-constr"::: ABCMIZ_A:def 9 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "e")) "is" ($#v5_abcmiz_1 :::"compound"::: ) )) "implies" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "e")) "is" ($#v5_abcmiz_1 :::"compound"::: ) ))) "implies" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))); :: deftheorem defines :::"args"::: ABCMIZ_A:def 10 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Var "C")) "," (Set "(" ($#k28_abcmiz_1 :::"MSVars"::: ) (Set (Var "C")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_abcmiz_a :::"args"::: ) (Set (Var "e")))) "iff" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "b3")))) ")" )))); theorem :: ABCMIZ_A:33 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool (Set (Var "e")) "is" ($#m1_abcmiz_a :::"subexpression"::: ) "of" (Set (Var "e"))))) ; theorem :: ABCMIZ_A:34 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"variable":::) (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) "holds" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set "(" (Set (Var "x")) ($#k35_abcmiz_1 :::"-term"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ABCMIZ_A:35 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "c")) "being" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k34_abcmiz_1 :::"QuasiTerms"::: ) (Set (Var "C"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "c")) ")" )))) "holds" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set "(" (Set (Var "c")) ($#k36_abcmiz_1 :::"-trm"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "c")))))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "e" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); attr "e" is :::"constructor"::: means :: ABCMIZ_A:def 11 (Bool "(" (Bool "e" "is" ($#v5_abcmiz_1 :::"compound"::: ) ) & (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) "e") "is" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" "C") ")" ); end; :: deftheorem defines :::"constructor"::: ABCMIZ_A:def 11 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "e")) "is" ($#v2_abcmiz_a :::"constructor"::: ) ) "iff" (Bool "(" (Bool (Set (Var "e")) "is" ($#v5_abcmiz_1 :::"compound"::: ) ) & (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set (Var "e"))) "is" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C"))) ")" ) ")" ))); registrationlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#v2_abcmiz_a :::"constructor"::: ) -> ($#v5_abcmiz_1 :::"compound"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" "C" "," (Set "(" ($#k28_abcmiz_1 :::"MSVars"::: ) "C" ")" ) ")" ")" ))); end; registrationlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) ($#v3_trees_9 :::"finite-branching"::: ) ($#v2_abcmiz_a :::"constructor"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" "C" "," (Set "(" ($#k28_abcmiz_1 :::"MSVars"::: ) "C" ")" ) ")" ")" ))); end; registrationlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "e" be ($#v2_abcmiz_a :::"constructor"::: ) ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) ($#v3_trees_9 :::"finite-branching"::: ) ($#v2_abcmiz_a :::"constructor"::: ) for ($#m1_abcmiz_a :::"subexpression"::: ) "of" "e"; end; registrationlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::); let "X" be bbbadV3_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_msafree3 :::"Free"::: ) "(" (Set (Const "S")) "," (Set (Const "X")) ")" ")" ); cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) "t") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; theorem :: ABCMIZ_A:36 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "e")) "being" ($#v2_abcmiz_a :::"constructor"::: ) ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_abcmiz_a :::"constrs"::: ) (Set (Var "e")))))) ; begin definitionlet "C" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::); attr "C" is :::"arity-rich"::: means :: ABCMIZ_A:def 12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "C" "holds" (Bool "{" (Set (Var "o")) where o "is" ($#m1_subset_1 :::"OperSymbol":::) "of" "C" : (Bool "(" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" ) "}" "is" ($#v1_finset_1 :::"infinite"::: ) ))); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "C")); attr "o" is :::"nullary"::: means :: ABCMIZ_A:def 13 (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "o") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); attr "o" is :::"unary"::: means :: ABCMIZ_A:def 14 (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) "o" ")" )) ($#r1_hidden :::"="::: ) (Num 1)); attr "o" is :::"binary"::: means :: ABCMIZ_A:def 15 (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) "o" ")" )) ($#r1_hidden :::"="::: ) (Num 2)); end; :: deftheorem defines :::"arity-rich"::: ABCMIZ_A:def 12 : (Bool "for" (Set (Var "C")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_abcmiz_a :::"arity-rich"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "C")) "holds" (Bool "{" (Set (Var "o")) where o "is" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) : (Bool "(" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" ) "}" "is" ($#v1_finset_1 :::"infinite"::: ) ))) ")" )); :: deftheorem defines :::"nullary"::: ABCMIZ_A:def 13 : (Bool "for" (Set (Var "C")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v4_abcmiz_a :::"nullary"::: ) ) "iff" (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))); :: deftheorem defines :::"unary"::: ABCMIZ_A:def 14 : (Bool "for" (Set (Var "C")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v5_abcmiz_a :::"unary"::: ) ) "iff" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))); :: deftheorem defines :::"binary"::: ABCMIZ_A:def 15 : (Bool "for" (Set (Var "C")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v6_abcmiz_a :::"binary"::: ) ) "iff" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )) ($#r1_hidden :::"="::: ) (Num 2)) ")" ))); theorem :: ABCMIZ_A:37 (Bool "for" (Set (Var "C")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"Signature":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "o")) "is" ($#v4_abcmiz_a :::"nullary"::: ) )) "implies" (Bool "not" (Bool (Set (Var "o")) "is" ($#v5_abcmiz_a :::"unary"::: ) )) ")" & "(" (Bool (Bool (Set (Var "o")) "is" ($#v4_abcmiz_a :::"nullary"::: ) )) "implies" (Bool "not" (Bool (Set (Var "o")) "is" ($#v6_abcmiz_a :::"binary"::: ) )) ")" & "(" (Bool (Bool (Set (Var "o")) "is" ($#v5_abcmiz_a :::"unary"::: ) )) "implies" (Bool "not" (Bool (Set (Var "o")) "is" ($#v6_abcmiz_a :::"binary"::: ) )) ")" ")" ))) ; registrationlet "C" be ($#l1_msualg_1 :::"ConstructorSignature":::); cluster (Set ($#k15_abcmiz_1 :::"non_op"::: ) "C") -> ($#v5_abcmiz_a :::"unary"::: ) ; cluster (Set ($#k16_abcmiz_1 :::"ast"::: ) "C") -> ($#v6_abcmiz_a :::"binary"::: ) ; end; registrationlet "C" be ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#v4_abcmiz_a :::"nullary"::: ) -> ($#v2_abcmiz_1 :::"constructor"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C"); end; theorem :: ABCMIZ_A:38 (Bool "for" (Set (Var "C")) "being" ($#l1_msualg_1 :::"ConstructorSignature":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_abcmiz_1 :::"initialized"::: ) ) "iff" (Bool "ex" (Set (Var "m")) "being" ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set ($#k12_abcmiz_1 :::"a_Type"::: ) (Set (Var "C")))(Bool "ex" (Set (Var "a")) "being" ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set ($#k13_abcmiz_1 :::"an_Adj"::: ) (Set (Var "C"))) "st" (Bool "(" (Bool (Set (Var "m")) "is" ($#v4_abcmiz_a :::"nullary"::: ) ) & (Bool (Set (Var "a")) "is" ($#v4_abcmiz_a :::"nullary"::: ) ) ")" ))) ")" )) ; registrationlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#v2_abcmiz_1 :::"constructor"::: ) ($#v4_abcmiz_a :::"nullary"::: ) for ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set ($#k12_abcmiz_1 :::"a_Type"::: ) "C"); cluster ($#v2_abcmiz_1 :::"constructor"::: ) ($#v4_abcmiz_a :::"nullary"::: ) for ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set ($#k13_abcmiz_1 :::"an_Adj"::: ) "C"); end; registrationlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#v2_abcmiz_1 :::"constructor"::: ) ($#v4_abcmiz_a :::"nullary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C"); end; registration cluster ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV1_INSTALG1() ($#v3_abcmiz_a :::"arity-rich"::: ) -> ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v12_abcmiz_1 :::"with_an_operation_for_each_sort"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster bbbadV1_INSTALG1() ($#v1_abcmiz_1 :::"constructor"::: ) ($#v3_abcmiz_a :::"arity-rich"::: ) -> ($#v3_abcmiz_1 :::"initialized"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registration cluster (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) -> ($#v3_abcmiz_a :::"arity-rich"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() bbbadV1_INSTALG1() ($#v1_abcmiz_1 :::"constructor"::: ) ($#v3_abcmiz_1 :::"initialized"::: ) ($#v3_abcmiz_a :::"arity-rich"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registrationlet "C" be ($#v3_abcmiz_a :::"arity-rich"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "C")); cluster ($#v2_abcmiz_1 :::"constructor"::: ) ($#v4_abcmiz_a :::"nullary"::: ) for ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" "s"; cluster ($#v2_abcmiz_1 :::"constructor"::: ) ($#v5_abcmiz_a :::"unary"::: ) for ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" "s"; cluster ($#v2_abcmiz_1 :::"constructor"::: ) ($#v6_abcmiz_a :::"binary"::: ) for ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" "s"; end; registrationlet "C" be ($#v3_abcmiz_a :::"arity-rich"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); cluster ($#v2_abcmiz_1 :::"constructor"::: ) ($#v5_abcmiz_a :::"unary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C"); cluster ($#v2_abcmiz_1 :::"constructor"::: ) ($#v6_abcmiz_a :::"binary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C"); end; theorem :: ABCMIZ_A:39 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "o")) "being" ($#v4_abcmiz_a :::"nullary"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "is" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set (Var "C")) "," (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")))))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "m" be ($#v2_abcmiz_1 :::"constructor"::: ) ($#v4_abcmiz_a :::"nullary"::: ) ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set ($#k12_abcmiz_1 :::"a_Type"::: ) (Set (Const "C"))); :: original: :::"term"::: redefine func "m" :::"term"::: -> ($#v9_abcmiz_1 :::"pure"::: ) ($#m1_abcmiz_1 :::"expression"::: ) "of" "C" "," (Set ($#k12_abcmiz_1 :::"a_Type"::: ) "C"); end; definitionlet "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ); func :::"@"::: "c" -> ($#v2_abcmiz_1 :::"constructor"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) equals :: ABCMIZ_A:def 16 "c"; end; :: deftheorem defines :::"@"::: ABCMIZ_A:def 16 : (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ) "holds" (Bool (Set ($#k13_abcmiz_a :::"@"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "c")))); definitionlet "m" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_abcmiz_a :::"Modes"::: ) ); :: original: :::"@"::: redefine func :::"@"::: "m" -> ($#v2_abcmiz_1 :::"constructor"::: ) ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set ($#k12_abcmiz_1 :::"a_Type"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )); end; registration cluster (Set ($#k13_abcmiz_a :::"@"::: ) (Set ($#k8_abcmiz_a :::"set-constr"::: ) )) -> ($#v2_abcmiz_1 :::"constructor"::: ) ($#v4_abcmiz_a :::"nullary"::: ) ; end; theorem :: ABCMIZ_A:40 (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k14_abcmiz_a :::"@"::: ) (Set ($#k8_abcmiz_a :::"set-constr"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; definitionfunc :::"set-type"::: -> ($#m3_abcmiz_1 :::"quasi-type":::) equals :: ABCMIZ_A:def 17 (Set (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) ")" ) ")" ) ($#k40_abcmiz_1 :::"ast"::: ) (Set "(" (Set "(" ($#k14_abcmiz_a :::"@"::: ) (Set ($#k8_abcmiz_a :::"set-constr"::: ) ) ")" ) ($#k12_abcmiz_a :::"term"::: ) ")" )); end; :: deftheorem defines :::"set-type"::: ABCMIZ_A:def 17 : (Bool (Set ($#k15_abcmiz_a :::"set-type"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) ")" ) ")" ) ($#k40_abcmiz_1 :::"ast"::: ) (Set "(" (Set "(" ($#k14_abcmiz_a :::"@"::: ) (Set ($#k8_abcmiz_a :::"set-constr"::: ) ) ")" ) ($#k12_abcmiz_a :::"term"::: ) ")" ))); theorem :: ABCMIZ_A:41 (Bool "(" (Bool (Set ($#k41_abcmiz_1 :::"adjs"::: ) (Set ($#k15_abcmiz_a :::"set-type"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k42_abcmiz_1 :::"the_base_of"::: ) (Set ($#k15_abcmiz_a :::"set-type"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_abcmiz_a :::"@"::: ) (Set ($#k8_abcmiz_a :::"set-constr"::: ) ) ")" ) ($#k12_abcmiz_a :::"term"::: ) )) ")" ) ; definitionlet "l" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ); func :::"args"::: "l" -> ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k34_abcmiz_1 :::"QuasiTerms"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )) means :: ABCMIZ_A:def 18 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "l")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "l"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "l" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k35_abcmiz_1 :::"-term"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ))) ")" ) ")" ); end; :: deftheorem defines :::"args"::: ABCMIZ_A:def 18 : (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k34_abcmiz_1 :::"QuasiTerms"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_abcmiz_a :::"args"::: ) (Set (Var "l")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "l"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k35_abcmiz_1 :::"-term"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ))) ")" ) ")" ) ")" ))); definitionlet "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ); func :::"base_exp_of"::: "c" -> ($#m1_subset_1 :::"expression":::) equals :: ABCMIZ_A:def 19 (Set (Set "(" ($#k13_abcmiz_a :::"@"::: ) "c" ")" ) ($#k36_abcmiz_1 :::"-trm"::: ) (Set "(" ($#k16_abcmiz_a :::"args"::: ) (Set "(" ($#k25_abcmiz_1 :::"loci_of"::: ) "c" ")" ) ")" )); end; :: deftheorem defines :::"base_exp_of"::: ABCMIZ_A:def 19 : (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k20_abcmiz_1 :::"Constructors"::: ) ) "holds" (Bool (Set ($#k17_abcmiz_a :::"base_exp_of"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_abcmiz_a :::"@"::: ) (Set (Var "c")) ")" ) ($#k36_abcmiz_1 :::"-trm"::: ) (Set "(" ($#k16_abcmiz_a :::"args"::: ) (Set "(" ($#k25_abcmiz_1 :::"loci_of"::: ) (Set (Var "c")) ")" ) ")" )))); theorem :: ABCMIZ_A:42 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v2_abcmiz_1 :::"constructor"::: ) ) "iff" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k20_abcmiz_1 :::"Constructors"::: ) )) ")" )) ; theorem :: ABCMIZ_A:43 (Bool "for" (Set (Var "m")) "being" ($#v4_abcmiz_a :::"nullary"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) "holds" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set "(" (Set (Var "m")) ($#k29_abcmiz_1 :::"term"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m")))) ; theorem :: ABCMIZ_A:44 (Bool "for" (Set (Var "m")) "being" ($#v2_abcmiz_1 :::"constructor"::: ) ($#v5_abcmiz_a :::"unary"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m1_abcmiz_1 :::"quasi-term":::) "holds" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set "(" (Set (Var "m")) ($#k30_abcmiz_1 :::"term"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m"))))) ; theorem :: ABCMIZ_A:45 (Bool "for" (Set (Var "a")) "being" ($#m1_abcmiz_1 :::"quasi-adjective":::) "holds" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set "(" (Set "(" ($#k32_abcmiz_1 :::"non_op"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) ")" ) ($#k30_abcmiz_1 :::"term"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_abcmiz_1 :::"non_op"::: ) ))) ; theorem :: ABCMIZ_A:46 (Bool "for" (Set (Var "m")) "being" ($#v2_abcmiz_1 :::"constructor"::: ) ($#v6_abcmiz_a :::"binary"::: ) ($#m1_subset_1 :::"OperSymbol":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_abcmiz_1 :::"quasi-term":::) "holds" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set "(" (Set (Var "m")) ($#k31_abcmiz_1 :::"term"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m"))))) ; theorem :: ABCMIZ_A:47 (Bool "for" (Set (Var "q")) "being" ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) "," (Set ($#k12_abcmiz_1 :::"a_Type"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )) (Bool "for" (Set (Var "a")) "being" ($#m1_abcmiz_1 :::"quasi-adjective":::) "holds" (Bool (Set ($#k10_abcmiz_a :::"main-constr"::: ) (Set "(" (Set "(" ($#k33_abcmiz_1 :::"ast"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) ")" ) ($#k31_abcmiz_1 :::"term"::: ) "(" (Set (Var "a")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_abcmiz_1 :::"*"::: ) )))) ; definitionlet "T" be ($#m3_abcmiz_1 :::"quasi-type":::); func :::"constrs"::: "T" -> ($#m1_hidden :::"set"::: ) equals :: ABCMIZ_A:def 20 (Set (Set "(" ($#k9_abcmiz_a :::"constrs"::: ) (Set "(" ($#k42_abcmiz_1 :::"the_base_of"::: ) "T" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k9_abcmiz_a :::"constrs"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_abcmiz_1 :::"quasi-adjective":::) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k41_abcmiz_1 :::"adjs"::: ) "T")) "}" ")" )); end; :: deftheorem defines :::"constrs"::: ABCMIZ_A:def 20 : (Bool "for" (Set (Var "T")) "being" ($#m3_abcmiz_1 :::"quasi-type":::) "holds" (Bool (Set ($#k18_abcmiz_a :::"constrs"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_abcmiz_a :::"constrs"::: ) (Set "(" ($#k42_abcmiz_1 :::"the_base_of"::: ) (Set (Var "T")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k9_abcmiz_a :::"constrs"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_abcmiz_1 :::"quasi-adjective":::) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k41_abcmiz_1 :::"adjs"::: ) (Set (Var "T")))) "}" ")" )))); theorem :: ABCMIZ_A:48 (Bool "for" (Set (Var "q")) "being" ($#v9_abcmiz_1 :::"pure"::: ) ($#m1_abcmiz_1 :::"expression"::: ) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) "," (Set ($#k12_abcmiz_1 :::"a_Type"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) ")" ) "holds" (Bool (Set ($#k18_abcmiz_a :::"constrs"::: ) (Set "(" (Set (Var "A")) ($#k40_abcmiz_1 :::"ast"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_abcmiz_a :::"constrs"::: ) (Set (Var "q")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k9_abcmiz_a :::"constrs"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_abcmiz_1 :::"quasi-adjective":::) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ")" ))))) ; theorem :: ABCMIZ_A:49 (Bool "for" (Set (Var "a")) "being" ($#m1_abcmiz_1 :::"quasi-adjective":::) (Bool "for" (Set (Var "T")) "being" ($#m3_abcmiz_1 :::"quasi-type":::) "holds" (Bool (Set ($#k18_abcmiz_a :::"constrs"::: ) (Set "(" (Set (Var "a")) ($#k43_abcmiz_1 :::"ast"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_abcmiz_a :::"constrs"::: ) (Set (Var "a")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k18_abcmiz_a :::"constrs"::: ) (Set (Var "T")) ")" ))))) ; begin definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "t", "p" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); pred "t" :::"matches_with"::: "p" means :: ABCMIZ_A:def 21 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" "C" "st" (Bool "t" ($#r1_hidden :::"="::: ) (Set "p" ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "f"))))); reflexivity (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Const "C")) "st" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "f")))))) ; end; :: deftheorem defines :::"matches_with"::: ABCMIZ_A:def 21 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_abcmiz_a :::"matches_with"::: ) (Set (Var "p"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Var "C")) "st" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "f"))))) ")" ))); theorem :: ABCMIZ_A:50 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "t3")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "t1")) ($#r1_abcmiz_a :::"matches_with"::: ) (Set (Var "t2"))) & (Bool (Set (Var "t2")) ($#r1_abcmiz_a :::"matches_with"::: ) (Set (Var "t3")))) "holds" (Bool (Set (Var "t1")) ($#r1_abcmiz_a :::"matches_with"::: ) (Set (Var "t3"))))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set (Const "C")) ")" ); pred "A" :::"matches_with"::: "B" means :: ABCMIZ_A:def 22 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" "C" "st" (Bool (Set "B" ($#k63_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) "A")); reflexivity (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set (Const "C")) ")" ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Const "C")) "st" (Bool (Set (Set (Var "A")) ($#k63_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ; end; :: deftheorem defines :::"matches_with"::: ABCMIZ_A:def 22 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_abcmiz_a :::"matches_with"::: ) (Set (Var "B"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Var "C")) "st" (Bool (Set (Set (Var "B")) ($#k63_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ")" ))); theorem :: ABCMIZ_A:51 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k38_abcmiz_1 :::"QuasiAdjs"::: ) (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "A1")) ($#r2_abcmiz_a :::"matches_with"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A2")) ($#r2_abcmiz_a :::"matches_with"::: ) (Set (Var "A3")))) "holds" (Bool (Set (Var "A1")) ($#r2_abcmiz_a :::"matches_with"::: ) (Set (Var "A3"))))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "T", "P" be ($#m3_abcmiz_1 :::"quasi-type"::: ) "of" (Set (Const "C")); pred "T" :::"matches_with"::: "P" means :: ABCMIZ_A:def 23 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" "C" "st" (Bool "(" (Bool (Set (Set "(" ($#k41_abcmiz_1 :::"adjs"::: ) "P" ")" ) ($#k63_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k41_abcmiz_1 :::"adjs"::: ) "T")) & (Bool (Set (Set "(" ($#k42_abcmiz_1 :::"the_base_of"::: ) "P" ")" ) ($#k62_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k42_abcmiz_1 :::"the_base_of"::: ) "T")) ")" )); reflexivity (Bool "for" (Set (Var "T")) "being" ($#m3_abcmiz_1 :::"quasi-type"::: ) "of" (Set (Const "C")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Const "C")) "st" (Bool "(" (Bool (Set (Set "(" ($#k41_abcmiz_1 :::"adjs"::: ) (Set (Var "T")) ")" ) ($#k63_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k41_abcmiz_1 :::"adjs"::: ) (Set (Var "T")))) & (Bool (Set (Set "(" ($#k42_abcmiz_1 :::"the_base_of"::: ) (Set (Var "T")) ")" ) ($#k62_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k42_abcmiz_1 :::"the_base_of"::: ) (Set (Var "T")))) ")" ))) ; end; :: deftheorem defines :::"matches_with"::: ABCMIZ_A:def 23 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "T")) "," (Set (Var "P")) "being" ($#m3_abcmiz_1 :::"quasi-type"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "T")) ($#r3_abcmiz_a :::"matches_with"::: ) (Set (Var "P"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Set "(" ($#k41_abcmiz_1 :::"adjs"::: ) (Set (Var "P")) ")" ) ($#k63_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k41_abcmiz_1 :::"adjs"::: ) (Set (Var "T")))) & (Bool (Set (Set "(" ($#k42_abcmiz_1 :::"the_base_of"::: ) (Set (Var "P")) ")" ) ($#k62_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k42_abcmiz_1 :::"the_base_of"::: ) (Set (Var "T")))) ")" )) ")" ))); theorem :: ABCMIZ_A:52 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "T3")) "being" ($#m3_abcmiz_1 :::"quasi-type"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "T1")) ($#r3_abcmiz_a :::"matches_with"::: ) (Set (Var "T2"))) & (Bool (Set (Var "T2")) ($#r3_abcmiz_a :::"matches_with"::: ) (Set (Var "T3")))) "holds" (Bool (Set (Var "T1")) ($#r3_abcmiz_a :::"matches_with"::: ) (Set (Var "T3"))))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "t1", "t2" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); let "f" be ($#m1_subset_1 :::"valuation":::) "of" (Set (Const "C")); pred "f" :::"unifies"::: "t1" "," "t2" means :: ABCMIZ_A:def 24 (Bool (Set "t1" ($#k56_abcmiz_1 :::"at"::: ) "f") ($#r1_hidden :::"="::: ) (Set "t2" ($#k56_abcmiz_1 :::"at"::: ) "f")); end; :: deftheorem defines :::"unifies"::: ABCMIZ_A:def 24 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) (Set (Var "t1")) "," (Set (Var "t2"))) "iff" (Bool (Set (Set (Var "t1")) ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "f")))) ")" )))); theorem :: ABCMIZ_A:53 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) (Set (Var "t1")) "," (Set (Var "t2")))) "holds" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) (Set (Var "t2")) "," (Set (Var "t1")))))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "t1", "t2" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); pred "t1" "," "t2" :::"are_unifiable"::: means :: ABCMIZ_A:def 25 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" "C" "st" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) "t1" "," "t2")); reflexivity (Bool "for" (Set (Var "t1")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Const "C")) "st" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) (Set (Var "t1")) "," (Set (Var "t1"))))) ; symmetry (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")) "st" (Bool (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Const "C")) "st" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) (Set (Var "t1")) "," (Set (Var "t2"))))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Const "C")) "st" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) (Set (Var "t2")) "," (Set (Var "t1"))))) ; end; :: deftheorem defines :::"are_unifiable"::: ABCMIZ_A:def 25 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t1")) "," (Set (Var "t2")) ($#r5_abcmiz_a :::"are_unifiable"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Var "C")) "st" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) (Set (Var "t1")) "," (Set (Var "t2")))) ")" ))); definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "t1", "t2" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); pred "t1" "," "t2" :::"are_weakly-unifiable"::: means :: ABCMIZ_A:def 26 (Bool "ex" (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#v15_abcmiz_1 :::"irrelevant"::: ) ($#m1_subset_1 :::"valuation":::) "of" "C" "st" (Bool "(" (Bool (Set ($#k45_abcmiz_1 :::"variables_in"::: ) "t2") ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool "t1" "," (Set "t2" ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "g"))) ($#r5_abcmiz_a :::"are_unifiable"::: ) ) ")" )); reflexivity (Bool "for" (Set (Var "t1")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")) (Bool "ex" (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#v15_abcmiz_1 :::"irrelevant"::: ) ($#m1_subset_1 :::"valuation":::) "of" (Set (Const "C")) "st" (Bool "(" (Bool (Set ($#k45_abcmiz_1 :::"variables_in"::: ) (Set (Var "t1"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "t1")) "," (Set (Set (Var "t1")) ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "g"))) ($#r5_abcmiz_a :::"are_unifiable"::: ) ) ")" ))) ; end; :: deftheorem defines :::"are_weakly-unifiable"::: ABCMIZ_A:def 26 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t1")) "," (Set (Var "t2")) ($#r6_abcmiz_a :::"are_weakly-unifiable"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#v15_abcmiz_1 :::"irrelevant"::: ) ($#m1_subset_1 :::"valuation":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set ($#k45_abcmiz_1 :::"variables_in"::: ) (Set (Var "t2"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "t1")) "," (Set (Set (Var "t2")) ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "g"))) ($#r5_abcmiz_a :::"are_unifiable"::: ) ) ")" )) ")" ))); theorem :: ABCMIZ_A:54 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "t1")) "," (Set (Var "t2")) ($#r5_abcmiz_a :::"are_unifiable"::: ) )) "holds" (Bool (Set (Var "t1")) "," (Set (Var "t2")) ($#r6_abcmiz_a :::"are_weakly-unifiable"::: ) ))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "t", "t1", "t2" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); pred "t" :::"is_a_unification_of"::: "t1" "," "t2" means :: ABCMIZ_A:def 27 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" "C" "st" (Bool "(" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) "t1" "," "t2") & (Bool "t" ($#r1_hidden :::"="::: ) (Set "t1" ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "f")))) ")" )); end; :: deftheorem defines :::"is_a_unification_of"::: ABCMIZ_A:def 27 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r7_abcmiz_a :::"is_a_unification_of"::: ) (Set (Var "t1")) "," (Set (Var "t2"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"valuation":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r4_abcmiz_a :::"unifies"::: ) (Set (Var "t1")) "," (Set (Var "t2"))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t1")) ($#k56_abcmiz_1 :::"at"::: ) (Set (Var "f")))) ")" )) ")" ))); theorem :: ABCMIZ_A:55 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "t")) ($#r7_abcmiz_a :::"is_a_unification_of"::: ) (Set (Var "t1")) "," (Set (Var "t2")))) "holds" (Bool (Set (Var "t")) ($#r7_abcmiz_a :::"is_a_unification_of"::: ) (Set (Var "t2")) "," (Set (Var "t1"))))) ; theorem :: ABCMIZ_A:56 (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "t")) ($#r7_abcmiz_a :::"is_a_unification_of"::: ) (Set (Var "t1")) "," (Set (Var "t2")))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_abcmiz_a :::"matches_with"::: ) (Set (Var "t1"))) & (Bool (Set (Var "t")) ($#r1_abcmiz_a :::"matches_with"::: ) (Set (Var "t2"))) ")" ))) ; definitionlet "C" be ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::); let "t", "t1", "t2" be ($#m1_subset_1 :::"expression":::) "of" (Set (Const "C")); pred "t" :::"is_a_general-unification_of"::: "t1" "," "t2" means :: ABCMIZ_A:def 28 (Bool "(" (Bool "t" ($#r7_abcmiz_a :::"is_a_unification_of"::: ) "t1" "," "t2") & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"expression":::) "of" "C" "st" (Bool (Bool (Set (Var "u")) ($#r7_abcmiz_a :::"is_a_unification_of"::: ) "t1" "," "t2")) "holds" (Bool (Set (Var "u")) ($#r1_abcmiz_a :::"matches_with"::: ) "t") ")" ) ")" ); end; :: deftheorem defines :::"is_a_general-unification_of"::: ABCMIZ_A:def 28 : (Bool "for" (Set (Var "C")) "being" ($#v3_abcmiz_1 :::"initialized"::: ) ($#l1_msualg_1 :::"ConstructorSignature":::) (Bool "for" (Set (Var "t")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r8_abcmiz_a :::"is_a_general-unification_of"::: ) (Set (Var "t1")) "," (Set (Var "t2"))) "iff" (Bool "(" (Bool (Set (Var "t")) ($#r7_abcmiz_a :::"is_a_unification_of"::: ) (Set (Var "t1")) "," (Set (Var "t2"))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"expression":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "u")) ($#r7_abcmiz_a :::"is_a_unification_of"::: ) (Set (Var "t1")) "," (Set (Var "t2")))) "holds" (Bool (Set (Var "u")) ($#r1_abcmiz_a :::"matches_with"::: ) (Set (Var "t"))) ")" ) ")" ) ")" ))); begin theorem :: ABCMIZ_A:57 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set (Var "s")) "st" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))))) ; theorem :: ABCMIZ_A:58 (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_2 :::"quasi-loci":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set (Var "s")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l"))))) "holds" (Bool (Set ($#k45_abcmiz_1 :::"variables_in"::: ) (Set "(" (Set (Var "m")) ($#k36_abcmiz_1 :::"-trm"::: ) (Set "(" ($#k16_abcmiz_a :::"args"::: ) (Set (Var "l")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l"))))))) ; theorem :: ABCMIZ_A:59 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "st" (Bool (Bool (Set ($#k1_abcmiz_1 :::"varcl"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#v2_abcmiz_1 :::"constructor"::: ) ($#m2_abcmiz_1 :::"OperSymbol"::: ) "of" (Set (Var "s"))(Bool "ex" (Set (Var "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k34_abcmiz_1 :::"QuasiTerms"::: ) (Set ($#k27_abcmiz_1 :::"MaxConstrSign"::: ) )) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "m")) ")" ))) & (Bool (Set ($#k46_abcmiz_1 :::"vars"::: ) (Set "(" (Set (Var "m")) ($#k36_abcmiz_1 :::"-trm"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))))) ; definitionlet "d" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "," (Set ($#k4_abcmiz_a :::"QuasiTypes"::: ) ); attr "d" is :::"even"::: means :: ABCMIZ_A:def 29 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"variable":::) (Bool "for" (Set (Var "T")) "being" ($#m3_abcmiz_1 :::"quasi-type":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "d")) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set "d" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k48_abcmiz_1 :::"vars"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k3_abcmiz_1 :::"vars"::: ) (Set (Var "x")))))); end; :: deftheorem defines :::"even"::: ABCMIZ_A:def 29 : (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "," (Set ($#k4_abcmiz_a :::"QuasiTypes"::: ) ) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#v7_abcmiz_a :::"even"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"variable":::) (Bool "for" (Set (Var "T")) "being" ($#m3_abcmiz_1 :::"quasi-type":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "d")))) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k48_abcmiz_1 :::"vars"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k3_abcmiz_1 :::"vars"::: ) (Set (Var "x")))))) ")" )); definitionlet "l" be ($#m2_finseq_2 :::"quasi-loci":::); mode :::"type-distribution"::: "of" "l" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "," (Set ($#k4_abcmiz_a :::"QuasiTypes"::: ) ) means :: ABCMIZ_A:def 30 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) "l")) & (Bool it "is" ($#v7_abcmiz_a :::"even"::: ) ) ")" ); end; :: deftheorem defines :::"type-distribution"::: ABCMIZ_A:def 30 : (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_2 :::"quasi-loci":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_abcmiz_1 :::"Vars"::: ) ) "," (Set ($#k4_abcmiz_a :::"QuasiTypes"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_abcmiz_a :::"type-distribution"::: ) "of" (Set (Var "l"))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l")))) & (Bool (Set (Var "b2")) "is" ($#v7_abcmiz_a :::"even"::: ) ) ")" ) ")" ))); theorem :: ABCMIZ_A:60 (Bool "for" (Set (Var "l")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m2_finseq_2 :::"quasi-loci":::) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m2_abcmiz_a :::"type-distribution"::: ) "of" (Set (Var "l")))) ;