:: OSAFREE semantic presentation begin definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); mode :::"OSGeneratorSet"::: "of" "U0" -> ($#m3_pboole :::"MSSubset":::) "of" "U0" means :: OSAFREE:def 1 (Bool "for" (Set (Var "O")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" "U0" "st" (Bool (Bool (Set (Var "O")) ($#r8_pboole :::"="::: ) (Set ($#k2_osalg_2 :::"OSCl"::: ) it))) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "O")) ")" )) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U0"))); end; :: deftheorem defines :::"OSGeneratorSet"::: OSAFREE:def 1 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_osafree :::"OSGeneratorSet"::: ) "of" (Set (Var "U0"))) "iff" (Bool "for" (Set (Var "O")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "O")) ($#r8_pboole :::"="::: ) (Set ($#k2_osalg_2 :::"OSCl"::: ) (Set (Var "b3"))))) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "O")) ")" )) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U0"))))) ")" )))); theorem :: OSAFREE:1 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#m1_osafree :::"OSGeneratorSet"::: ) "of" (Set (Var "U0"))) "iff" (Bool "for" (Set (Var "O")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "O")) ($#r8_pboole :::"="::: ) (Set ($#k2_osalg_2 :::"OSCl"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Var "U0")))) ")" )))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); let "IT" be ($#m1_osafree :::"OSGeneratorSet"::: ) "of" (Set (Const "U0")); attr "IT" is :::"osfree"::: means :: OSAFREE:def 2 (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" "S" (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" "IT" "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) (Bool "ex" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" "U0" "," (Set (Var "U1")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) "U0" "," (Set (Var "U1"))) & (Bool (Set (Var "h")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) & (Bool (Set (Set (Var "h")) ($#k1_msafree :::"||"::: ) "IT") ($#r8_pboole :::"="::: ) (Set (Var "f"))) ")" )))); end; :: deftheorem defines :::"osfree"::: OSAFREE:def 2 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "IT")) "being" ($#m1_osafree :::"OSGeneratorSet"::: ) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_osafree :::"osfree"::: ) ) "iff" (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "IT")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) (Bool "ex" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U0")) "," (Set (Var "U1")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U0")) "," (Set (Var "U1"))) & (Bool (Set (Var "h")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) & (Bool (Set (Set (Var "h")) ($#k1_msafree :::"||"::: ) (Set (Var "IT"))) ($#r8_pboole :::"="::: ) (Set (Var "f"))) ")" )))) ")" )))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "IT" be ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); attr "IT" is :::"osfree"::: means :: OSAFREE:def 3 (Bool "ex" (Set (Var "G")) "being" ($#m1_osafree :::"OSGeneratorSet"::: ) "of" "IT" "st" (Bool (Set (Var "G")) "is" ($#v1_osafree :::"osfree"::: ) )); end; :: deftheorem defines :::"osfree"::: OSAFREE:def 3 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "IT")) "being" ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_osafree :::"osfree"::: ) ) "iff" (Bool "ex" (Set (Var "G")) "being" ($#m1_osafree :::"OSGeneratorSet"::: ) "of" (Set (Var "IT")) "st" (Bool (Set (Var "G")) "is" ($#v1_osafree :::"osfree"::: ) )) ")" ))); begin definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"OSREL"::: "X" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) means :: OSAFREE:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" )) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))))) ")" & "(" (Bool (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" )))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool "(" (Bool (Set (Var "i")) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree :::"coprod"::: ) "(" (Set (Var "i")) "," "X" ")" )) ")" )) ")" ")" ) ")" ) ")" ) ")" ) ")" ) ")" ))); end; :: deftheorem defines :::"OSREL"::: OSAFREE:def 4 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_osafree :::"OSREL"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ) ")" )) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))))) ")" & "(" (Bool (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" )))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree :::"coprod"::: ) "(" (Set (Var "i")) "," (Set (Var "X")) ")" )) ")" )) ")" ")" ) ")" ) ")" ) ")" ) ")" ) ")" ))) ")" )))); theorem :: OSAFREE:2 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_osafree :::"OSREL"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))))) ")" & "(" (Bool (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" )))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree :::"coprod"::: ) "(" (Set (Var "i")) "," (Set (Var "X")) ")" )) ")" )) ")" ")" ) ")" ) ")" ) ")" ))))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"DTConOSA"::: "X" -> ($#l1_lang1 :::"DTConstrStr"::: ) equals :: OSAFREE:def 5 (Set ($#g1_lang1 :::"DTConstrStr"::: ) "(#" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) "X" ")" ) ")" ) ")" ) "," (Set "(" ($#k1_osafree :::"OSREL"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"DTConOSA"::: OSAFREE:def 5 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_lang1 :::"DTConstrStr"::: ) "(#" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) "," (Set "(" ($#k1_osafree :::"OSREL"::: ) (Set (Var "X")) ")" ) "#)" )))); registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); cluster (Set ($#k2_osafree :::"DTConOSA"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lang1 :::"strict"::: ) ; end; theorem :: OSAFREE:3 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k2_lang1 :::"NonTerminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k1_lang1 :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k3_msafree :::"coprod"::: ) (Set (Var "X")) ")" ))) ")" ))) ; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); cluster (Set ($#k2_osafree :::"DTConOSA"::: ) "X") -> ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_dtconstr :::"with_useful_nonterminals"::: ) ; end; theorem :: OSAFREE:4 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) "iff" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" )))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); func :::"OSSym"::: "(" "o" "," "X" ")" -> ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) equals :: OSAFREE:def 6 (Set ($#k4_tarski :::"["::: ) "o" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"OSSym"::: OSAFREE:def 6 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ))))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func :::"ParsedTerms"::: "(" "X" "," "s" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) ")" ) equals :: OSAFREE:def 7 "{" (Set (Var "a")) where a "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) : (Bool "(" (Bool "ex" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" "S"(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) "s") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "s1")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ))) ")" ))) "or" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r3_orders_2 :::"<="::: ) "s") ")" )) ")" ) "}" ; end; :: deftheorem defines :::"ParsedTerms"::: OSAFREE:def 7 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_osafree :::"ParsedTerms"::: ) "(" (Set (Var "X")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) : (Bool "(" (Bool "ex" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ))) ")" ))) "or" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s"))) ")" )) ")" ) "}" )))); registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k4_osafree :::"ParsedTerms"::: ) "(" "X" "," "s" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"ParsedTerms"::: "X" -> ($#m1_hidden :::"OrderSortedSet":::) "of" "S" means :: OSAFREE:def 8 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_osafree :::"ParsedTerms"::: ) "(" "X" "," (Set (Var "s")) ")" ))); end; :: deftheorem defines :::"ParsedTerms"::: OSAFREE:def 8 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_osafree :::"ParsedTerms"::: ) "(" (Set (Var "X")) "," (Set (Var "s")) ")" ))) ")" )))); registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); cluster (Set ($#k5_osafree :::"ParsedTerms"::: ) "X") -> bbbadV2_RELAT_1() ; end; theorem :: OSAFREE:5 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) "holds" (Bool (Set (Var "x")) "is" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))))))) ; theorem :: OSAFREE:6 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_osafree :::"ParsedTerms"::: ) "(" (Set (Var "X")) "," (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" ) ")" ))))) ; theorem :: OSAFREE:7 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) ")" ))))) ; theorem :: OSAFREE:8 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); func :::"PTDenOp"::: "(" "o" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) "X" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S") ")" ) ($#k1_funct_1 :::"."::: ) "o" ")" ) "," (Set "(" (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) "X" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S") ")" ) ($#k1_funct_1 :::"."::: ) "o" ")" ) means :: OSAFREE:def 9 (Bool "for" (Set (Var "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) "st" (Bool (Bool (Set ($#k3_osafree :::"OSSym"::: ) "(" "o" "," "X" ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "p"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_osafree :::"OSSym"::: ) "(" "o" "," "X" ")" ")" ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p"))))); end; :: deftheorem defines :::"PTDenOp"::: OSAFREE:def 9 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_osafree :::"PTDenOp"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set ($#k3_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ")" ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p"))))) ")" ))))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"PTOper"::: "X" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) "X" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S")) "," (Set (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) "X" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S")) means :: OSAFREE:def 10 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "holds" (Bool (Set it ($#k5_msualg_4 :::"."::: ) (Set (Var "o"))) ($#r2_funct_2 :::"="::: ) (Set ($#k6_osafree :::"PTDenOp"::: ) "(" (Set (Var "o")) "," "X" ")" ))); end; :: deftheorem defines :::"PTOper"::: OSAFREE:def 10 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S")))) "," (Set (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_osafree :::"PTOper"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k5_msualg_4 :::"."::: ) (Set (Var "o"))) ($#r2_funct_2 :::"="::: ) (Set ($#k6_osafree :::"PTDenOp"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ))) ")" )))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"ParsedTermsOSA"::: "X" -> ($#l3_msualg_1 :::"OSAlgebra":::) "of" "S" equals :: OSAFREE:def 11 (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) "X" ")" ) "," (Set "(" ($#k7_osafree :::"PTOper"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"ParsedTermsOSA"::: OSAFREE:def 11 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "(" ($#k5_osafree :::"ParsedTerms"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k7_osafree :::"PTOper"::: ) (Set (Var "X")) ")" ) "#)" )))); registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); cluster (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) "X") -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ; end; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); :: original: :::"OSSym"::: redefine func :::"OSSym"::: "(" "o" "," "X" ")" -> ($#m2_subset_1 :::"NonTerminal":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ); end; theorem :: OSAFREE:9 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) : (Bool "(" (Bool "ex" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ))) ")" ))) "or" (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s"))) ")" )) ")" ) "}" )))) ; theorem :: OSAFREE:10 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "," (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool "(" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) & "(" (Bool (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "implies" (Bool (Set (Var "s")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s1"))) ")" & "(" (Bool (Bool (Set (Var "s")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s1")))) "implies" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")))) ")" ")" ))))) ; theorem :: OSAFREE:11 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool "ex" (Set (Var "p")) "being" ($#m2_dtconstr :::"SubtreeSeq"::: ) "of" (Set ($#k9_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) "st" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ")" ) ($#k9_dtconstr :::"-tree"::: ) (Set (Var "p")))) & (Bool (Set ($#k9_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "p")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" )) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p")))) ")" )) & (Bool "(" "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s2")) ($#k4_tarski :::"]"::: ) )))) ")" ) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")))) "iff" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s1"))) ")" ) ")" ) ")" ))))) ; theorem :: OSAFREE:12 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "ts"))))) "holds" (Bool "(" (Bool (Set (Var "nt")) ($#r2_hidden :::"in"::: ) (Set ($#k7_dtconstr :::"NonTerminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set (Var "nt")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) & (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "ts")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" )) & (Bool (Set (Set (Var "nt")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "ts")))) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Set (Var "nt")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")))) "iff" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s1"))) ")" ) ")" ) ")" )) ")" ))))) ; theorem :: OSAFREE:13 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" )) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) & (Bool (Set ($#k9_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k14_trees_3 :::"roots"::: ) (Set (Var "x")))) ")" ) ")" ))))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "t" be ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" )); func :::"LeastSort"::: "t" -> ($#m1_subset_1 :::"SortSymbol":::) "of" "S" means :: OSAFREE:def 12 (Bool "(" (Bool "t" ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) it)) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool (Bool "t" ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "holds" (Bool it ($#r3_orders_2 :::"<="::: ) (Set (Var "s1"))) ")" ) ")" ); end; :: deftheorem defines :::"LeastSort"::: OSAFREE:def 12 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_osafree :::"LeastSort"::: ) (Set (Var "t")))) "iff" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "b4")))) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "holds" (Bool (Set (Var "b4")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s1"))) ")" ) ")" ) ")" ))))); 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"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); mode Element of "A" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A")); end; theorem :: OSAFREE:14 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) ")" )))) ; theorem :: OSAFREE:15 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "x")) "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))))))) ; theorem :: OSAFREE:16 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set ($#k10_osafree :::"LeastSort"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s")))))))) ; theorem :: OSAFREE:17 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k10_osafree :::"LeastSort"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))))))))) ; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "o2" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); cluster (Set ($#k3_msualg_1 :::"Args"::: ) "(" "o2" "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" ) ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "x" be ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" )); func :::"LeastSorts"::: "x" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k3_finseq_2 :::"*"::: ) ) means :: OSAFREE:def 13 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "x")) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "x"))) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) "st" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set "x" ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k10_osafree :::"LeastSort"::: ) (Set (Var "t")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"LeastSorts"::: OSAFREE:def 13 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_osafree :::"LeastSorts"::: ) (Set (Var "x")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x")))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x"))))) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k10_osafree :::"LeastSort"::: ) (Set (Var "t")))) ")" )) ")" ) ")" ) ")" ))))); theorem :: OSAFREE:18 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set ($#k11_osafree :::"LeastSorts"::: ) (Set (Var "x"))) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" )) ")" ))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v5_osalg_1 :::"discernable"::: ) ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; definitionlet "S" be ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "x" be ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" )); assume (Bool (Set ($#k9_osafree :::"OSSym"::: ) "(" (Set "(" ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Const "o")) "," (Set "(" ($#k11_osafree :::"LeastSorts"::: ) (Set (Const "x")) ")" ) ")" ")" ) "," (Set (Const "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Const "x")))) ; func :::"pi"::: "(" "o" "," "x" ")" -> ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) equals :: OSAFREE:def 14 (Set (Set "(" ($#k9_osafree :::"OSSym"::: ) "(" (Set "(" ($#k2_osalg_1 :::"LBound"::: ) "(" "o" "," (Set "(" ($#k11_osafree :::"LeastSorts"::: ) "x" ")" ) ")" ")" ) "," "X" ")" ")" ) ($#k8_trees_4 :::"-tree"::: ) "x"); end; :: deftheorem defines :::"pi"::: OSAFREE:def 14 : (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set ($#k9_osafree :::"OSSym"::: ) "(" (Set "(" ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_osafree :::"LeastSorts"::: ) (Set (Var "x")) ")" ) ")" ")" ) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k12_osafree :::"pi"::: ) "(" (Set (Var "o")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_osafree :::"OSSym"::: ) "(" (Set "(" ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_osafree :::"LeastSorts"::: ) (Set (Var "x")) ")" ) ")" ")" ) "," (Set (Var "X")) ")" ")" ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "x")))))))); definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" ); assume (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Const "t")) ($#r1_lang1 :::"==>"::: ) (Set (Var "p")))) ; func :::"@"::: "(" "X" "," "t" ")" -> ($#m1_subset_1 :::"OperSymbol":::) "of" "S" means :: OSAFREE:def 15 (Bool (Set ($#k4_tarski :::"["::: ) it "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) "t"); end; :: deftheorem defines :::"@"::: OSAFREE:def 15 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "t")) ($#r1_lang1 :::"==>"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k13_osafree :::"@"::: ) "(" (Set (Var "X")) "," (Set (Var "t")) ")" )) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b4")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" ))))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" ); assume (Bool (Set (Const "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" ))) ; func :::"pi"::: "t" -> ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) equals :: OSAFREE:def 16 (Set ($#k2_trees_4 :::"root-tree"::: ) "t"); end; :: deftheorem defines :::"pi"::: OSAFREE:def 16 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k14_osafree :::"pi"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t"))))))); definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"LCongruence"::: "X" -> ($#v3_osalg_4 :::"monotone"::: ) ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) "X") means :: OSAFREE:def 17 (Bool "for" (Set (Var "R")) "being" ($#v3_osalg_4 :::"monotone"::: ) ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) "X") "holds" (Bool it ($#r2_pboole :::"c="::: ) (Set (Var "R")))); end; :: deftheorem defines :::"LCongruence"::: OSAFREE:def 17 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#v3_osalg_4 :::"monotone"::: ) ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_osafree :::"LCongruence"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "R")) "being" ($#v3_osalg_4 :::"monotone"::: ) ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) "holds" (Bool (Set (Var "b3")) ($#r2_pboole :::"c="::: ) (Set (Var "R")))) ")" )))); definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"FreeOSA"::: "X" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" "S" equals :: OSAFREE:def 18 (Set ($#k16_osalg_4 :::"QuotOSAlg"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) "X" ")" ) ")" ); end; :: deftheorem defines :::"FreeOSA"::: OSAFREE:def 18 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k16_osafree :::"FreeOSA"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k16_osalg_4 :::"QuotOSAlg"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) (Set (Var "X")) ")" ) ")" )))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" ); func :::"@"::: "t" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k2_zfmisc_1 :::":]"::: ) ) equals :: OSAFREE:def 19 "{" (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) "t" ")" ) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ) where s1 "is" ($#m1_subset_1 :::"Element":::) "of" "S" : (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S"(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool "t" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "s")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s1"))) ")" ))) "}" ; end; :: deftheorem defines :::"@"::: OSAFREE:def 19 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k17_osafree :::"@"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" ) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ) where s1 "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "s")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s1"))) ")" ))) "}" )))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "nt" be ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" ); let "x" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) ($#k2_zfmisc_1 :::":]"::: ) )); func :::"@"::: "(" "nt" "," "x" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k2_zfmisc_1 :::":]"::: ) ) equals :: OSAFREE:def 20 "{" (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x2")) ")" ) "," (Set (Var "s3")) ($#k4_tarski :::"]"::: ) ) where o2 "is" ($#m1_subset_1 :::"OperSymbol":::) "of" "S", x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" ) ")" ), s3 "is" ($#m1_subset_1 :::"Element":::) "of" "S" : (Bool "(" (Bool "ex" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool "(" (Bool "nt" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "o1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2")) ")" ))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s3"))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s3"))) ")" )) & (Bool "ex" (Set (Var "w3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "x")) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "x"))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "w3")) ($#k7_partfun1 :::"/."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "x" ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" )) ")" ) "}" ; end; :: deftheorem defines :::"@"::: OSAFREE:def 20 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k2_zfmisc_1 :::":]"::: ) )) "holds" (Bool (Set ($#k18_osafree :::"@"::: ) "(" (Set (Var "nt")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x2")) ")" ) "," (Set (Var "s3")) ($#k4_tarski :::"]"::: ) ) where o2 "is" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")), x2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ), s3 "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool "(" (Bool "ex" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "o1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2")) ")" ))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s3"))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s3"))) ")" )) & (Bool "ex" (Set (Var "w3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x")))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "w3")) ($#k7_partfun1 :::"/."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" )) ")" ) "}" ))))); definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"PTClasses"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) means :: OSAFREE:def 21 (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_osafree :::"@"::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "ts"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_osafree :::"@"::: ) "(" (Set (Var "nt")) "," (Set "(" it ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"PTClasses"::: OSAFREE:def 21 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_osafree :::"@"::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "ts"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_osafree :::"@"::: ) "(" (Set (Var "nt")) "," (Set "(" (Set (Var "b3")) ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ) ")" ))) ")" ) ")" ) ")" )))); theorem :: OSAFREE:19 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "y")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) ")" ) ")" )))) ; theorem :: OSAFREE:20 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "y")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))))))) ; theorem :: OSAFREE:21 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "s2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" ))))) ; theorem :: OSAFREE:22 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z")))))))) ; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"PTCongruence"::: "X" -> ($#v2_msualg_4 :::"MSEquivalence-like"::: ) ($#m1_osalg_4 :::"OrderSortedRelation"::: ) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) "X") means :: OSAFREE:def 22 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) where x, y "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) : (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) "X" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) "}" )); end; :: deftheorem defines :::"PTCongruence"::: OSAFREE:def 22 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#v2_msualg_4 :::"MSEquivalence-like"::: ) ($#m1_osalg_4 :::"OrderSortedRelation"::: ) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) where x, y "is" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) : (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) "}" )) ")" )))); theorem :: OSAFREE:23 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" )))) ; theorem :: OSAFREE:24 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#m2_subset_1 :::"Component":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_osalg_4 :::"CompClass"::: ) "(" (Set "(" ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")) ")" ) "," (Set (Var "C")) ")" )) "iff" (Bool "ex" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" )) ")" ))))) ; theorem :: OSAFREE:25 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set ($#k8_osalg_4 :::"OSClass"::: ) "(" (Set "(" ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set "(" ($#k19_osafree :::"PTClasses"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))))))) ; theorem :: OSAFREE:26 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r8_pboole :::"="::: ) (Set ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) "implies" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ) ")" ) "," (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k1_msualg_4 :::"."::: ) (Set (Var "s2")))) ")" & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ) ")" ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k1_msualg_4 :::"."::: ) (Set (Var "s2")))) "or" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k1_msualg_4 :::"."::: ) (Set (Var "s2")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s1")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o1")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ) (Bool "for" (Set (Var "s3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o1")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x2")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k1_msualg_4 :::"."::: ) (Set (Var "s3")))) "iff" (Bool "(" (Bool (Set (Var "o1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2")) ")" ))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s3"))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s3"))) & (Bool "ex" (Set (Var "w3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x1")))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w3"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x1")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k1_msualg_4 :::"."::: ) (Set "(" (Set (Var "w3")) ($#k7_partfun1 :::"/."::: ) (Set (Var "y")) ")" ))) ")" ) ")" )) ")" ) ")" )))) ")" ) ")" ) ")" )))) ; theorem :: OSAFREE:27 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X"))) "is" ($#v3_osalg_4 :::"monotone"::: ) ))) ; registrationlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); cluster (Set ($#k20_osafree :::"PTCongruence"::: ) "X") -> ($#v2_msualg_4 :::"MSEquivalence-like"::: ) ($#v3_osalg_4 :::"monotone"::: ) ; end; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func :::"PTVars"::: "(" "s" "," "X" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) "s" ")" ) means :: OSAFREE:def 23 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k1_funct_1 :::"."::: ) "s")) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," "s" ($#k4_tarski :::"]"::: ) ))) ")" )) ")" )); end; :: deftheorem defines :::"PTVars"::: OSAFREE:def 23 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k21_osafree :::"PTVars"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))) ")" )) ")" )) ")" ))))); registrationlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k21_osafree :::"PTVars"::: ) "(" "s" "," "X" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: OSAFREE:28 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k21_osafree :::"PTVars"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" ) where t "is" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) : (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set (Var "t")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ) "}" )))) ; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"PTVars"::: "X" -> ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" ) means :: OSAFREE:def 24 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k21_osafree :::"PTVars"::: ) "(" (Set (Var "s")) "," "X" ")" ))); end; :: deftheorem defines :::"PTVars"::: OSAFREE:def 24 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k22_osafree :::"PTVars"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k21_osafree :::"PTVars"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ))) ")" )))); theorem :: OSAFREE:29 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k22_osafree :::"PTVars"::: ) (Set (Var "X"))) "is" bbbadV2_RELAT_1()))) ; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func :::"OSFreeGen"::: "(" "s" "," "X" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k16_osafree :::"FreeOSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) "s" ")" ) means :: OSAFREE:def 25 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k1_funct_1 :::"."::: ) "s")) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k18_osalg_4 :::"OSNat_Hom"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) "X" ")" ) ")" ")" ) ($#k1_msualg_3 :::"."::: ) "s" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," "s" ($#k4_tarski :::"]"::: ) ) ")" ))) ")" )) ")" )); end; :: deftheorem defines :::"OSFreeGen"::: OSAFREE:def 25 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k16_osafree :::"FreeOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k23_osafree :::"OSFreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k18_osalg_4 :::"OSNat_Hom"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" ))) ")" )) ")" )) ")" ))))); registrationlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k23_osafree :::"OSFreeGen"::: ) "(" "s" "," "X" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: OSAFREE:30 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k23_osafree :::"OSFreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" (Set "(" ($#k18_osalg_4 :::"OSNat_Hom"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" ) ")" ) where t "is" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) : (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set (Var "t")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ) "}" )))) ; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"OSFreeGen"::: "X" -> ($#m1_osafree :::"OSGeneratorSet"::: ) "of" (Set ($#k16_osafree :::"FreeOSA"::: ) "X") means :: OSAFREE:def 26 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k23_osafree :::"OSFreeGen"::: ) "(" (Set (Var "s")) "," "X" ")" ))); end; :: deftheorem defines :::"OSFreeGen"::: OSAFREE:def 26 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_osafree :::"OSGeneratorSet"::: ) "of" (Set ($#k16_osafree :::"FreeOSA"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k24_osafree :::"OSFreeGen"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k23_osafree :::"OSFreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ))) ")" )))); theorem :: OSAFREE:31 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k24_osafree :::"OSFreeGen"::: ) (Set (Var "X"))) "is" bbbadV2_RELAT_1()))) ; registrationlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); cluster (Set ($#k24_osafree :::"OSFreeGen"::: ) "X") -> bbbadV2_RELAT_1() ; end; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "R" be ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Const "X"))); let "t" be ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" )); func :::"OSClass"::: "(" "R" "," "t" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_osalg_4 :::"OSClass"::: ) "(" "R" "," (Set "(" ($#k10_osafree :::"LeastSort"::: ) "t" ")" ) ")" ) means :: OSAFREE:def 27 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool "t" ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k8_osalg_4 :::"OSClass"::: ) "(" "R" "," (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"OSClass"::: OSAFREE:def 27 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_osalg_4 :::"OSClass"::: ) "(" (Set (Var "R")) "," (Set "(" ($#k10_osafree :::"LeastSort"::: ) (Set (Var "t")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set (Var "R")) "," (Set (Var "t")) ")" )) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_osalg_4 :::"OSClass"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" )))) ")" )))))); theorem :: OSAFREE:32 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set (Var "R")) "," (Set (Var "t")) ")" )))))) ; theorem :: OSAFREE:33 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set "(" ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")) ")" ) "," (Set (Var "t")) ")" )) "iff" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" )))))) ; theorem :: OSAFREE:34 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set (Var "t2")) ($#r2_hidden :::"in"::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set (Var "R")) "," (Set (Var "t1")) ")" )) "iff" (Bool (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set (Var "R")) "," (Set (Var "t1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set (Var "R")) "," (Set (Var "t2")) ")" )) ")" ))))) ; theorem :: OSAFREE:35 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_osalg_4 :::"OSCongruence":::) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set (Var "R1")) ($#r2_pboole :::"c="::: ) (Set (Var "R2")))) "holds" (Bool (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set (Var "R1")) "," (Set (Var "t")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set (Var "R2")) "," (Set (Var "t")) ")" )))))) ; theorem :: OSAFREE:36 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set "(" ($#k15_osafree :::"LCongruence"::: ) (Set (Var "X")) ")" ) "," (Set (Var "t")) ")" )) "iff" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" )))))) ; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "A" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k22_osafree :::"PTVars"::: ) (Set (Const "X"))) "," (Set (Const "A")); let "t" be ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" ); assume (Bool (Set (Const "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Const "X")) ")" ))) ; func :::"pi"::: "(" "F" "," "A" "," "t" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) "A") means :: OSAFREE:def 28 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" "t" ($#k2_xtuple_0 :::"`2"::: ) ")" )))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) "t" ")" )))); end; :: deftheorem defines :::"pi"::: OSAFREE:def 28 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k22_osafree :::"PTVars"::: ) (Set (Var "X"))) "," (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k26_osafree :::"pi"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) "," (Set (Var "t")) ")" )) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "t")) ($#k2_xtuple_0 :::"`2"::: ) ")" )))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )))) ")" ))))))); theorem :: OSAFREE:37 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k22_osafree :::"PTVars"::: ) (Set (Var "X"))) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) (Bool "ex" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) "," (Set (Var "U1")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) "," (Set (Var "U1"))) & (Bool (Set (Var "h")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) & (Bool (Set (Set (Var "h")) ($#k1_msafree :::"||"::: ) (Set "(" ($#k22_osafree :::"PTVars"::: ) (Set (Var "X")) ")" )) ($#r8_pboole :::"="::: ) (Set (Var "f"))) ")" )))))) ; definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func :::"NHReverse"::: "(" "s" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k23_osafree :::"OSFreeGen"::: ) "(" "s" "," "X" ")" ")" ) "," (Set "(" ($#k21_osafree :::"PTVars"::: ) "(" "s" "," "X" ")" ")" ) means :: OSAFREE:def 29 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) "st" (Bool (Bool (Set (Set "(" (Set "(" ($#k18_osalg_4 :::"OSNat_Hom"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) "X" ")" ) ")" ")" ) ($#k1_msualg_3 :::"."::: ) "s" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k23_osafree :::"OSFreeGen"::: ) "(" "s" "," "X" ")" ))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k18_osalg_4 :::"OSNat_Hom"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) "X" ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) "X" ")" ) ")" ")" ) ($#k1_msualg_3 :::"."::: ) "s" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t"))))); end; :: deftheorem defines :::"NHReverse"::: OSAFREE:def 29 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k23_osafree :::"OSFreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k21_osafree :::"PTVars"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k27_osafree :::"NHReverse"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Set "(" (Set "(" ($#k18_osalg_4 :::"OSNat_Hom"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k23_osafree :::"OSFreeGen"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k18_osalg_4 :::"OSNat_Hom"::: ) "(" (Set "(" ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k15_osafree :::"LCongruence"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t"))))) ")" ))))); definitionlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"NHReverse"::: "X" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k24_osafree :::"OSFreeGen"::: ) "X") "," (Set ($#k22_osafree :::"PTVars"::: ) "X") means :: OSAFREE:def 30 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k27_osafree :::"NHReverse"::: ) "(" (Set (Var "s")) "," "X" ")" ))); end; :: deftheorem defines :::"NHReverse"::: OSAFREE:def 30 : (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k24_osafree :::"OSFreeGen"::: ) (Set (Var "X"))) "," (Set ($#k22_osafree :::"PTVars"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k28_osafree :::"NHReverse"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k27_osafree :::"NHReverse"::: ) "(" (Set (Var "s")) "," (Set (Var "X")) ")" ))) ")" )))); theorem :: OSAFREE:38 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k24_osafree :::"OSFreeGen"::: ) (Set (Var "X"))) "is" ($#v1_osafree :::"osfree"::: ) ))) ; theorem :: OSAFREE:39 (Bool "for" (Set (Var "S")) "being" ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k16_osafree :::"FreeOSA"::: ) (Set (Var "X"))) "is" ($#v2_osafree :::"osfree"::: ) ))) ; registrationlet "S" be ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v12_osalg_1 :::"order-sorted"::: ) ($#v13_osalg_1 :::"monotone"::: ) ($#v2_osafree :::"osfree"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; begin definitionlet "S" be ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"PTMin"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) ")" ) "," (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) ")" ) means :: OSAFREE:def 31 (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_osafree :::"pi"::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "ts"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_osafree :::"pi"::: ) "(" (Set "(" ($#k13_osafree :::"@"::: ) "(" "X" "," (Set (Var "nt")) ")" ")" ) "," (Set "(" it ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"PTMin"::: OSAFREE:def 31 : (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dtconstr :::"Terminals"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_osafree :::"pi"::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "ts")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "ts"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_osafree :::"pi"::: ) "(" (Set "(" ($#k13_osafree :::"@"::: ) "(" (Set (Var "X")) "," (Set (Var "nt")) ")" ")" ) "," (Set "(" (Set (Var "b3")) ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ) ")" ))) ")" ) ")" ) ")" )))); theorem :: OSAFREE:40 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set "(" ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")) ")" ) "," (Set (Var "t")) ")" )) & (Bool (Set ($#k10_osafree :::"LeastSort"::: ) (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k10_osafree :::"LeastSort"::: ) (Set (Var "t")))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "ts")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set ($#k9_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k1_dtconstr :::"roots"::: ) (Set (Var "ts")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ")" ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "ts"))))) "holds" (Bool "(" (Bool (Set ($#k11_osafree :::"LeastSorts"::: ) (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" )) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")))) & (Bool (Set ($#k9_osafree :::"OSSym"::: ) "(" (Set (Var "o")) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k14_trees_3 :::"roots"::: ) (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ))) & (Bool (Set ($#k9_osafree :::"OSSym"::: ) "(" (Set "(" ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_osafree :::"LeastSorts"::: ) (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ) ")" ) ")" ")" ) "," (Set (Var "X")) ")" ) ($#r1_lang1 :::"==>"::: ) (Set ($#k14_trees_3 :::"roots"::: ) (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ))) & (Bool (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_osafree :::"OSSym"::: ) "(" (Set "(" ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_osafree :::"LeastSorts"::: ) (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ) ")" ) ")" ")" ) "," (Set (Var "X")) ")" ")" ) ($#k4_trees_4 :::"-tree"::: ) (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k11_lang1 :::"*"::: ) (Set (Var "ts")) ")" ))) ")" )) ")" ) ")" )))) ; theorem :: OSAFREE:41 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "," (Set (Var "t1")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "st" (Bool (Bool (Set (Var "t1")) ($#r2_hidden :::"in"::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set "(" ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")) ")" ) "," (Set (Var "t")) ")" ))) "holds" (Bool (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))))))) ; theorem :: OSAFREE:42 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set (Var "t2")) ($#r2_hidden :::"in"::: ) (Set ($#k25_osafree :::"OSClass"::: ) "(" (Set "(" ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")) ")" ) "," (Set (Var "t1")) ")" )) "iff" (Bool (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")))) ")" )))) ; theorem :: OSAFREE:43 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t1"))))))) ; theorem :: OSAFREE:44 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#v2_msualg_4 :::"MSEquivalence-like"::: ) ($#v3_osalg_4 :::"monotone"::: ) ($#m1_osalg_4 :::"OrderSortedRelation"::: ) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set "(" (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k2_msualg_4 :::"."::: ) (Set "(" ($#k10_osafree :::"LeastSort"::: ) (Set (Var "t")) ")" ))))))) ; theorem :: OSAFREE:45 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#v2_msualg_4 :::"MSEquivalence-like"::: ) ($#v3_osalg_4 :::"monotone"::: ) ($#m1_osalg_4 :::"OrderSortedRelation"::: ) "of" (Set ($#k8_osafree :::"ParsedTermsOSA"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set (Var "R")))))) ; theorem :: OSAFREE:46 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k15_osafree :::"LCongruence"::: ) (Set (Var "X"))) ($#r8_pboole :::"="::: ) (Set ($#k20_osafree :::"PTCongruence"::: ) (Set (Var "X")))))) ; definitionlet "S" be ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); mode :::"MinTerm"::: "of" "S" "," "X" -> ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" )) means :: OSAFREE:def 32 (Bool (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) "X" ")" ) ($#k3_funct_2 :::"."::: ) it) ($#r1_hidden :::"="::: ) it); end; :: deftheorem defines :::"MinTerm"::: OSAFREE:def 32 : (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) (Set (Var "X")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_osafree :::"MinTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "X"))) "iff" (Bool (Set (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) ")" )))); definitionlet "S" be ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "S")); func :::"MinTerms"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set "(" ($#k2_osafree :::"DTConOSA"::: ) "X" ")" ) ")" ) equals :: OSAFREE:def 33 (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k29_osafree :::"PTMin"::: ) "X" ")" )); end; :: deftheorem defines :::"MinTerms"::: OSAFREE:def 33 : (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k30_osafree :::"MinTerms"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k29_osafree :::"PTMin"::: ) (Set (Var "X")) ")" ))))); theorem :: OSAFREE:47 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#v2_osalg_4 :::"locally_directed"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m2_osafree :::"MinTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k30_osafree :::"MinTerms"::: ) (Set (Var "X")))) ")" )))) ;