Quellcode-Bibliothek orthogonality.prf
Sprache: Lisp
(mem_testnil 3569253011"" (skeep) (("" (grind) nil nil )) nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" mem_test nil )nil mem_test nil )"finite_set[T]" seq2set "structures/" ))nil 3569226615"" (skeep)"" (expand subseq)"" (skeep)"" (inst -1 i)"" (expand member_seq)"" (expand finseq_appl)"" (skosimp)"" (typepred i!1)"" (expand rest (-1 -2))"" (expand * ^ min )"" (expand empty_seq -1)"" (lift-if)"" (assert )"" (prop) (("" (inst 7 "1+i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" mem_test nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )nil mem_test nil )nil finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )NOT const-decl "[bool -> bool]" booleans nil )"finseq" seq_extras "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posint" nil )"finseq" finite_sequences nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"finseq" finite_sequences nil )"bool" mem_test nil ))nil 3569231569"" (skeep)"" (split)"1" (flatten)"1" (expand o)"1" (expand seq2set)"1" (expand finseq_appl)"1" (skosimp)"1" (lift-if)"1" (prop)"1" (inst 1 kk!1) nil nil )"2" (inst 3 "kk!1 - seq1`length" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand o)"2" (expand seq2set)"2" (expand finseq_appl)"2" (split)"1" (skosimp)"1" (inst 1 kk!1)"1" (lift-if) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil )"2" (skosimp)"2" (inst 1 "kk!1+seq1`length" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"finseq" finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"below(seq1`length + seq2`length)" mem_testnil )"finseq[T]" mem_test nil )"finseq[T]" mem_test nil )"(strict_total_order?[real])" real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )nil mem_test nil )nil finite_sequences nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"finite_set[T]" seq2set "structures/" )"below(length(seq1))" mem_test nil )"nonneg_int" nil ))nil 3575042025 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil nat_types nil )"bool" reals nil ))nil ))nil 3575042025 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil nat_types nil )"bool" reals nil ))nil ))nil 3575042025 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil ))nil ))nil 3575042025 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil ))nil ))nil 3575042025 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil ))nil ))nil 3575042028"" (induct n)"1" (skeep)"1" (inst 1 empty_seq)"1" (expand empty_seq 1 1) (("1" (skeep) nil nil )) nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (inst -1 P "rest(seq1)" "rest(seq2)" )"2" (prop)"1" (inst -4 0)"1" (skosimp*)"1" (inst 1 "add_first(x!1, seq!1)" )"1" (expand * add_first insert? finseq_appl)"1" (assert )"1" (skeep)"1" (lift-if)"1" (case "i=0" )"1" (assert ) nil nil )"2" (assert )"2" "2" expand rest -2)"2" expand * ^ min empty_seq)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1)) (("2" (grind) nil nil )) nil )"3" (hide-all-but (-2 1)) (("3" (grind) nil nil )) nil )"4" (hide 2)"4" (skeep)"4" (typepred i)"4" (expand * rest ^ min empty_seq)"4" (assert ) (("4" (inst -4 1+i) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (skeep) (("3" (skeep) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep)"4" (skeep) (("4" (skeep) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"5" (hide 2)"5" (skeep) (("5" (skeep) (("5" (assert ) nil nil )) nil )) nil ))nil )"6" (hide 2)"6" (skeep) (("6" (skeep) (("6" (assert ) nil nil )) nil )) nil ))nil )"7" (hide 2) (("7" (skeep) (("7" (assert ) nil nil )) nil )) nil )"8" (hide 2) (("8" (skeep) (("8" (assert ) nil nil )) nil )) nil ))nil )"finseq" seq_extras "structures/" )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"finseq" seq_extras "structures/" )"posint" nil )"int" integers nil )"finseq" finite_sequences nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )"finseq" finite_sequences nil )nil naturalnumbers nil )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil mem_test nil )nil finite_sequences nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" reals nil ))nil 3575131546 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil ))nil ))nil 3575131579"" (induct n)"1" (skeep)"1" (inst 1 empty_seq)"1" (expand empty_seq 1 1) (("1" (skeep) nil nil )) nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (inst -1 P1)"2" (prop)"1" (skosimp)"1" (inst -3 j)"1" (skosimp)"1" (inst 1 "add_last(seq!1, x!1)" )"1" (expand * add_last insert? finseq_appl)"1" (assert )"1" (skeep)"1" (lift-if)"1" (prop)"1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep) (("2" (inst -1 i) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep) (("3" (skeep) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"below[1 + j]" mem_test nil )"nat" mem_test nil )NOT const-decl "[bool -> bool]" booleans nil )"finseq" seq_extras "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"finseq" finite_sequences nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil mem_test nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil nat_types nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil ))nil 3581385367"" (rewrite "var_countable" ) nil nil )nil orthogonality nil )) nil ))nil 3581173294"" (skosimp*)"" (hide-all-but 3)"" (typepred "p!1" ) (("" (rewrite "ext_preserv_pos" ) nil nil ))nil ))nil ))nil )nil substitution nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil orthogonality nil )nil orthogonality nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" orthogonality nil )nil term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil positions nil )"positions" positions nil )"bool" rewrite_rules nil )nil rewrite_rules nil )"term" rewrite_rules nil )set type-eq-decl nil sets nil ) (member const-decl "bool" sets nil )nil positions nil ))nil ))nil 3581173294"" (skosimp*)"" (hide-all-but (-1 3))"" (rewrite "ext_preserv_pos" ) nil nil )) nil ))nil )"[symbol -> nat]" orthogonality nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil orthogonality nil )nil orthogonality nil )nil substitution nil )"bool" substitution nil )"set[term]" variables_term nil )"bool" sets nil ) (set type-eq-decl nil sets nil )"term" rewrite_rules nil )nil rewrite_rules nil )"bool" rewrite_rules nil )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil substitution nil ))nil ))nil 3581173357"" (skosimp*)"" (lemma "CP_lemma_aux1a" )"" (inst?)"" (assert )"" (skosimp*)"" case "ext(union_subs((restriction(sg1!1)(Vars(lhs(e1!1))), restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))))(subtermOF(lhs(e1!1), p!1)) = ext(union_subs((restriction(sg1!1)(Vars(lhs(e1!1))), restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))))(ext(rho!1)(lhs(e2!1)))" )"1" (lemma "unification" )"1" "subtermOF(lhs(e1!1), p!1)" "ext(rho!1)(lhs(e2!1))" )"1" (hide 2)"1" (prop)"1" (skosimp*)"1" (copy -1)"1" (expand "mgu" -1)"1" (flatten)"1" "1" "union_subs(restriction(sg1!1)(Vars(lhs(e1!1))), restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" )"1" expand "member" -1)"1" expand "U" -1)"1" expand "unifier" -1)"1" assert )"1" expand "<=" )"1" "1" "ext(theta!1)(rhs(e1!1))" "replaceTerm(ext(theta!1)(lhs(e1!1)), ext(theta!1)(ext(rho!1)(rhs(e2!1))),p!1)" "tau!1" )"1" "ext_o" )"1" "tau!1" "theta!1" )"1" "1" "1" "1" expand "ntCP?" )"1" "theta!1" "rho!1" "e1!1" "e2!1" "p!1" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "rhs(e1!1)" )"2" expand "o" )"2" replace "2" "2" replace "2" "2" "restriction_union" )"2" "restriction(sg1!1)(Vars(lhs(e1!1)))" "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "rhs(e1!1)" )"1" "dom_restriction" )"1" "1" "Vars(lhs(e1!1))" "sg1!1" )"1" "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1" )"1" "IUnion_extra[(V)].disjoint_subset" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" )"1" assert )"1" "1" replace "1" "restriction_term" )"1" "1" "1" assert )nil nil )"2" "2" "e1!1" )"2" expand "rewrite_rule?" )"2" expand *"lhs" "rhs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "IUnion_extra[(V)].disjoint_subset" )"2" "Vars(rhs(e1!1))" "Vars(rhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" )"2" "1" "1" expand *"subset?" "member" )"1" nil nil ))nil ))nil )"2" "2" "IUnion_extra[(V)].disjoint_subset" )"2" "Vars(rhs(e1!1))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(lhs(e2!1)))" "Vars(ext(rho!1)(lhs(e2!1)))" )"2" "1" "1" "e1!1" )"1" expand *"rewrite_rule?" "lhs" "rhs" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "restriction_Subs" )nil nil )"3" rewrite "restriction_Subs" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "ext_replace_ext" )"3" "3" "1" "1" "1" "ext(rho!1)(rhs(e2!1))" )"1" "lhs(e1!1)" )"1" expand "o" )"1" replace "1" replace "1" replace "1" "1" "restriction_union" )"1" "1" "restriction(sg1!1)(Vars(lhs(e1!1)))" "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "lhs(e1!1)" )"1" "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "restriction(sg1!1)(Vars(lhs(e1!1)))" "ext(rho!1)(rhs(e2!1))" )"1" "dom_restriction" )"1" "1" "Vars(lhs(e1!1))" "sg1!1" )"1" "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1" )"1" "IUnion_extra[(V)].disjoint_subset" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" )"1" assert )"1" "IUnion_extra[(V)].disjoint_commute" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" )"1" assert )"1" "1" rewrite "union_commute" )"1" "1" "1" "restriction_term" )"1" "1" "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1" "ext(rho!1)(rhs(e2!1))" )"1" "Vars(lhs(e1!1))" "sg1!1" "lhs(e1!1)" )"1" "1" replace "1" replace "1" rewrite "ext_o" )"1" expand "o" )"1" "ext(alpha!1)(ext(rho!1)(rhs(e2!1))) = ext(sg2!1)(rhs(e2!1))" )"1" "1" "1" "ext_o" )"1" "alpha!1" "rho!1" )"1" "1" "1" "1" "lhs(e2!1)" )"1" "rhs(e2!1)" )"1" expand "o" )"1" replace "1" replace "1" "1" "same_substitution" )"1" "comp(alpha!1, rho!1)" "sg2!1" "lhs(e2!1)" )"1" assert )"1" "same_term" )"1" "comp(alpha!1, rho!1)" "sg2!1" "rhs(e2!1)" )"1" "1" "1" "1" "x!1" )"1" assert )"1" "1" "e2!1" )"1" "1" expand "rewrite_rule?" )"1" "1" expand *"subset?" "rhs" "lhs" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil )"3" "3" "e2!1" )"3" expand "rewrite_rule?" )"3" "3" "rename_preserv_inclusion" )"3" expand *"rhs" "lhs" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand *"subset?" "member" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "IUnion_extra[(V)].disjoint_subset" )"2" case "disjoint?(Vars(lhs(e1!1)), Vars(ext(rho!1)(rhs(e2!1))))" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(rhs(e2!1)))" "Vars(ext(rho!1)(rhs(e2!1)))" )"1" "1" "IUnion_extra[(V)].disjoint_commute" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(ext(rho!1)(rhs(e2!1)))" )"1" assert )nil nil ))nil ))nil )"2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "e2!1" )"2" expand "rewrite_rule?" )"2" "2" expand *"lhs" "rhs" )"2" "rename_preserv_inclusion" )"2" "rho!1" "e2!1`1" "e2!1`2" )"2" assert )"2" "Vars(e1!1`1)" "Vars(e1!1`1)" "Vars(ext(rho!1)(e2!1`2))" "Vars(ext(rho!1)(e2!1`1))" )"2" "2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "IUnion_extra[(V)].disjoint_subset" )"3" "Vars(lhs(e1!1))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" )"3" "3" "3" expand *"subset?" "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "IUnion_extra[(V)].disjoint_subset" )"4" case "disjoint?(Vars(ext(rho!1)(rhs(e2!1))), Vars(lhs(e1!1)))" )"1" "Vars(ext(rho!1)(rhs(e2!1)))" "Vars(ext(rho!1)(rhs(e2!1)))" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" )"1" "1" "1" expand *"subset?" "member" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "e2!1" )"2" expand "rewrite_rule?" )"2" "2" "rename_preserv_inclusion" )"2" "rho!1" "e2!1`1" "e2!1`2" )"2" assert )"2" "Vars(e1!1`1)" "Vars(e1!1`1)" "Vars(ext(rho!1)(e2!1`2))" "Vars(ext(rho!1)(e2!1`1))" )"2" "1" expand *"rhs" "lhs" )"1" "1" "IUnion_extra[(V)].disjoint_commute" )"1" "Vars(e1!1`1)" "Vars(ext(rho!1)(e2!1`2))" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil )"3" expand *"rhs" "lhs" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "restriction_Subs" )nil nil ))nil )"3" "3" rewrite "restriction_Subs" )nil nil ))nil ))nil )"2" "2" rewrite "restriction_Subs" )nil nil ))nil )"3" "3" rewrite "restriction_Subs" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "restriction_Subs" )nil nil ))nil )"3" "3" rewrite "restriction_Subs" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (expand "unifiable" )"2" "union_subs((restriction(sg1!1)(Vars(lhs(e1!1))), restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))))" )"1" (expand "unifier" )"1" (propax) nil nil )) nil )"2" (hide-all-but 1)"2" rewrite "restriction_Subs" )nil nil ))nil )"3" (hide-all-but 1)"3" rewrite "restriction_Subs" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3 4)"2" (lemma "restriction_union" )"2" "restriction(sg1!1)(Vars(lhs(e1!1)))" "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "subtermOF(lhs(e1!1), p!1)" )"1" (lemma "dom_restriction" )"1" (inst -1 "Vars(lhs(e1!1))" "sg1!1" )"1" "IUnion_extra[(V)].disjoint_subset" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" )"1" (lemma "dom_restriction" )"1" "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1" )"1" assert )"1" "IUnion_extra[(V)].disjoint_subset" )"1" "Vars(lhs(e1!1))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" )"1" "1" "1" "restriction_union" )"1" "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "restriction(sg1!1)(Vars(lhs(e1!1)))" "ext(rho!1)(lhs(e2!1))" )"1" "IUnion_extra[(V)].disjoint_commute" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" )"1" assert )"1" "IUnion_extra[(V)].disjoint_subset" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(lhs(e2!1)))" "Vars(ext(rho!1)(lhs(e2!1)))" )"1" assert )"1" "1" rewrite "union_commute" )"1" "1" "restriction_term" )"1" "1" "1" replace "1" "restriction_term" )"1" "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1" "ext(rho!1)(lhs(e2!1))" )"1" "1" replace "1" rewrite "ext_o" )"1" expand "o" )"1" nil nil ))nil ))nil ))nil )"2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "vars_subterm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "IUnion_extra[(V)].disjoint_commute" )nil nil ))nil )"3" "3" expand *"subset?" "member" )"3" nil nil ))nil ))nil )"4" "4" "IUnion_extra[(V)].disjoint_subset" )"4" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(lhs(e2!1)))" "Vars(ext(rho!1)(lhs(e2!1)))" )"4" assert )"4" "1" "1" "IUnion_extra[(V)].disjoint_commute" )"1" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(ext(rho!1)(lhs(e2!1)))" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "restriction_Subs" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "vars_subterm" )"2" "2" assert )"2" "IUnion_extra[(V)].disjoint_subset" )"2" "Vars(subtermOF(lhs(e1!1), p!1))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" )"2" "2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand *"subset?" "member" )"3" (skeep) nil nil ))nil ))nil )"4" "4" "IUnion_extra[(V)].disjoint_subset" )"4" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" "Vars(lhs(e1!1))" "Vars(lhs(e1!1))" )"4" "IUnion_extra[(V)].disjoint_commute" )"4" "4" assert )"4" "1" "1" "vars_subterm" )"1" "1" assert )"1" "IUnion_extra[(V)].disjoint_subset" )"1" "Vars(subtermOF(lhs(e1!1), p!1))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" )"1" "1" "1" expand *"subset?" "member" )"1" nil nil ))nil ))nil )"2" "2" "IUnion_extra[(V)].disjoint_commute" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"subset?" "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "restriction_Subs" ) nil nil )) nil )"3" (hide-all-but 1)"3" (rewrite "restriction_Subs" ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (rewrite "union_is_sub" )"1" (hide 2)"1" (rewrite "restriction_Subs" ) nil nil )) nil )"2" (hide 2)"2" (rewrite "restriction_Subs" ) nil nil )) nil ))nil ))nil )"4" (hide-all-but (-1 1))"4" (expand "disjoint_D?" )"4" (lemma "dom_restriction" )"4" (copy -1)"4" (inst -1 "Vars(lhs(e1!1))" "sg1!1" )"4" "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1" )"4" "IUnion_extra[(V)].disjoint_subset" )"4" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but 1)"5" (rewrite "restriction_Subs" ) nil nil )) nil )"6" (hide-all-but 1)"6" (rewrite "restriction_Subs" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" orthogonality nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil orthogonality nil )nil orthogonality nil )nil critical_pairs nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )nil substitution nil )"bool" substitution nil )"term" rewrite_rules nil )"set[(V)]" subterm nil )"term" substitution nil )"term" substitution nil )nil substitution nil )"bool" substitution nil )ext def-decl "term" substitution nil )"[T, T -> boolean]" equalities nil )"Sub[variable, symbol, arity]" nil )"set[rewrite_rule[variable, symbol, arity]]" nil )"{e1 | member(e1, E!1)}" orthogonality nil )"Sub[variable, symbol, arity]" nil )"Ren[variable, symbol, arity]" nil )"{e2 | member(e2, E!1)}" orthogonality nil )"set[Sub]" unification nil )nil substitution nil )"T3" function_props nil )"term" substitution nil )nil substitution nil )nil substitution nil )nil substitution nil )nil substitution nil )nil substitution nil )"bool" sets nil )nil IUnion_extra nil )nil substitution nil )nil substitution nil )nil substitution nil )nil substitution nil )nil IUnion_extra nil )"(partial_order?[set[T]])" nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil substitution nil )"set[(V)]" substitution nil )"bool" orthogonality nil )"term" rewrite_rules nil )"term" replacement nil )"position[variable, symbol, arity]" nil )"Sub[variable, symbol, arity]" nil )"bool" unification nil )"bool" unification nil )"bool" unification nil )"bool" unification nil )nil unification nil )nil subterm nil )nil substitution nil )"bool" sets nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil rewrite_rules nil )"bool" rewrite_rules nil )nil substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil ))nil 3434983472"" (skosimp)"" (lemma Pos_var_is_finite)"" (inst -1 t!1 x!1) (("" (assert ) nil nil )) nil )) nil ))nil )"[symbol -> nat]" orthogonality nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil orthogonality nil )nil orthogonality nil )nil subterm nil )"set[(V)]" subterm nil )"bool" sets nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil ))nil ))nil 3460213554"" (skosimp)"" (lemma Pos_var_is_finite)"" (inst -1 t!1 x!1) (("" (assert ) nil nil )) nil )) nil ))nil )"[symbol -> nat]" orthogonality nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil orthogonality nil )nil orthogonality nil )nil subterm nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil ))nil ))nil 3460212656"" (skeep)"" (lemma finite_sets[position].card_one)"" (inst -1 "Pos_var(t, x)" )"" (lemma finite_sets[position].card_def)"" (inst -1 "Pos_var(t, x)" )"" (replace -1 -3 rl)"" (assert )"" (skosimp)"" (inst 1 x!1)"" (expand singleton)"" (decompose-equality)"" (inst -1 x!1)"" (expand Pos_var -1)"" (expand extend) (("" (prop) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"[symbol -> nat]" orthogonality nil )nil orthogonality nil )nil orthogonality nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )nil finite_sets nil )nil finite_sets nil )"(singleton?)" sets nil )"R" extend nil )"[T, T -> boolean]" equalities nil )"positions" subterm nil )nil positions nil )"set[term]" variables_term nil )nil term_adt nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil ))nil 3460128485"" (skeep)"" (prop)"1" (replace -1 1) (("1" (propax) nil nil )) nil )"2" (lemma subterm_of_replace)"2" (copy -1)"2" (inst -1 p s t1)"2" (inst -2 p s t2) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil replacement nil )nil orthogonality nil )nil orthogonality nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" orthogonality nil ))nil 3466433636"" (skosimp)"" (lemma seq_first_rest_1[posnat])"" (inst -1 p!1)"" (assert )"" (lemma pos_ax)"" (inst -1 "#(first(p!1))" "rest(p!1)" s!1)"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil seq_extras "structures/" )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil term_adt nil )nil positions nil )nil positions nil )"[symbol -> nat]" orthogonality nil )nil orthogonality nil )nil orthogonality nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil ))nil ))nil 3466433636"" (skosimp)"" (lemma Pos_var_is_finite)"" (inst -1 "subtermOF(s!1, #(first(p!1)))" "x!1" )"" (assert ) nil nil )) nil ))nil ))nil )"[symbol -> nat]" orthogonality nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil orthogonality nil )nil orthogonality nil )nil subterm nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )nil finite_sequences nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil ))nil ))nil 3467717493"" (skeep)"" (case "card(Pos_var(subtermOF(s, #(first(p))), x)) >= 2" )"1" (lemma finite_sets[position].card_2_has_2)"1" (inst -1 "Pos_var(subtermOF(s, #(first(p))), x)" )"1" (assert )"1" (skosimp)"1" (case "member( #(first(p)) o x!1 , Pos_var(s,x))" )"1" case "member( #(first(p)) o y!1 , Pos_var(s,x))" )"1" (expand member)"1" (hide -3 -4 -5 3)"1" (expand Pos_var (-1 -2))"1" (expand extend)"1" (prop)"1" (rewrite card_one)"1" "1" expand * Pos_var extend)"1" "1" "1" "add_first(first(p), x!1)" )"1" "add_first(first(p), y!1)" )"1" "1" case "add_first(first(p), x!1) = #(first(p)) o x!1 & add_first(first(p), y!1) = #(first(p)) o y!1" )"1" "1" replace -1 -3)"1" replace -2 -4)"1" assert )"1" replace "1" replace "1" expand "1" replace "1" "1" "1" "first(p)" "first(p)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand add_first 1)"1" expand insert?)"1" "1" expand "1" expand o)"1" "1" nil nil )"2" case "#(first(p))`length = 1" )"1" replace "1" assert )"1" "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil )"5" "5" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "#(first(p))`length = 1" )"1" expand *"1" expand "1" expand o)"1" "1" assert )nil nil )"2" "1" "1" "1" replace "1" assert )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand member)"2" (hide -1 -2)"2" (expand Pos_var (-1 1))"2" (expand extend)"2" (prop)"1" (lemma pos_subterm)"1" "#(first(p))" y!1 s)"1" "1" "#(first(p))" y!1 s)"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (lemma pos_o_term)"2" "#(first(p))" y!1 s)"2" assert )"2" expand positionsOF (-5 1))"2" "2" "1" expand only_empty_seq -2)"1" rewrite empty_0)nil nil ))nil )"2" "2" expand only_empty_seq)"2" rewrite empty_0)nil nil ))nil ))nil )"3" expand *"3" "1" rewrite empty_0)nil nil )"2" "2" "2" "2" "1" "1" expand "1" "1" "1" "1" expand "1" nil nil ))nil ))nil )"2" "2" expand "2" nil nil ))nil ))nil )"3" expand *nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" replace "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 -7 2 4)"2" (expand Pos_var (-1 1))"2" (expand * extend member)"2" (prop)"1" (lemma pos_subterm)"1" (inst -1 "#(first(p))" x!1 s)"1" (assert ) nil nil )) nil ))nil )"2" (lemma pos_o_term)"2" (inst -1 "#(first(p))" x!1 s)"2" (assert )"2" "2" expand positionsOF (-4 1))"2" "2" "1" "1" expand only_empty_seq)"1" rewrite empty_0)nil nil ))nil ))nil )"2" "2" expand only_empty_seq)"2" rewrite empty_0)nil nil ))nil ))nil )"3" expand *"3" "1" rewrite empty_0)nil nil )"2" "2" "2" "2" "1" "1" expand "1" "1" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil )"3" expand *nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace -3 1)"2" replace "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "card(Pos_var(subtermOF(s, #(first(p))), x)) = 0" )"1" (rewrite card_empty?)"1" (expand empty?)"1" (inst -1 "rest(p)" )"1" (expand member)"1" (hide -4 2 4)"1" (expand * Pos_var extend)"1" (prop)"1" (lemma pos_subterm)"1" (inst -1 "#(first(p))" "rest(p)" s)"1" (prop)"1" (lemma seq_first_rest_1[posnat])"1" "1" (assert ) nil nil ))nil ))nil )"2" (lemma seq_first_rest_1[posnat])"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma pos_subterm_ax)"2" (inst -1 "#(first(p))" "rest(p)" s)"2" (assert )"2" (lemma seq_first_rest_1[posnat])"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )nil finite_sequences nil )"term" subterm nil )nil positions nil )"positions" positions nil )"positions" subterm nil )nil positions nil )"set[term]" variables_term nil )nil term_adt nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil positions nil )"[symbol -> nat]" orthogonality nil )nil orthogonality nil )nil orthogonality nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"R" extend nil )nil finite_sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil seq_extras "structures/" )"position[variable, symbol, arity]" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"position[variable, symbol, arity]" nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"position[variable, symbol, arity]" nil )"int" integers nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"non_empty_finite_set[position]" orthogonality nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" booleans nil )"bool" sets nil )"(singleton?)" sets nil )"positions" positions nil )"set[T]" indexed_sets nil )"set" sets nil )"finseq" finite_sequences nil )"bool" reals nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil IUnion_extra nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"positions" positions nil )nil seq_extras "structures/" )nil subterm nil )nil subterm nil )"finseq" finite_sequences nil )"bool" sets nil )"(total_order?[real])" nil )nil finite_sets nil )nil finite_sets nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )nil subterm nil )"bool" sets nil ))nil 3481280713"" (skosimp)"" (hide 1)"" (typepred x!1)"" (expand * V ext ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )ext def-decl "term" substitution nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil orthogonality nil )nil orthogonality nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" orthogonality nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil ))nil ))nil 3481280713"" (skosimp)"" (lemma SigmaP_Subs)"" (inst -1 p2!1 sigma!1 t!1 x!1)"" (assert )"" (typepred x!1)"" (expand * V ext ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" orthogonality nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil orthogonality nil )nil orthogonality nil )nil substitution nil )ext def-decl "term" substitution nil )NOT const-decl "[bool -> bool]" booleans nil )nil substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3481280714"" (induct s)"1" (skeep)"1" (skeep)"1" (expand SigmaP)"1" (case "x = vars(vars1_var)" )"1" (name-replace "z" "vars(vars1_var)" )"1" (hide 2)"1" (replace -1 1)"1" (expand member)"1" (expand Vars)"1" (inst 1 empty_seq)"1" (grind) nil nil )"2" (hide -) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name-replace "z" "vars(vars1_var)" )"2" (expand ext 3 2)"2" (assert )"2" (expand ext 3) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (expand ext 2)"2" (assert )"2" (lift-if)"2" (case "length(app2_var) = 0" )"1" (assert ) nil nil )"2" (split)"1" (propax) nil nil )"2" (assert )"2" (decompose-equality)"1" (decompose-equality)"1" (decompose-equality)"1" (inst -1 "x!1" )"1" (inst -1 "p2" "sigma" "t" "x" )"1" assert )"1" expand finseq_appl)"1" "1" "1" expand * member Vars)"1" "1" " add_first(x!1 + 1, p!1)" )"1" expand subtermOF 1)"1" "1" "1" "1" expand "1" expand "1" assert )nil nil ))nil ))nil ))nil )"2" expand "2" rewrite "2" rewrite "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand positionsOF)"2" expand union)"2" "2" "2" expand member)"2" expand IUnion)"2" "x!1 + 1" )"2" expand "2" expand "2" "2" "2" expand "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (lemma SigmaP_Subs)"2" "2" assert )"2" "2" expand V)"2" expand ext -3)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (hide-all-but (-2 1))"3" "3" expand V)"3" expand ext -2)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (lemma SigmaP_Subs)"2" (inst -1 p2 sigma t x)"2" assert )"2" "2" "2" expand V)"2" expand ext -2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (lemma SigmaP_Subs)"3" (inst -1 p2 sigma t x)"3" assert )"3" "3" "3" expand V)"3" expand ext -2)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (lemma SigmaP_Subs)"2" (inst -1 p2 sigma t x)"2" (assert )"2" "2" "2" expand V)"2" expand ext -2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (hide-all-but (-2 1))"3" (typepred x)"3" (expand V)"3" expand ext -2)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (lemma SigmaP_Subs)"3" (inst -1 p2 sigma t x)"3" (assert )"3" (hide-all-but (-1 1))"3" (typepred x)"3" (expand V)"3" (expand ext -2) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep)"4" (hide 1)"4" (typepred x)"4" (expand V)"4" (expand ext -2) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )"symbol" orthogonality nil )"{args: finite_sequence[term[variable, symbol, arity]] | " orthogonality nil) "Sub[variable, symbol, arity]" nil )"(V)" orthogonality nil )"position[variable, symbol, arity]" nil )"term[variable, symbol, arity]" orthogonalitynil )"[below[length(fs)] -> T]" finite_sequencesnil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) nil term_adt nil )"[term -> boolean]" term_adt nil )"(total_order?[real])" nil )nil IUnion_extra nil )"bool" reals nil )"positions" positions nil )"set[T]" indexed_sets nil )"set" sets nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"int" integers nil )nil seq_extras "structures/" )"positions?[variable, symbol, arity](app2_var`seq(x!1))" nil )"below[app2_var`length]" orthogonality nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"finseq" seq_extras "structures/" )"posint" nil )nil substitution nil )nil finite_sequences nil )"positions" positions nil )"posint" nil )"term" subterm nil )"finseq" finite_sequences nil )nil finite_sequences nil )"(vars?)" orthogonality nil )"[variable -> (vars?)]" term_adt nil )"[term -> boolean]" term_adt nil )nil term_adt nil )nil orthogonality nil )nil orthogonality nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" orthogonality nil )"[T, T -> boolean]" equalities nil )nil positions nil )"term" substitution nil )nil term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"set[(V)]" subterm nil )nil positions nil )"positions" positions nil )ext def-decl "term" substitution nil ))nil 3452963667"" (skosimp) (("" (expand ext -3) (("" (assert ) nil nil )) nil ))nil )ext def-decl "term" substitution nil )) nil ))nil 3452963667"" (skosimp)"" (lemma SigmaP_Subs)"" (inst -1 p2!1 sigma!1 t!1 x!1)"" (expand ext -4) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[symbol -> nat]" orthogonality nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil orthogonality nil )nil orthogonality nil )nil substitution nil )ext def-decl "term" substitution nil )nil substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3452963667"" (skosimp*)"" (assert )"" (lemma "subterm_ext_commute" )"" (inst -1 "p1!1" "s!1" "sigma!1" )"" (assert )"" (replace -3 -1 rl)"" (replace -1 -4 rl)"" (rewrite pos_o_term)"" (lemma positions_of_ext)"" (inst -1 sigma!1 s!1)"" (decompose-equality -1)"" (inst -1 p1!1)"" (iff)"" (flatten)"" "" expand * union member)"" "" rewrite seq_o_empty)"" assert )"" "" expand *"" "" assert )"" "" expand *nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution nil )nil subterm nil )ext def-decl "term" substitution nil )"bool" sets nil )nil seq_extras "structures/" )"positions" positions nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )nil finite_sequences nil )"term" subterm nil )nil positions nil )"[term -> boolean]" term_adt nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set" sets nil )"positions" positions nil )nil positions nil )"[T, T -> boolean]" equalities nil )nil substitution nil )nil substitution nil )nil orthogonality nil )nil orthogonality nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" orthogonality nil ))nil ))nil 3459620652"" (lemma finite_sets[position].card_def)"" (lemma finite_sets[position].card_one)"" (expand singleton)"" (induct s)"1" (skeep)"1" (skeep)"1" (case "vars(vars1_var) = x" )"1" (name-replace "z" "vars(vars1_var)" )"1" (replace -1)"1" (expand ext 1 1)"1" (lift-if)"1" (assert )"1" (expand SigmaP)"1" (expand positionsOF -3)"1" expand only_empty_seq)"1" replace -3 1)"1" rewrite empty_o_seq)"1" expand ext 1)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name-replace "z" "vars(vars1_var)" )"2" (hide 2)"2" (expand positionsOF -2)"2" (assert )"2" (expand only_empty_seq)"2" (replace -2 -4)"2" (expand subtermOF -4)"2" rewrite empty_0)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (name-replace "sym" "app1_var" )"2" (expand ext 1 1)"2" (lift-if)"2" (assert )"2" (case "length(app2_var) = 0" )"1" (hide-all-but (-1 -3 -4 -6 1))"1" (expand positionsOF)"1" (assert )"1" expand only_empty_seq)"1" replace -3 -4)"1" expand subtermOF)"1" rewrite empty_0)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand finseq_appl 2)"2" (expand replaceTerm 2)"2" "2" case "length(p1 o p2) = 0" )"1" "1" rewrite empty_0)"1" "1" "1" assert )"1" "1" "1" rewrite empty_0)"1" replace -1 -4)"1" "1" expand "1" assert )"1" "1" assert )"1" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "1" "1" (grind) nil nil ))nil )"2" expand finseq_appl)"2" expand ext 1 2)"2" expand finseq_appl)"2" expand ext 1 3)"2" expand finseq_appl)"2" expand replace 1)"2" "1" "1" expand "1" case "x!1 = first(p1 o p2) - 1" )"1" assert )"1" "1" "rest(p1)" "1" assert )"1" "1" replace "1" assert )"1" rewrite "1" "1" "1" rewrite "1" expand "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "app(sym, app2_var)" )"2" assert )"2" "1" replace "1" expand "1" rewrite "1" "1" "1" rewrite "1" expand "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "3" "3" "1" "1" expand "1" assert )nil nil ))nil ))nil )"2" expand "2" replace "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" case "length(p1) /= 0" )"1" "1" "1" "app(sym, app2_var)" "1" assert )"1" "1" "Pos_var(app(sym, app2_var), x)" )"1" "Pos_var(app2_var`seq(x!1), x)" )"1" replace "1" replace "1" "1" assert )"1" rewrite "1" expand "1" assert )"1" "1" assert )"1" case "length( #(first(p1))) /= 0" )"1" assert )"1" expand *"1" expand "1" expand *"1" assert )"1" case " length( #(first(p1))) = 1" )"1" expand "1" "1" expand "1" expand *min "1" assert )"1" expand "#" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" case "member(x, Vars(app2_var`seq(x!1)))" )"1" expand "1" "Pos_var(app(sym, app2_var), x)" )"1" replace "1" "1" rewrite "1" "1" case "length(p1) = 0" )"1" expand "1" assert )nil nil ))nil )"2" expand "2" "2" "2" case "EXISTS p: positionsOF(app(sym, app2_var))(p) & p /= p1 & subtermOF(app(sym, app2_var), p) = x" )"1" "1" "1" "1" case "Pos_var(app(sym, app2_var), x)(p1) & Pos_var(app(sym, app2_var), x)(p)" )"1" "1" assert )nil nil ))nil )"2" "1" expand "1" expand "1" nil nil ))nil ))nil )"2" expand "2" expand "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "2" "2" expand "2" assert )"2" expand "2" "add_first(x!1 + 1, p!1)" )"2" "1" expand "1" expand *"1" "1" "1 + x!1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "2" "2" "2" assert )"2" replace "2" "2" "2" "rest(p1)" "1 + x!1" "first(p1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "3" "3" "1" "1" expand *"1" assert )nil nil ))nil ))nil )"2" expand "2" "2" "1 + x!1" )"2" "2" "2" "1 + x!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "2" "2" "2" "app2_var`seq(x!1)" "2" assert )"2" expand "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "app(sym, app2_var)" "2" assert )"2" "2" "2" "app(sym, app2_var)" "2" assert )"2" replace "2" "2" "p1 o p2" "ext(sigma)(app(sym, app2_var))" )"2" "1" "1" expand "1" case "args(ext(sigma)(app(sym, app2_var)))`seq(first(p1 o p2) - 1) = ext(sigma)(app2_var`seq(first(o(p1, p2)) - 1))" )"1" replace "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "ext(sigma)(app(sym, app2_var))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" case "length(p1) = 0" )"1" expand "1" assert )nil nil ))nil )"2" rewrite "2" expand *"2" rewrite "2" assert )"2" "2" expand "2" "2" expand "2" expand "2" "2" "2" "1" expand "1" expand "1" expand "1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" rewrite "4" expand ext "4" nil nil ))nil ))nil ))nil )"5" "5" expand ext -4)"5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand ext -4)"3" rewrite SigmaP_Subs)nil nil ))nil ))nil )"4" "4" expand ext -4)"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (lemma ext_preserv_pos)"3" (inst -1 p1 s sigma)"3" (assert )"3" (hide 2)"3" (replace -5 -4)"3" (lemma subterm_ext_commute)"3" (inst -1 p1 s sigma)"3" (assert )"3" (replace -1 -5 rl)"3" "3" "ext(sigma)(s)" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skeep)"4" (expand ext -3)"4" (assert ) (("4" (rewrite SigmaP_Subs) nil nil ))nil ))nil ))nil )"5" (skeep)"5" (expand ext -3) (("5" (assert ) nil nil )) nil )) nil )"6" (skeep)"6" (hide-all-but 1)"6" (lemma Pos_var_is_finite)"6" (inst -1 s x) (("6" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_sets nil )"positions" subterm nil )"bool" finite_sets nil )"[term -> boolean]" term_adt nil )ext def-decl "term" substitution nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"nat" finite_sets nil )nil finite_sets nil )"term" substitution nil )"finseq" finite_sequences nil )nil finite_sequences nil )"term" replacement nil )nil term_adt nil )nil seq_extras "structures/" )"finseq" finite_sequences nil )nil seq_extras "structures/" )"positions" positions nil )"[variable -> (vars?)]" term_adt nil )nil seq_extras "structures/" )"(total_order?[real])" nil )"bool" reals nil )"symbol" orthogonality nil )"{args: finite_sequence[term[variable, symbol, arity]] | " orthogonality nil) "Sub[variable, symbol, arity]" nil )"(V)" orthogonality nil )"position[variable, symbol, arity]" nil )"term[variable, symbol, arity]" orthogonalitynil )"finseq" seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )replace const-decl "finseq" seq_extras "structures/" )"[(app?) -> symbol]" term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) nil term_adt nil )"[term -> boolean]" term_adt nil )"posint" nil )nil substitution nil )"[bool, bool -> bool]" booleans nil )nil substitution nil )nil substitution nil )"nonneg_int" nil )nil subterm nil )"finite_sequence[T]" set2seq "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props nil )nil nil )nil positions nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil orthogonality nil )"non_empty_finite_set[position]" orthogonality nil )"R" extend nil )"set[T]" indexed_sets nil )"positions" positions nil )"set" sets nil )"(total_order?[real])" nil )"bool" reals nil )nil IUnion_extra nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"set[(V)]" subterm nil )"bool" sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )NOT const-decl "[bool -> bool]" booleans nil )"position[variable, symbol, arity]" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil finite_sequences nil )nil subterm nil )"(singleton?)" sets nil )nil finite_sets nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil orthogonality nil )nil orthogonality nil )"[symbol -> nat]" orthogonality nil )nil positions nil ))nil 3448728252"" (skeep)"" (assert )"" (flatten)"" (lemma "replace_distributivity" )"" (inst -1 p1 p2 t "ext(sg2)(ext(rho2)(rhs(e2p)))" )"" (assert )"" (lemma "pos_subterm" )"" (inst -1 p1 p2 t)"" (assert )"" (lemma "positions_of_ext" )"" (inst -1 "comp(sg1, rho1)" "lhs(e1p)" )"1" (decompose-equality -1)"1" (inst -1 "p2" )"1" (iff)"1" "1" "1" expand * "union" "member" )"1" "1" "ntCP_lemma_aux1" )"1" "comp(sg1, rho1)" "comp(sg2, rho2)" "E" "p2" "e1p" "e2p" )"1" expand Ambiguous?)"1" "1" "1" "t1!1" "t2!1" )nil nil ))nil )"2" "subterm_ext_commute" )"2" "p2" "lhs(e1p)" "comp(sg1, rho1)" )"2" assert )"2" "2" rewrite ext_o)"2" rewrite "2" expand "2" "2" replace "2" replace "2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace -1)"3" replace -2)"3" expand lhs)"3" expand rhs)"3" "3" rewrite "3" replace "3" "3" "3" replace "3" replace "3" replace "3" "3" "3" "3" "3" expand "3" "3" "3" "e2p`2" )"3" "e2p`1" )"3" "e2p`2" )"3" "e2p`1" )"3" replace "3" replace "3" replace "3" replace "3" "3" "3" "comp(sg1, rho1)" "comp(sg2, rho2)" "e2p`1" )"3" "e2p" )"3" expand "3" "3" expand "3" "3" "comp(sg1, rho1)" "comp(sg2, rho2)" "e2p`2" )"3" expand "3" expand *"3" "3" "3" assert )"3" "3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite subs_o)nil nil ))nil )"3" "3" rewrite subs_o)nil nil ))nil ))nil ))nil )"2" "2" "p1p" "p2p" ))"2" expand Linear?)"2" "2" expand Left_Linear?)"2" expand "2" "2" "2" expand "2" "subtermOF(lhs(e1p), p1p)" )"1" "subtermOF(lhs(e1p), p1p)" )"1" "1" "rhs(e1p)" "subtermOF(lhs(e1p), p1p)" )"1" assert )"1" "1" "1" "replaceTerm( t1, ext(SigmaP(comp(sg1, rho1), ext(sg2)(ext(rho2)(rhs(e2p))), ") "1" "1" expand "1" expand *"1" "1" "1" expand "1" "comp(sg2, rho2)" "p1 o (pr o p2p)" )"1" "1" "1" "rhs(e1p)" "comp(sg1, rho1)" )"1" assert )"1" rewrite "1" expand "1" rewrite "1" expand "1" replace "1" replace "1" "1" expand "1" replace "1" "1" "ext(sg1)(ext(rho1)(rhs(e1p)))" )"1" assert )"1" "1" "ext(sg1)(ext(rho1)(rhs(e1p)))" )"1" assert )"1" replace "1" replace "1" "1" "p1 o pr" "1" "1" case "p1 o pr o p2p = p1 o (pr o p2p)" )"1" replace "1" replace "1" "1" "1" "1" "1" "1" assert )"1" "1" replace "1" replace "1" "1" "rhs(e1p)" "comp(sg1, rho1)" )"1" assert )"1" rewrite "1" expand "1" replace "1" replace "1" replace "1" "1" "ext(sg1)(ext(rho1)(lhs(e1p)))" )"1" "1" replace "1" "1" "lhs(e1p)" "comp(sg1, rho1)" )"1" assert )"1" rewrite "1" expand "1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "ext(sg1)(ext(rho1)(lhs(e1p)))" )"2" "1" "1" "lhs(e1p)" "comp(sg1, rho1)" )"1" assert )"1" rewrite "1" expand "1" nil nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil )"2" replace "2" "2" "lhs(e1p)" "comp(sg1, rho1)" )"1" assert )"1" rewrite "1" expand "1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "p1 o pr" "2" "1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" "2" assert )"2" "2" "2" assert )"2" replace "2" replace "2" "2" "rhs(e1p)" "comp(sg1, rho1)" )"1" assert )"1" rewrite "1" expand "1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "rhs(e1p)" "comp(sg1, rho1)" "ext(sg2)(ext(rho2)(rhs(e2p)))" "subtermOF(rhs(e1p), pr)" )"1" assert )"1" replace "1" replace "1" rewrite "1" expand "1" rewrite "1" expand "1" "1" "1" "ext(sg1)(ext(rho1)(rhs(e1p)))" )"1" assert )"1" "1" "ext(sg1)(ext(rho1)(rhs(e1p)))" )"1" assert )"1" replace "1" replace "1" "1" "pr o p2p" "ext(sg2)(ext(rho2)(rhs(e2p)))" "subtermOF(t1, p1)" )"1" "1" replace "1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "rhs(e1p)" "comp(sg1, rho1)" )"1" assert )"1" rewrite "1" expand "1" replace "1" "1" "rhs(e1p)" "comp(sg1, rho1)" )"1" assert )"1" rewrite "1" expand "1" replace "1" "1" replace "1" "1" "subtermOF(t1, p1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "2" expand "2" "2" "ext(sg1)(ext(rho1)(rhs(e1p)))" )"2" assert )"2" replace
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.701Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
