products/sources/formale sprachen/PVS/ints/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: coqProject_file.ml   Sprache: Lisp

Original von: PVS©
(critical_pairs
 (IMP_critical_pairs_aux_TCC1 0
  (IMP_critical_pairs_aux_TCC1-1 nil 3420229945
   ("" (lemma "var_countable") (("" (propax) nil nil)) nil)
   ((var_countable formula-decl nil critical_pairs nil)) nil))
 (CP?_TCC1 0
  (CP?_TCC1-1 nil 3395743409
   ("" (skosimp*)
    (("" (lemma "ext_preserv_pos")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((arity formal-const-decl "[symbol -> nat]" critical_pairs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (symbol formal-nonempty-type-decl nil critical_pairs nil)
    (variable formal-nonempty-type-decl nil critical_pairs nil)
    (ext_preserv_pos formula-decl nil substitution nil)
    (Sub type-eq-decl nil substitution nil)
    (Sub? const-decl "bool" substitution nil)
    (V const-decl "set[term]" variables_term nil)
    (positions? type-eq-decl nil positions nil)
    (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
    (lhs const-decl "term" rewrite_rules nil)
    (rewrite_rule type-eq-decl nil rewrite_rules nil)
    (rewrite_rule? const-decl "bool" rewrite_rules nil)
    (positionsOF def-decl "positions" positions nil)
    (positions type-eq-decl nil positions nil)
    (term type-decl nil term_adt nil)
    (position type-eq-decl nil positions nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (below type-eq-decl nil nat_types nil))
   nil))
 (CP_lemma_aux1a_TCC1 0
  (CP_lemma_aux1a_TCC1-1 nil 3406618276
   ("" (skosimp*)
    (("" (hide-all-but 2)
      (("" (typepred "alpha!1" "rho!1")
        (("" (hide -3) (("" (rewrite "subs_o") nil nil)) nil)) nil))
      nil))
    nil)
   ((subs_o formula-decl nil substitution nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (variable formal-nonempty-type-decl nil critical_pairs nil)
    (symbol formal-nonempty-type-decl nil critical_pairs nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (arity formal-const-decl "[symbol -> nat]" critical_pairs nil)
    (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
    (V const-decl "set[term]" variables_term nil)
    (Sub? const-decl "bool" substitution nil)
    (Sub type-eq-decl nil substitution nil)
    (Ren? const-decl "bool" substitution nil)
    (Ren type-eq-decl nil substitution nil))
   nil))
 (CP_lemma_aux1a 0
  (CP_lemma_aux1a-1 nil 3406746822
   ("" (skosimp*)
    (("" (lemma "exists_renaming")
      (("" (inst -1 "Vars(lhs(e2!1))" "Vars(lhs(e1!1))")
        (("1" (skosimp*)
          (("1" (lemma "inverse_renaming")
            (("1" (inst?)
              (("1" (skosimp*)
                (("1" (lemma "inverse_rename_identity")
                  (("1" (inst -1 "rho!1" "rho1!1" "lhs(e2!1)")
                    (("1" (prop)
                      (("1" (inst 2 "comp(sg2!1, rho1!1)" "rho!1")
                        (("1" (split)
                          (("1" (lemma "vars_term_rename")
                            (("1" (inst?)
                              (("1"
                                (assert)
                                (("1"
                                  (lemma
                                   "IUnion_extra[(V)].disjoint_subset")
                                  (("1"
                                    (inst
                                     -1
                                     "Vars(lhs(e1!1))"
                                     "Vars(lhs(e1!1))"
                                     "Vars(ext(rho!1)(lhs(e2!1)))"
                                     "restrict[term[variable, symbol, arity], ((V)), boolean](Ran(rho!1))")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (hide-all-but 1)
                                        (("1"
                                          (expand* "subset?" "member")
                                          (("1" (skeep) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide (-4 2))
                            (("2" (rewrite "o_ass")
                              (("2"
                                (rewrite "ext_o")
                                (("2"
                                  (expand "o")
                                  (("2" (replaces -1) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (rewrite "subs_o") nil nil))
                        nil)
                       ("2" (hide-all-but (-2 1))
                        (("2" (expand* "subset?" "member")
                          (("2" (skosimp*)
                            (("2" (decompose-equality -2)
                              (("2"
                                (inst -1 "x!1")
                                (("2"
                                  (iff)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide-all-but 1)
          (("2" (rewrite "vars_of_term_finite") nil nil)) nil)
         ("3" (hide-all-but 1)
          (("3" (rewrite "vars_of_term_finite") nil nil)) nil))
        nil))
      nil))
    nil)
   ((arity formal-const-decl "[symbol -> nat]" critical_pairs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (symbol formal-nonempty-type-decl nil critical_pairs nil)
    (variable formal-nonempty-type-decl nil critical_pairs nil)
    (exists_renaming formula-decl nil substitution nil)
    (vars_of_term_finite formula-decl nil subterm nil)
    (Ren type-eq-decl nil substitution nil)
    (Ren? const-decl "bool" substitution nil)
    (Sub type-eq-decl nil substitution nil)
    (Sub? const-decl "bool" substitution nil)
    (inverse_rename_identity formula-decl nil substitution nil)
    (subs_o formula-decl nil substitution nil)
    (disjoint_subset formula-decl nil IUnion_extra nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset? const-decl "bool" sets nil)
    (ext def-decl "term" substitution nil)
    (restrict const-decl "R" restrict nil)
    (Ran const-decl "set[term]" substitution nil)
    (vars_term_rename formula-decl nil substitution nil)
    (o_ass formula-decl nil substitution nil)
    (O const-decl "T3" function_props nil)
    (ext_o formula-decl nil substitution nil)
    (rho1!1 skolem-const-decl "Ren[variable, symbol, arity]"
     critical_pairs nil)
    (sg2!1 skolem-const-decl "Sub[variable, symbol, arity]"
     critical_pairs nil)
    (comp const-decl "term" substitution nil)
    (Dom const-decl "set[(V)]" substitution nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (inverse_renaming formula-decl nil substitution nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (e1!1 skolem-const-decl "{e1 | member(e1, E!1)}" critical_pairs
     nil)
    (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
    (V const-decl "set[term]" variables_term nil)
    (is_finite const-decl "bool" finite_sets nil)
    (Vars const-decl "set[(V)]" subterm nil)
    (rewrite_rule? const-decl "bool" rewrite_rules nil)
    (rewrite_rule type-eq-decl nil rewrite_rules nil)
    (lhs const-decl "term" rewrite_rules nil)
    (member const-decl "bool" sets nil)
    (E!1 skolem-const-decl "set[rewrite_rule]" critical_pairs nil)
    (e2!1 skolem-const-decl "{e2 | member(e2, E!1)}" critical_pairs
     nil))
   shostak))
 (CP_lemma_aux1_TCC1 0
  (CP_lemma_aux1_TCC1-1 nil 3402063728
   ("" (skosimp*)
    (("" (hide-all-but (-1 2))
      (("" (rewrite "ext_preserv_pos") nil nil)) nil))
    nil)
   ((arity formal-const-decl "[symbol -> nat]" critical_pairs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (symbol formal-nonempty-type-decl nil critical_pairs nil)
    (variable formal-nonempty-type-decl nil critical_pairs nil)
    (Sub type-eq-decl nil substitution nil)
    (Sub? const-decl "bool" substitution nil)
    (V const-decl "set[term]" variables_term nil)
    (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
    (lhs const-decl "term" rewrite_rules nil)
    (rewrite_rule type-eq-decl nil rewrite_rules nil)
    (rewrite_rule? const-decl "bool" rewrite_rules nil)
    (term type-decl nil term_adt nil)
    (position type-eq-decl nil positions nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (below type-eq-decl nil nat_types nil)
    (ext_preserv_pos formula-decl nil substitution nil))
   nil))
 (CP_lemma_aux1 0
  (CP_lemma_aux1-1 nil 3402063736
   ("" (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"
                  (inst -1 "subtermOF(lhs(e1!1), p!1)"
                   "ext(rho!1)(lhs(e2!1))")
                  (("1" (prop)
                    (("1" (skosimp*)
                      (("1" (copy -1)
                        (("1" (expand "mgu" -1)
                          (("1" (flatten)
                            (("1" (hide -1)
                              (("1"
                                (inst
                                 -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"
                                            (skosimp*)
                                            (("1"
                                              (inst
                                               2
                                               "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"
                                                (lemma "ext_o")
                                                (("1"
                                                  (inst
                                                   -1
                                                   "tau!1"
                                                   "theta!1")
                                                  (("1"
                                                    (decompose-equality
                                                     -1)
                                                    (("1"
                                                      (split)
                                                      (("1"
                                                        (hide -1)
                                                        (("1"
                                                          (expand
                                                           "CP?")
                                                          (("1"
                                                            (inst
                                                             1
                                                             "theta!1"
                                                             "rho!1"
                                                             "e1!1"
                                                             "e2!1"
                                                             "p!1")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (inst
                                                         -1
                                                         "rhs(e1!1)")
                                                        (("2"
                                                          (expand "o")
                                                          (("2"
                                                            (replace
                                                             -1
                                                             1
                                                             rl)
                                                            (("2"
                                                              (hide -1)
                                                              (("2"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("2"
                                                                  (hide
                                                                   -1)
                                                                  (("2"
                                                                    (lemma
                                                                     "restriction_union")
                                                                    (("2"
                                                                      (inst
                                                                       -1
                                                                       "restriction(sg1!1)(Vars(lhs(e1!1)))"
                                                                       "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))"
                                                                       "rhs(e1!1)")
                                                                      (("1"
                                                                        (lemma
                                                                         "dom_restriction")
                                                                        (("1"
                                                                          (copy
                                                                           -1)
                                                                          (("1"
                                                                            (inst
                                                                             -1
                                                                             "Vars(lhs(e1!1))"
                                                                             "sg1!1")
                                                                            (("1"
                                                                              (inst
                                                                               -2
                                                                               "Vars(ext(rho!1)(lhs(e2!1)))"
                                                                               "alpha!1")
                                                                              (("1"
                                                                                (lemma
                                                                                 "IUnion_extra[(V)].disjoint_subset")
                                                                                (("1"
                                                                                  (inst
                                                                                   -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"
                                                                                      (prop)
                                                                                      (("1"
                                                                                        (replace
                                                                                         -1
                                                                                         1)
                                                                                        (("1"
                                                                                          (lemma
                                                                                           "restriction_term")
                                                                                          (("1"
                                                                                            (inst?)
                                                                                            (("1"
                                                                                              (prop)
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil)
                                                                                               ("2"
                                                                                                (hide-all-but
                                                                                                 1)
                                                                                                (("2"
                                                                                                  (typepred
                                                                                                   "e1!1")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "rewrite_rule?")
                                                                                                    (("2"
                                                                                                      (expand*
                                                                                                       "lhs"
                                                                                                       "rhs")
                                                                                                      (("2"
                                                                                                        (prop)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (hide-all-but
                                                                                         (-2
                                                                                          -3
                                                                                          -6
                                                                                          1))
                                                                                        (("2"
                                                                                          (lemma
                                                                                           "IUnion_extra[(V)].disjoint_subset")
                                                                                          (("2"
                                                                                            (inst
                                                                                             -1
                                                                                             "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"
                                                                                              (prop)
                                                                                              (("1"
                                                                                                (hide-all-but
                                                                                                 1)
                                                                                                (("1"
                                                                                                  (expand*
                                                                                                   "subset?"
                                                                                                   "member")
                                                                                                  (("1"
                                                                                                    (skeep)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (hide-all-but
                                                                                                 (-3
                                                                                                  1))
                                                                                                (("2"
                                                                                                  (lemma
                                                                                                   "IUnion_extra[(V)].disjoint_subset")
                                                                                                  (("2"
                                                                                                    (inst
                                                                                                     -1
                                                                                                     "Vars(rhs(e1!1))"
                                                                                                     "Vars(lhs(e1!1))"
                                                                                                     "Vars(ext(rho!1)(lhs(e2!1)))"
                                                                                                     "Vars(ext(rho!1)(lhs(e2!1)))")
                                                                                                    (("2"
                                                                                                      (prop)
                                                                                                      (("1"
                                                                                                        (hide
                                                                                                         (-1
                                                                                                          2))
                                                                                                        (("1"
                                                                                                          (typepred
                                                                                                           "e1!1")
                                                                                                          (("1"
                                                                                                            (expand*
                                                                                                             "rewrite_rule?"
                                                                                                             "lhs"
                                                                                                             "rhs")
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil)
                                                                                                       ("2"
                                                                                                        (hide
                                                                                                         (-1
                                                                                                          2))
                                                                                                        (("2"
                                                                                                          (expand*
                                                                                                           "subset?"
                                                                                                           "member")
                                                                                                          (("2"
                                                                                                            (skeep)
                                                                                                            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"
                                                        (lemma
                                                         "ext_replace_ext")
                                                        (("3"
                                                          (inst?)
                                                          (("3"
                                                            (prop)
                                                            (("1"
                                                              (replaces
                                                               -1)
                                                              (("1"
                                                                (copy
                                                                 -1)
                                                                (("1"
                                                                  (inst
                                                                   -1
                                                                   "ext(rho!1)(rhs(e2!1))")
                                                                  (("1"
                                                                    (inst
                                                                     -2
                                                                     "lhs(e1!1)")
                                                                    (("1"
                                                                      (expand
                                                                       "o")
                                                                      (("1"
                                                                        (replace
                                                                         -1
                                                                         1
                                                                         rl)
                                                                        (("1"
                                                                          (replace
                                                                           -2
                                                                           1
                                                                           rl)
                                                                          (("1"
                                                                            (replace
                                                                             -3
                                                                             1
                                                                             rl)
                                                                            (("1"
                                                                              (hide
                                                                               (-1
                                                                                -2
                                                                                -3))
                                                                              (("1"
                                                                                (lemma
                                                                                 "restriction_union")
                                                                                (("1"
                                                                                  (copy
                                                                                   -1)
                                                                                  (("1"
                                                                                    (inst
                                                                                     -1
                                                                                     "restriction(sg1!1)(Vars(lhs(e1!1)))"
                                                                                     "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))"
                                                                                     "lhs(e1!1)")
                                                                                    (("1"
                                                                                      (inst
                                                                                       -2
                                                                                       "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))"
                                                                                       "restriction(sg1!1)(Vars(lhs(e1!1)))"
                                                                                       "ext(rho!1)(rhs(e2!1))")
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "dom_restriction")
                                                                                        (("1"
                                                                                          (copy
                                                                                           -1)
                                                                                          (("1"
                                                                                            (inst
                                                                                             -1
                                                                                             "Vars(lhs(e1!1))"
                                                                                             "sg1!1")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -2
                                                                                               "Vars(ext(rho!1)(lhs(e2!1)))"
                                                                                               "alpha!1")
                                                                                              (("1"
                                                                                                (lemma
                                                                                                 "IUnion_extra[(V)].disjoint_subset")
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   -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"
                                                                                                      (lemma
                                                                                                       "IUnion_extra[(V)].disjoint_commute")
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         -1
                                                                                                         "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))"
                                                                                                         "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))")
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          (("1"
                                                                                                            (prop)
                                                                                                            (("1"
                                                                                                              (rewrite
                                                                                                               "union_commute")
                                                                                                              (("1"
                                                                                                                (replaces
                                                                                                                 -1)
                                                                                                                (("1"
                                                                                                                  (replaces
                                                                                                                   -1)
                                                                                                                  (("1"
                                                                                                                    (lemma
                                                                                                                     "restriction_term")
                                                                                                                    (("1"
                                                                                                                      (copy
                                                                                                                       -1)
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -1
                                                                                                                         "Vars(ext(rho!1)(lhs(e2!1)))"
                                                                                                                         "alpha!1"
                                                                                                                         "ext(rho!1)(rhs(e2!1))")
                                                                                                                        (("1"
                                                                                                                          (inst
                                                                                                                           -2
                                                                                                                           "Vars(lhs(e1!1))"
                                                                                                                           "sg1!1"
                                                                                                                           "lhs(e1!1)")
                                                                                                                          (("1"
                                                                                                                            (prop)
                                                                                                                            (("1"
                                                                                                                              (replace
                                                                                                                               -1
                                                                                                                               1
                                                                                                                               rl)
                                                                                                                              (("1"
                                                                                                                                (replace
                                                                                                                                 -2
                                                                                                                                 1
                                                                                                                                 rl)
                                                                                                                                (("1"
                                                                                                                                  (rewrite
                                                                                                                                   "ext_o")
                                                                                                                                  (("1"
                                                                                                                                    (expand
                                                                                                                                     "o")
                                                                                                                                    (("1"
                                                                                                                                      (case-replace
                                                                                                                                       "ext(alpha!1)(ext(rho!1)(rhs(e2!1))) = ext(sg2!1)(rhs(e2!1))")
                                                                                                                                      (("1"
                                                                                                                                        (hide-all-but
                                                                                                                                         (-10
                                                                                                                                          -12
                                                                                                                                          1))
                                                                                                                                        (("1"
                                                                                                                                          (replaces
                                                                                                                                           -1)
                                                                                                                                          (("1"
                                                                                                                                            (lemma
                                                                                                                                             "ext_o")
                                                                                                                                            (("1"
                                                                                                                                              (inst
                                                                                                                                               -1
                                                                                                                                               "alpha!1"
                                                                                                                                               "rho!1")
                                                                                                                                              (("1"
                                                                                                                                                (copy
                                                                                                                                                 -1)
                                                                                                                                                (("1"
                                                                                                                                                  (decompose-equality
                                                                                                                                                   -1)
                                                                                                                                                  (("1"
                                                                                                                                                    (decompose-equality
                                                                                                                                                     -2)
                                                                                                                                                    (("1"
                                                                                                                                                      (inst
                                                                                                                                                       -1
                                                                                                                                                       "lhs(e2!1)")
                                                                                                                                                      (("1"
                                                                                                                                                        (inst
                                                                                                                                                         -2
                                                                                                                                                         "rhs(e2!1)")
                                                                                                                                                        (("1"
                                                                                                                                                          (expand
                                                                                                                                                           "o")
                                                                                                                                                          (("1"
                                                                                                                                                            (replace
                                                                                                                                                             -1
                                                                                                                                                             *
                                                                                                                                                             rl)
                                                                                                                                                            (("1"
                                                                                                                                                              (replace
                                                                                                                                                               -2
                                                                                                                                                               *
                                                                                                                                                               rl)
                                                                                                                                                              (("1"
                                                                                                                                                                (hide
                                                                                                                                                                 (-1
                                                                                                                                                                  -2))
                                                                                                                                                                (("1"
                                                                                                                                                                  (lemma
                                                                                                                                                                   "same_substitution")
                                                                                                                                                                  (("1"
                                                                                                                                                                    (inst
                                                                                                                                                                     -1
                                                                                                                                                                     "comp(alpha!1, rho!1)"
                                                                                                                                                                     "sg2!1"
                                                                                                                                                                     "lhs(e2!1)")
                                                                                                                                                                    (("1"
                                                                                                                                                                      (assert)
                                                                                                                                                                      (("1"
                                                                                                                                                                        (lemma
                                                                                                                                                                         "same_term")
                                                                                                                                                                        (("1"
                                                                                                                                                                          (inst
                                                                                                                                                                           -1
                                                                                                                                                                           "comp(alpha!1, rho!1)"
                                                                                                                                                                           "sg2!1"
                                                                                                                                                                           "rhs(e2!1)")
                                                                                                                                                                          (("1"
                                                                                                                                                                            (prop)
                                                                                                                                                                            (("1"
                                                                                                                                                                              (skosimp*)
                                                                                                                                                                              (("1"
                                                                                                                                                                                (hide
                                                                                                                                                                                 (-3
                                                                                                                                                                                  2))
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.59 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

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.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff