Loading theory "FOL-ex.Classical"
Loading theory "FOL-ex.If"
### theory "FOL-ex.If"
### 0.090s elapsed time, 0.180s cpu time, 0.000s GC time
Loading theory "FOL-ex.Intro"
### theory "FOL-ex.Intro"
### 0.024s elapsed time, 0.048s cpu time, 0.000s GC time
Loading theory "FOL-ex.Miniscope"
### Ignoring duplicate rewrite rule:
### \<not> (?P1 \<and> ?Q1) \<equiv> \<not> ?P1 \<or> \<not> ?Q1
### Ignoring duplicate rewrite rule:
### \<not> (?P1 \<or> ?Q1) \<equiv> \<not> ?P1 \<and> \<not> ?Q1
### Ignoring duplicate rewrite rule:
### \<not> \<not> ?Q \<equiv> ?Q
### Ignoring duplicate rewrite rule:
### \<not> (\<forall>x. ?P1(x)) \<equiv> \<exists>x. \<not> ?P1(x)
### Ignoring duplicate rewrite rule:
### \<not> (?P1 \<longrightarrow> ?Q1) \<equiv> ?P1 \<and> \<not> ?Q1
### Ignoring duplicate rewrite rule:
### \<forall>x. ?Q \<equiv> ?Q
val mini_ss =
   Simpset
    ({depth = (0, ref false), prems = [], rules =
      Net {atoms = {}, comb =
           Net {atoms =
                {("IFOL.Ex",
                   Net {atoms = {}, comb =
                        Net {atoms =
                             {("IFOL.eq",
                                Net {atoms = {}, comb = Leaf [], var =
                                     Leaf
[{elhs = "......", extra = false, fo = true, lhs =
  Const ("...", ...) $ Abs ("...", "?'b1", ...), name = "FOL.IFOL_simps_37",
  ...}]})},
                             comb = Leaf [], var = Leaf []},
                        var =
                        Leaf
                         [{elhs = "\<exists>x. ?P1 \<or> ?Q1(x)", extra =
                           false, fo = false, lhs =
                           Const ("IFOL.Ex",
                                  "(... ... ...) \<Rightarrow> o") $
                             Abs ("x", "?'f1",
                               Const ("...", ...) $ Var ((...), "o") $ ...),
                           name = "Miniscope.mini_simps_15", perm = false,
                           thm =
                           "\<exists>x. ?P1 \<or> ?Q1......... \<equiv>
                            ?P1 \<or> (...x... ......)"},
                          {elhs = "\<exists>x. ?P1(x) \<or> ?Q1", extra =
                           false, fo = false, lhs =
                           Const ("IFOL.Ex", "(...) ... o") $
                             Abs ("x", "?'e1",
                               Const ("...",
"o \<Rightarrow> o \<Rightarrow> o") $
                                 ... $ ...),
                           name = "Miniscope.mini_simps_14", perm = false,
                           thm =
                           "\<exists>x. ...... ... ?Q1 \<equiv>
                            (......... ...) \<or> ?Q1"},
                          {elhs =
                           "\<exists>x. ?P1......... \<or> ?Q1.........",
                           extra = false, fo = false, lhs =
                           Const ("IFOL.Ex", "... ... ...") $
                             Abs ("x", "...", ... $ ... $ ...),
                           name = "Miniscope.mini_simps_13", perm = false,
                           thm =
                           "...x... ... ... ... \<equiv> (...) ... (...)"},
                          {elhs = "\<exists>x. ?P1 ... ......", extra =
                           false, fo = false, lhs =
                           Const ("IFOL.Ex", "...") $ Abs ("x", "...", ...),
                           name = "Miniscope.mini_simps_12", perm = false,
                           thm = "......... ... ... ... ... ..."},
                          {elhs = "...x... ... ... ...", extra = false, fo =
                           false, lhs =
                           Const ("IFOL.Ex", "...") $ Abs ("x", ..., ...),
                           name = "Miniscope.mini_simps_11", perm = false,
                           thm = "... ... ..."},
                          {elhs = "......... ...", extra = false, fo = true,
                           lhs =
                           Const ("...", ...) $ Abs ("...", "?'a1", ...),
                           name = "Miniscope.mini_simps_10", ...},
                          {elhs = "...", extra = false, fo = false, lhs =
                           Const ("...",
                                  "(?'b1 \<Rightarrow> o)
                                   \<Rightarrow> o") $
                             ...,
                           ...},
                          {elhs = "...", extra = false, fo = false, ...},
                          {elhs = ..., extra = false, ...}, ...]}),
                  ("IFOL.All",
                    Net {atoms = {}, comb = Leaf [], var =
                         Leaf
                          [{elhs = "\<forall>x. ?P1 \<or> ?Q1(x)", extra =
                            false, fo = false, lhs =
                            Const ("IFOL.All", "(...) ... o") $
                              Abs ("x", "?'f1",
                                Const ("...",
 "o \<Rightarrow> o \<Rightarrow> o") $
                                  ... $ ...),
                            name = "Miniscope.mini_simps_21", perm = false,
                            thm =
                            "\<forall>x. ?P1 ... ...... \<equiv>
                             ?P1 \<or> (......... ...)"},
                           {elhs = "\<forall>x. ?P1......... \<or> ?Q1",
                            extra = false, fo = false, lhs =
                            Const ("IFOL.All", "... ... ...") $
                              Abs ("x", "...", ... $ ... $ ...),
                            name = "Miniscope.mini_simps_20", perm = false,
                            thm =
                            "...x... ... ... ... \<equiv> (...) ... ?Q1"},
                           {elhs = "\<forall>x. ?P1 ... ......", extra =
                            false, fo = false, lhs =
                            Const ("IFOL.All", "...") $
                              Abs ("x", "...", ...),
                            name = "Miniscope.mini_simps_19", perm = false,
                            thm = "......... ... ... ... ... ..."},
                           {elhs = "...x... ... ... ...", extra = false,
                            fo = false, lhs =
                            Const ("IFOL.All", "...") $ Abs ("x", ..., ...),
                            name = "Miniscope.mini_simps_18", perm = false,
                            thm = "... ... ..."},
                           {elhs = "......... ...", extra = false, fo =
                            false, lhs =
                            Const ("...", ...) $ Abs ("...", "?'b1", ...),
                            name = "Miniscope.mini_simps_17", ...},
                           {elhs = "...", extra = false, fo = false, lhs =
                            Const ("...",
                                   "(?'b1 \<Rightarrow> o)
                                    \<Rightarrow> o") $
                              ...,
                            ...},
                           {elhs = "...", extra = false, fo = false, ...},
                           {elhs = ..., extra = false, ...}, ...]}),
                  ("IFOL.Not",
                    Net {atoms =
                         {("IFOL.True",
                            Leaf
                             [{elhs = "\<not> True", extra = false, fo =
                               true, lhs =
                               Const ("IFOL.Not", "...") $
                                 Const ("IFOL.True", "..."),
                               name = "FOL.IFOL_simps_20", perm = false,
                               thm = "... True ... False"}]),
                           ("IFOL.False",
                             Leaf
                              [{elhs = "\<not> False", extra = false, fo =
                                true, lhs =
                                Const ("IFOL.Not", "...") $
                                  Const ("...", ...),
                                name = "FOL.IFOL_simps_19", perm = false,
                                thm = "... ... ... ..."}])},
                         comb =
                         Net {atoms =
                              {("IFOL.Ex",
                                 Net {atoms = {}, comb = Leaf [], var =
Leaf
 [{elhs = "...", extra = false, fo = true, ...},
  {elhs = ..., extra = false, ...}]}),
                                ("IFOL.All",
                                  Net {atoms = {}, comb = Leaf [], var =
 Leaf [{elhs = ..., extra = false, ...}]}),
                                ("IFOL.Not",
                                  Net {atoms = {}, comb = Leaf [...], var =
 Leaf [...]})},
                              comb =
                              Net {atoms =
                                   {("IFOL.iff",
Net {atoms = {}, comb = Leaf [...], var = Net {atoms = {}, ...}}),
                                     ("IFOL.imp",
 Net {atoms = {}, comb = ..., var = ...}),
                                     ("IFOL.conj", Net {atoms = {}, ...}),
                                     ("IFOL.disj", ...)},
                                   comb = Leaf [], var = Leaf []},
                              var = Leaf []},
                         var = Leaf []}),
                  ("Pure.all",
                    Net {atoms = {}, comb = Leaf [], var =
                         Leaf
                          [{elhs = "\<And>x. PROP ?V", extra = false, fo =
                            true, lhs =
                            Const ("Pure.all", "...") $
                              Abs ("x", "...", ...),
                            name = "FOL.meta_simps_1", perm = false, thm =
                            "(...) ... PROP ?V"}]})},
                comb =
                Net {atoms =
                     {("IFOL.eq",
                        Net {atoms = {}, comb = Leaf [], var =
                             Net {atoms = {}, comb = Leaf [], var =
                                  Leaf
                                   [{elhs = "?a1 ... ?a1", extra = false,
                                     fo = true, lhs =
                                     Const ("IFOL.eq", "...") $
 Var (("...", 1), ...) $ Var ((...), "?'a1"),
                                     name = "FOL.IFOL_simps_1", perm =
                                     false, thm = "... ... ..."}]}}),
                       ("IFOL.iff",
                         Net {atoms =
                              {("IFOL.True",
                                 Net {atoms = {}, comb = Leaf [], var =
Leaf
 [{elhs = "...", extra = false, fo = true, lhs =
   Const ("...", "o \<Rightarrow> o \<Rightarrow> o") $ ... $ ..., ...}]}),
                                ("IFOL.False",
                                  Net {atoms = {}, comb = Leaf [], var =
 Leaf [{elhs = "...", extra = false, fo = true, ...}]})},
                              comb =
                              Net {atoms =
                                   {("IFOL.Not",
Net {atoms = {}, comb = Leaf [], var =
     Net {atoms = {}, comb = ..., var = ...}})},
                                   comb =
                                   Net {atoms =
  {("IFOL.imp", Net {atoms = {}, comb = ..., var = ...})}, comb = Leaf [],
  var = Leaf []},
                                   var = Leaf []},
                              var =
                              Net {atoms =
                                   {("IFOL.True",
Leaf
 [{elhs = "...", extra = false, fo = true, lhs =
   Const ("...", "o \<Rightarrow> o \<Rightarrow> o") $ ... $ ..., ...}]),
                                     ("IFOL.False",
 Leaf [{elhs = "...", extra = false, fo = true, ...}])},
                                   comb = Leaf [], var =
                                   Leaf
                                    [{elhs = "... ... ...", extra = false,
fo = true, lhs = Const ("...", ...) $ Var ((...), "o") $ ..., name =
"Miniscope.mini_simps_8", ...},
                                     {elhs = "...", extra = false, fo =
true, lhs = Const ("...", "o \<Rightarrow> o \<Rightarrow> o") $ ... $ ...,
...}]}}),
                       ("IFOL.imp",
                         Net {atoms =
                              {("IFOL.True",
                                 Net {atoms = {}, comb = Leaf [], var =
Leaf [{elhs = "...", extra = false, fo = true, ...}]}),
                                ("IFOL.False",
                                  Net {atoms = {}, comb = Leaf [], var =
 Leaf [{elhs = ..., extra = false, ...}]})},
                              comb =
                              Net {atoms =
                                   {("IFOL.Not",
Net {atoms = {}, comb = Leaf [...], var = Net {atoms = {}, ...}})},
                                   comb = Leaf [], var = Leaf []},
                              var =
                              Net {atoms =
                                   {("IFOL.True",
Leaf [{elhs = "...", extra = false, fo = true, ...}]),
                                     ("IFOL.False",
 Leaf [{elhs = ..., extra = false, ...}])},
                                   comb =
                                   Net {atoms =
  {("IFOL.Not", Net {atoms = {}, ...})}, comb = Leaf [], var = Leaf []},
                                   var =
                                   Leaf
                                    [{elhs = "...", extra = false, fo =
true, lhs = Const ("...", "o \<Rightarrow> o \<Rightarrow> o") $ ... $ ...,
...},
                                     {elhs = "...", extra = false, fo =
true, ...}]}}),
                       ("Pure.imp",
                         Net {atoms = {}, comb =
                              Net {atoms =
                                   {("IFOL.Trueprop",
Net {atoms = {...}, comb = ..., var = ...})},
                                   comb = Leaf [], var = Leaf []},
                              var = Leaf []}),
                       ("IFOL.conj",
                         Net {atoms =
                              {("IFOL.True",
                                 Net {atoms = {}, comb = Leaf [...], var =
Leaf [...]}),
                                ("IFOL.False",
                                  Net {atoms = {}, comb = ..., var = ...})},
                              comb =
                              Net {atoms =
                                   {("IFOL.Not", Net {atoms = {}, ...})},
                                   comb =
                                   Net {atoms = {...}, comb = ..., var =
  ...},
                                   var = Leaf []},
                              var =
                              Net {atoms =
                                   {("IFOL.True", Leaf [...]),
                                     ("IFOL.False", ...)},
                                   comb =
                                   Net {atoms = {...}, comb = ..., var =
  ...},
                                   var =
                                   Leaf
                                    [{elhs = ..., extra = false, ...}]}}),
                       ("IFOL.disj",
                         Net {atoms =
                              {("IFOL.True",
                                 Net {atoms = {}, comb = ..., var = ...}),
                                ("IFOL.False", Net {atoms = {}, ...})},
                              comb =
                              Net {atoms = {("IFOL.Not", ...)}, comb =
                                   Net {atoms = {...}, ...}, var =
                                   Leaf [...]},
                              var =
                              Net {atoms = {("IFOL.True", ...), ...}, comb =
                                   Net {atoms = {...}, ...}, var =
                                   Leaf [...]}})},
                     comb = Leaf [], var = Leaf []},
                var = Leaf []},
           var = Leaf []}},
     {congs =
      ([((true, "IFOL.imp"),
         "\<lbrakk>?P \<equiv> ?P';
           ?P' \<Longrightarrow> ?Q \<equiv> ?Q'\<rbrakk>
          \<Longrightarrow> ?P \<longrightarrow> ?Q \<equiv>
                            ?P' \<longrightarrow> ?Q'")],
       []),
      loop_tacs = [], mk_rews =
      {mk = fn, mk_cong = fn, mk_eq_True = fn, mk_sym = fn, reorient = fn},
      procs =
      Net {atoms = {}, comb =
           Net {atoms =
                {("IFOL.Ex",
                   Net {atoms = {}, comb = Leaf [], var =
                        Leaf
                         [Proc
                           {lhs =
                            Const ("IFOL.Ex", "(...) ... o") $
                              Abs ("x", "?'a",
                                Var ((...), "?'a \<Rightarrow> o") $ ...),
                            name = "FOL.defined_Ex", proc = fn, stamp =
                            Stamp 62004}]}),
                  ("IFOL.All",
                    Net {atoms = {}, comb = Leaf [], var =
                         Leaf
                          [Proc
                            {lhs =
                             Const ("IFOL.All", "... ... ...") $
                               Abs ("x", "...", ... $ ...),
                             name = "FOL.defined_All", proc = fn, stamp =
                             Stamp 62050}]})},
                comb = Leaf [], var = Leaf []},
           var = Leaf []},
      solvers =
      ([Solver {id = Stamp 61872, name = "FOL unsafe", solver = fn}],
       [Solver {id = Stamp 61870, name = "FOL safe", solver = fn}]),
      subgoal_tac = fn, term_ord = fn}):
   simpset
val mini_tac = fn: Proof.context -> int -> tactic
### theory "FOL-ex.Miniscope"
### 0.057s elapsed time, 0.112s cpu time, 0.000s GC time
Loading theory "FOL-ex.Nat"
### theory "FOL-ex.Nat"
### 0.033s elapsed time, 0.064s cpu time, 0.000s GC time
Loading theory "FOL-ex.Nat_Class"
class nat = term +
  fixes Zero :: "'a" 
    and Suc :: "'a \<Rightarrow> 'a" 
    and
    rec ::
      "'a \<Rightarrow> 'a \<Rightarrow> ('a
    \<Rightarrow> 'a \<Rightarrow> 'a)
   \<Rightarrow> 'a"
      
  assumes
    "induct":
      "\<And>P n.
          \<lbrakk>P(0); \<And>x. P(x) \<Longrightarrow> P(Suc(x))\<rbrakk>
          \<Longrightarrow> P(n)"
    and "Suc_inject": "\<And>m n. Suc(m) = Suc(n) \<Longrightarrow> m = n"
    and "Suc_neq_Zero": "\<And>m R. Suc(m) = 0 \<Longrightarrow> R"
    and "rec_Zero": "\<And>a f. rec(0, a, f) = a"
    and "rec_Suc": "\<And>m a f. rec(Suc(m), a, f) = f(m, rec(m, a, f))"
### theory "FOL-ex.Nat_Class"
### 0.067s elapsed time, 0.132s cpu time, 0.000s GC time
Loading theory "FOL-ex.Natural_Numbers"
### theory "FOL-ex.Natural_Numbers"
### 0.031s elapsed time, 0.064s cpu time, 0.000s GC time
Loading theory "FOL-ex.Prolog"
val prolog_tac = fn: Proof.context -> tactic
### theory "FOL-ex.Prolog"
### 0.099s elapsed time, 0.196s cpu time, 0.000s GC time
Loading theory "FOL-ex.Propositional_Cla"
### theory "FOL-ex.Propositional_Cla"
### 0.059s elapsed time, 0.116s cpu time, 0.000s GC time
Loading theory "FOL-ex.Quantifiers_Cla"
### theory "FOL-ex.Classical"
### 0.514s elapsed time, 1.016s cpu time, 0.000s GC time
Loading theory "FOL-ex.Foundation"
### theory "FOL-ex.Quantifiers_Cla"
### 0.056s elapsed time, 0.112s cpu time, 0.000s GC time
Loading theory "FOL-ex.Intuitionistic"
### theory "FOL-ex.Foundation"
### 0.028s elapsed time, 0.056s cpu time, 0.000s GC time
Loading theory "FOL-ex.Propositional_Int"
### theory "FOL-ex.Propositional_Int"
### 0.062s elapsed time, 0.120s cpu time, 0.000s GC time
Loading theory "FOL-ex.Quantifiers_Int"
### theory "FOL-ex.Quantifiers_Int"
### 0.075s elapsed time, 0.148s cpu time, 0.000s GC time
### theory "FOL-ex.Intuitionistic"
### 0.293s elapsed time, 0.580s cpu time, 0.000s GC time
Loading theory "FOL-ex.Locale_Test1" (required by "FOL-ex.Locale_Test")
### Ambiguous input (line 22 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy") produces 2 parse trees:
### ("\<^const>IFOL.Trueprop"
###   ("\<^const>IFOL.eq"
###     ("\<^const>Locale_Test1.minus"
###       ("\<^const>Locale_Test1.minus" ("_position" x)))
###     ("_position" x)))
### ("\<^const>IFOL.Trueprop"
###   ("\<^const>Locale_Test1.minus"
###     ("\<^const>IFOL.eq" ("\<^const>Locale_Test1.minus" ("_position" x))
###       ("_position" x))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
locale param1
  fixes p :: "'a" 
locale param1
  fixes p :: "'a" 
locale param2
  fixes p :: "'b" 
locale param2
  fixes p :: "'b" 
locale param3
  fixes p :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"   (infix ".." 50)
locale param3
  fixes p :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"   (infix ".." 50)
locale param4
  fixes p :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infix ".." 50)
locale param4
  fixes p :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infix ".." 50)
locale constraint1
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
  assumes "constraint1(( ** ))"
locale constraint1
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
  assumes "constraint1(( ** ))"
  notes
    "constraint1_axioms" = (\<open>constraint1(( ** ))\<close>)
      ["attribute" "<attribute>"]
  notes "l_id" = \<open>?x ** ?y = ?x\<close>
  notes "assoc" = \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)\<close>
locale constraint2
  fixes p :: "'a" 
    and q :: "'a" 
  assumes "constraint2(p, q)"
locale constraint2
  fixes p :: "'a" 
    and q :: "'a" 
  assumes "constraint2(p, q)"
  notes
    "constraint2_axioms" = (\<open>constraint2(p, q)\<close>)
      ["attribute" "<attribute>"]
locale semi
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
  assumes "semi(( ** ))"
locale semi
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
  assumes "semi(( ** ))"
  notes
    "semi_axioms" = (\<open>semi(( ** ))\<close>)
      ["attribute" "<attribute>"]
  notes "assoc" = \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)\<close>
semi(?prod) \<equiv>
\<forall>x y z. ?prod(?prod(x, y), z) = ?prod(x, ?prod(y, z))
locale lgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "lgrp(( ** ), one, inv)"
locale lgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "lgrp(( ** ), one, inv)"
  notes
    "semi_axioms" = (\<open>semi(( ** ))\<close>)
      ["attribute" "<attribute>"]
  notes "assoc" = \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)\<close>
  notes
    "lgrp_axioms" = (\<open>lgrp(( ** ), one, inv)\<close>)
      ["attribute" "<attribute>"]
  notes "lone" = \<open>one ** ?x = ?x\<close>
  notes "linv" = \<open>inv(?x) ** ?x = one\<close>
lgrp(?prod, ?one, ?inv) \<equiv>
semi(?prod) \<and> lgrp_axioms(?prod, ?one, ?inv)
lgrp_axioms(?prod, ?one, ?inv) \<equiv>
(\<forall>x. ?prod(?one, x) = x) \<and>
(\<forall>x. ?prod(?inv(x), x) = ?one)
locale add_lgrp
  fixes sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "++" 60)
    and zero :: "'a" 
    and neg :: "'a \<Rightarrow> 'a" 
  assumes "add_lgrp((++), zero, neg)"
locale add_lgrp
  fixes sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "++" 60)
    and zero :: "'a" 
    and neg :: "'a \<Rightarrow> 'a" 
  assumes "add_lgrp((++), zero, neg)"
  notes
    "semi_axioms" = (\<open>semi((++))\<close>) ["attribute" "<attribute>"]
  notes "assoc" = \<open>?x ++ ?y ++ ?z = ?x ++ (?y ++ ?z)\<close>
  notes
    "add_lgrp_axioms" = (\<open>add_lgrp((++), zero, neg)\<close>)
      ["attribute" "<attribute>"]
  notes "lzero" = \<open>zero ++ ?x = ?x\<close>
  notes "lneg" = \<open>neg(?x) ++ ?x = zero\<close>
add_lgrp(?sum, ?zero, ?neg) \<equiv>
semi(?sum) \<and> add_lgrp_axioms(?sum, ?zero, ?neg)
add_lgrp_axioms(?sum, ?zero, ?neg) \<equiv>
(\<forall>x. ?sum(?zero, x) = x) \<and>
(\<forall>x. ?sum(?neg(x), x) = ?zero)
locale rev_lgrp
  fixes sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "++" 60)
  assumes "rev_lgrp((++))"
locale rev_lgrp
  fixes sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "++" 60)
  assumes "rev_lgrp((++))"
  notes
    "semi_axioms" = (\<open>semi(\<lambda>x y. y ++ x)\<close>)
      ["attribute" "<attribute>"]
  notes "assoc" = \<open>?z ++ (?y ++ ?x) = ?z ++ ?y ++ ?x\<close>
  notes
    "rev_lgrp_axioms" = (\<open>rev_lgrp((++))\<close>)
      ["attribute" "<attribute>"]
rev_lgrp(?sum) \<equiv> semi(\<lambda>x y. ?sum(y, x))
locale hom
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
    and g :: "'b \<Rightarrow> 'b \<Rightarrow> 'b" 
  assumes "hom(f, g)"
locale hom
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
    and g :: "'b \<Rightarrow> 'b \<Rightarrow> 'b" 
  assumes "hom(f, g)"
  notes
    "f.semi_axioms" = (\<open>semi(f)\<close>) ["attribute" "<attribute>"]
  notes "f.assoc" = \<open>f(f(?x, ?y), ?z) = f(?x, f(?y, ?z))\<close>
  notes
    "g.semi_axioms" = (\<open>semi(g)\<close>) ["attribute" "<attribute>"]
  notes "g.assoc" = \<open>g(g(?x, ?y), ?z) = g(?x, g(?y, ?z))\<close>
  notes
    "hom_axioms" = (\<open>hom(f, g)\<close>) ["attribute" "<attribute>"]
hom(?f, ?g) \<equiv> semi(?f) \<and> semi(?g)
locale perturbation
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and delta :: "'a \<Rightarrow> 'a" 
  assumes "perturbation(( ** ), delta)"
locale perturbation
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and delta :: "'a \<Rightarrow> 'a" 
  assumes "perturbation(( ** ), delta)"
  notes
    "semi_axioms" = (\<open>semi(( ** ))\<close>)
      ["attribute" "<attribute>"]
  notes "assoc" = \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)\<close>
  notes
    "d.semi_axioms" =
      (\<open>semi(\<lambda>x y. delta(x) ** delta(y))\<close>)
      ["attribute" "<attribute>"]
  notes
    "d.assoc" =
      \<open>delta(delta(?x) ** delta(?y)) ** delta(?z) =
             delta(?x) ** delta(delta(?y) ** delta(?z))\<close>
  notes
    "perturbation_axioms" = (\<open>perturbation(( ** ), delta)\<close>)
      ["attribute" "<attribute>"]
perturbation(?prod, ?delta) \<equiv>
semi(?prod) \<and> semi(\<lambda>x y. ?prod(?delta(x), ?delta(y)))
locale pert_hom
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
    and d1 :: "'a \<Rightarrow> 'a" 
    and d2 :: "'a \<Rightarrow> 'a" 
  assumes "pert_hom(f, d1, d2)"
locale pert_hom
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
    and d1 :: "'a \<Rightarrow> 'a" 
    and d2 :: "'a \<Rightarrow> 'a" 
  assumes "pert_hom(f, d1, d2)"
  notes
    "d1.semi_axioms" = (\<open>semi(f)\<close>) ["attribute" "<attribute>"]
  notes "d1.assoc" = \<open>f(f(?x, ?y), ?z) = f(?x, f(?y, ?z))\<close>
  notes
    "d1.d.semi_axioms" =
      (\<open>semi(\<lambda>x y. f(d1(x), d1(y)))\<close>)
      ["attribute" "<attribute>"]
  notes
    "d1.d.assoc" =
      \<open>f(d1(f(d1(?x), d1(?y))), d1(?z)) =
             f(d1(?x), d1(f(d1(?y), d1(?z))))\<close>
  notes
    "d1.perturbation_axioms" = (\<open>perturbation(f, d1)\<close>)
      ["attribute" "<attribute>"]
  notes
    "d2.d.semi_axioms" =
      (\<open>semi(\<lambda>x y. f(d2(x), d2(y)))\<close>)
      ["attribute" "<attribute>"]
  notes
    "d2.d.assoc" =
      \<open>f(d2(f(d2(?x), d2(?y))), d2(?z)) =
             f(d2(?x), d2(f(d2(?y), d2(?z))))\<close>
  notes
    "d2.perturbation_axioms" = (\<open>perturbation(f, d2)\<close>)
      ["attribute" "<attribute>"]
  notes
    "pert_hom_axioms" = (\<open>pert_hom(f, d1, d2)\<close>)
      ["attribute" "<attribute>"]
pert_hom(?f, ?d1.0, ?d2.0) \<equiv>
perturbation(?f, ?d1.0) \<and> perturbation(?f, ?d2.0)
locale pert_hom'
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
    and d1 :: "'a \<Rightarrow> 'a" 
    and d2 :: "'a \<Rightarrow> 'a" 
  assumes "pert_hom'(f, d1, d2)"
locale pert_hom'
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
    and d1 :: "'a \<Rightarrow> 'a" 
    and d2 :: "'a \<Rightarrow> 'a" 
  assumes "pert_hom'(f, d1, d2)"
  notes "semi_axioms" = (\<open>semi(f)\<close>) ["attribute" "<attribute>"]
  notes "assoc" = \<open>f(f(?x, ?y), ?z) = f(?x, f(?y, ?z))\<close>
  notes
    "d1.d.semi_axioms" =
      (\<open>semi(\<lambda>x y. f(d1(x), d1(y)))\<close>)
      ["attribute" "<attribute>"]
  notes
    "d1.d.assoc" =
      \<open>f(d1(f(d1(?x), d1(?y))), d1(?z)) =
             f(d1(?x), d1(f(d1(?y), d1(?z))))\<close>
  notes
    "d1.perturbation_axioms" = (\<open>perturbation(f, d1)\<close>)
      ["attribute" "<attribute>"]
  notes
    "d2.d.semi_axioms" =
      (\<open>semi(\<lambda>x y. f(d2(x), d2(y)))\<close>)
      ["attribute" "<attribute>"]
  notes
    "d2.d.assoc" =
      \<open>f(d2(f(d2(?x), d2(?y))), d2(?z)) =
             f(d2(?x), d2(f(d2(?y), d2(?z))))\<close>
  notes
    "d2.perturbation_axioms" = (\<open>perturbation(f, d2)\<close>)
      ["attribute" "<attribute>"]
  notes
    "pert_hom'_axioms" = (\<open>pert_hom'(f, d1, d2)\<close>)
      ["attribute" "<attribute>"]
pert_hom'(?f, ?d1.0, ?d2.0) \<equiv>
semi(?f) \<and> perturbation(?f, ?d1.0) \<and> perturbation(?f, ?d2.0)
locale logic
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "logic((&&), lnot)"
locale logic
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "logic((&&), lnot)"
  notes
    "logic_axioms" = (\<open>logic((&&), lnot)\<close>)
      ["attribute" "<attribute>"]
  notes "assoc" = \<open>?x && ?y && ?z = ?x && (?y && ?z)\<close>
  notes "notnot" = \<open>-- -- ?x = ?x\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes "lor_def" = \<open>?x || ?y = -- (-- ?x && -- ?y)\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
locale use_decl
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "use_decl((&&), lnot)"
locale extra_type
  fixes a :: "'a" 
    and P :: "'a \<Rightarrow> 'b \<Rightarrow> o" 
locale use_decl
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "use_decl((&&), lnot)"
  notes
    "l.logic_axioms" = (\<open>logic((&&), lnot)\<close>)
      ["attribute" "<attribute>"]
  notes "l.assoc" = \<open>?x && ?y && ?z = ?x && (?y && ?z)\<close>
  notes "l.notnot" = \<open>-- -- ?x = ?x\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes "l.lor_def" = \<open>?x || ?y = -- (-- ?x && -- ?y)\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "semi_axioms" = (\<open>semi((||))\<close>) ["attribute" "<attribute>"]
  notes "assoc" = \<open>?x || ?y || ?z = (?x || (?y || ?z))\<close>
  notes
    "use_decl_axioms" = (\<open>use_decl((&&), lnot)\<close>)
      ["attribute" "<attribute>"]
use_decl(?land, ?lnot) \<equiv>
logic(?land, ?lnot) \<and> semi(logic.lor(?land, ?lnot))
"extra_type.test"
  :: "('a \<Rightarrow> 'b \<Rightarrow> o)
      \<Rightarrow> 'a \<Rightarrow> o"
extra_type.test(?P, ?x) \<longleftrightarrow> (\<forall>b. ?P(?x, b))
extra_type.test(\<lambda>x y. x = 0, ?x) \<longleftrightarrow>
(\<forall>b. ?x = 0)
val check_syntax = fn: Proof.context -> thm -> string -> unit
locale syntax
  fixes p1 :: "'a \<Rightarrow> 'b" 
    and p2 :: "'b \<Rightarrow> o" 
D1(?x) \<longleftrightarrow> \<not> p2(p1(?x))
D2(?x) \<longleftrightarrow> \<not> p2(?x)
syntax.d1(?p1.0, ?p2.0, ?x) \<longleftrightarrow> \<not> ?p2.0(?p1.0(?x))
syntax.d2(?p2.0, ?x) \<longleftrightarrow> \<not> ?p2.0(?x)
locale syntax'
  fixes p1 :: "'a \<Rightarrow> 'a" 
    and p2 :: "'a \<Rightarrow> o" 
D1(?x) \<longleftrightarrow> \<not> p2(p1(?x))
D2(?x) \<longleftrightarrow> \<not> p2(?x)
val it = (): unit
val it = (): unit
locale syntax''
  fixes p3 :: "'a \<Rightarrow> 'b" 
    and p2 :: "'b \<Rightarrow> o" 
d1(?x) \<longleftrightarrow> \<not> p2(p3(?x))
D2(?x) \<longleftrightarrow> \<not> p2(?x)
val it = (): unit
val it = (): unit
logic(?land, ?lnot) \<Longrightarrow>
?land(?land(?x, ?y), ?z) = ?land(?x, ?land(?y, ?z))
logic(?land, ?lnot) \<Longrightarrow>
logic.lor(?land, ?lnot, ?x, ?y) = ?lnot(?land(?lnot(?x), ?lnot(?y)))
locale logic_def
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "||" 50)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "logic_def((&&), lnot)"
  defines "\<And>x y. x || y \<equiv> -- (-- x && -- y)"
?x || ?y \<equiv> -- (-- ?x && -- ?y)
  [\<And>x y. x || y \<equiv> -- (-- x && -- y), logic_def((&&), lnot)]
locale logic_def2
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "||" 50)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "logic_def2((&&), lnot)"
  defines "\<And>x y. x || y \<equiv> -- (-- x && -- y)"
locale semi_hom_loc
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
    and sum :: "'b \<Rightarrow> 'b \<Rightarrow> 'b" 
    and h :: "'a \<Rightarrow> 'b" 
  assumes "semi_hom_loc(prod, sum, h)"
\<lbrakk>semi_hom_loc(?proda, ?suma, ?ha);
 semi_hom(?prod, ?sum, ?h)\<rbrakk>
\<Longrightarrow> ?h(?prod(?x, ?y)) = ?sum(?h(?x), ?h(?y))
locale rgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "rgrp(( ** ), one, inv)"
locale lgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "lgrp(( ** ), one, inv)"
  notes
    "semi_axioms" = (\<open>semi(( ** ))  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "assoc" =
      \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)
               [lgrp(( ** ), one, inv)]\<close>
  notes
    "lgrp_axioms" =
      (\<open>lgrp(( ** ), one, inv)  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes "lone" = \<open>one ** ?x = ?x  [lgrp(( ** ), one, inv)]\<close>
  notes
    "linv" = \<open>inv(?x) ** ?x = one  [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "lcancel" =
      \<open>?x ** ?y = ?x ** ?z \<longleftrightarrow> ?y = ?z
               [lgrp(( ** ), one, inv)]\<close>
locale rgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "rgrp(( ** ), one, inv)"
  notes
    "semi_axioms" = (\<open>semi(( ** ))  [rgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "assoc" =
      \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)
               [rgrp(( ** ), one, inv)]\<close>
  notes
    "rgrp_axioms" =
      (\<open>rgrp(( ** ), one, inv)  [rgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes "rone" = \<open>?x ** one = ?x  [rgrp(( ** ), one, inv)]\<close>
  notes
    "rinv" = \<open>?x ** inv(?x) = one  [rgrp(( ** ), one, inv)]\<close>
  notes theorem
    "rcancel" =
      \<open>?y ** ?x = ?z ** ?x \<longleftrightarrow> ?y = ?z
               [rgrp(( ** ), one, inv)]\<close>
locale order
  fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "<<" 50)
  assumes "order((<<))"
locale order'
  fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "<<" 50)
  assumes "order'((<<))"
locale order_with_def
  fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "<<" 50)
  assumes "order_with_def((<<))"
locale lgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "lgrp(( ** ), one, inv)"
  notes
    "semi_axioms" = (\<open>semi(( ** ))  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "assoc" =
      \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)
               [lgrp(( ** ), one, inv)]\<close>
  notes
    "right.rgrp_axioms" =
      (\<open>rgrp(( ** ), one, inv)  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "right.rone" = \<open>?x ** one = ?x  [lgrp(( ** ), one, inv)]\<close>
  notes
    "right.rinv" =
      \<open>?x ** inv(?x) = one  [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "right.rcancel" =
      \<open>?y ** ?x = ?z ** ?x \<longleftrightarrow> ?y = ?z
               [lgrp(( ** ), one, inv)]\<close>
  notes
    "lgrp_axioms" =
      (\<open>lgrp(( ** ), one, inv)  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes "lone" = \<open>one ** ?x = ?x  [lgrp(( ** ), one, inv)]\<close>
  notes
    "linv" = \<open>inv(?x) ** ?x = one  [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "lcancel" =
      \<open>?x ** ?y = ?x ** ?z \<longleftrightarrow> ?y = ?z
               [lgrp(( ** ), one, inv)]\<close>
locale A5
  fixes A :: "o" 
    and B :: "o" 
    and C :: "o" 
    and D :: "o" 
    and E :: "o" 
  assumes "A5(A, B, C, D, E)"
locale rgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "rgrp(( ** ), one, inv)"
  notes
    "semi_axioms" = (\<open>semi(( ** ))  [rgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "assoc" =
      \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)
               [rgrp(( ** ), one, inv)]\<close>
  notes
    "left.lgrp_axioms" =
      (\<open>lgrp(( ** ), one, inv)  [rgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "left.lone" = \<open>one ** ?x = ?x  [rgrp(( ** ), one, inv)]\<close>
  notes
    "left.linv" =
      \<open>inv(?x) ** ?x = one  [rgrp(( ** ), one, inv)]\<close>
  notes theorem
    "left.lcancel" =
      \<open>?x ** ?y = ?x ** ?z \<longleftrightarrow> ?y = ?z
               [rgrp(( ** ), one, inv)]\<close>
  notes
    "rgrp_axioms" =
      (\<open>rgrp(( ** ), one, inv)  [rgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes "rone" = \<open>?x ** one = ?x  [rgrp(( ** ), one, inv)]\<close>
  notes
    "rinv" = \<open>?x ** inv(?x) = one  [rgrp(( ** ), one, inv)]\<close>
  notes theorem
    "rcancel" =
      \<open>?y ** ?x = ?z ** ?x \<longleftrightarrow> ?y = ?z
               [rgrp(( ** ), one, inv)]\<close>
locale lgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "lgrp(( ** ), one, inv)"
  notes
    "semi_axioms" = (\<open>semi(( ** ))  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "assoc" =
      \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)
               [lgrp(( ** ), one, inv)]\<close>
  notes
    "right.rgrp_axioms" =
      (\<open>rgrp(( ** ), one, inv)  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "right.rone" = \<open>?x ** one = ?x  [lgrp(( ** ), one, inv)]\<close>
  notes
    "right.rinv" =
      \<open>?x ** inv(?x) = one  [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "right.rcancel" =
      \<open>?y ** ?x = ?z ** ?x \<longleftrightarrow> ?y = ?z
               [lgrp(( ** ), one, inv)]\<close>
  notes
    "lgrp_axioms" =
      (\<open>lgrp(( ** ), one, inv)  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes "lone" = \<open>one ** ?x = ?x  [lgrp(( ** ), one, inv)]\<close>
  notes
    "linv" = \<open>inv(?x) ** ?x = one  [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "lcancel" =
      \<open>?x ** ?y = ?x ** ?z \<longleftrightarrow> ?y = ?z
               [lgrp(( ** ), one, inv)]\<close>
locale order
  fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "<<" 50)
  assumes "order((<<))"
  notes
    "dual.order_axioms" =
      (\<open>order(\<lambda>x y. y << x)  [order((<<))]\<close>)
      ["attribute" "<attribute>"]
  notes "dual.refl" = \<open>?x << ?x  [order((<<))]\<close>
  notes
    "dual.trans" =
      \<open>\<lbrakk>?y << ?x; ?z << ?y\<rbrakk> \<Longrightarrow> ?z << ?x
               [order((<<))]\<close>
  notes
    "order_axioms" = (\<open>order((<<))  [order((<<))]\<close>)
      ["attribute" "<attribute>"]
  notes "refl" = \<open>?x << ?x  [order((<<))]\<close>
  notes
    "trans" =
      \<open>\<lbrakk>?x << ?y; ?y << ?z\<rbrakk> \<Longrightarrow> ?x << ?z
               [order((<<))]\<close>
local facts:
  assoc: ?x ** ?y ** ?z = ?x ** (?y ** ?z)  [lgrp(( ** ), one, inv)]
  lcancel:
    ?x ** ?y = ?x ** ?z \<longleftrightarrow> ?y = ?z
      [lgrp(( ** ), one, inv)]
  lgrp_axioms: lgrp(( ** ), one, inv)  [lgrp(( ** ), one, inv)]
  linv: inv(?x) ** ?x = one  [lgrp(( ** ), one, inv)]
  lone: one ** ?x = ?x  [lgrp(( ** ), one, inv)]
  semi_axioms: semi(( ** ))  [lgrp(( ** ), one, inv)]
locale order_with_def
  fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "<<" 50)
  assumes "order_with_def((<<))"
  notes
    "order'_axioms" = (\<open>order'((<<))  [order_with_def((<<))]\<close>)
      ["attribute" "<attribute>"]
  notes "refl" = \<open>?x << ?x  [order_with_def((<<))]\<close>
  notes
    "trans" =
      \<open>\<lbrakk>?x << ?y; ?y << ?z\<rbrakk> \<Longrightarrow> ?x << ?z
               [order_with_def((<<))]\<close>
  notes
    "dual.order'_axioms" =
      (\<open>order'((>>))  [order_with_def((<<))]\<close>)
      ["attribute" "<attribute>"]
  notes "dual.refl" = \<open>?x >> ?x  [order_with_def((<<))]\<close>
  notes
    "dual.trans" =
      \<open>\<lbrakk>?x >> ?y; ?y >> ?z\<rbrakk> \<Longrightarrow> ?x >> ?z
               [order_with_def((<<))]\<close>
  notes
    "order_with_def_axioms" =
      (\<open>order_with_def((<<))  [order_with_def((<<))]\<close>)
      ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "greater_def" =
      \<open>?x >> ?y \<longleftrightarrow> ?y << ?x
               [order_with_def((<<))]\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
local facts:
  A5_axioms: A5(A, B, C, D, E)  [A5(A, B, C, D, E)]
  eq: A \<longleftrightarrow>
      B \<longleftrightarrow>
      C \<longleftrightarrow> D \<longleftrightarrow> E
        [A5(A, B, C, D, E)]
local facts:
  1.1.A5_axioms: A5(A, B, E, C, D)  [A5(A, B, C, D, E)]
  1.1.eq:
    A \<longleftrightarrow>
    B \<longleftrightarrow>
    E \<longleftrightarrow> C \<longleftrightarrow> D
      [A5(A, B, C, D, E)]
  1.A5_axioms: A5(A, B, D, E, C)  [A5(A, B, C, D, E)]
  1.eq:
    A \<longleftrightarrow>
    B \<longleftrightarrow>
    D \<longleftrightarrow> E \<longleftrightarrow> C
      [A5(A, B, C, D, E)]
  A5_axioms: A5(A, B, C, D, E)  [A5(A, B, C, D, E)]
  eq: A \<longleftrightarrow>
      B \<longleftrightarrow>
      C \<longleftrightarrow> D \<longleftrightarrow> E
        [A5(A, B, C, D, E)]
local facts:
  1.1.2.1.1.A5_axioms: A5(E, B, A, D, C)  [A5(A, B, C, D, E)]
  1.1.2.1.1.eq:
    E \<longleftrightarrow>
    B \<longleftrightarrow>
    A \<longleftrightarrow> D \<longleftrightarrow> C
      [A5(A, B, C, D, E)]
  1.1.2.1.2.1.1.A5_axioms: A5(C, B, E, D, A)  [A5(A, B, C, D, E)]
  1.1.2.1.2.1.1.eq:
    C \<longleftrightarrow>
    B \<longleftrightarrow>
    E \<longleftrightarrow> D \<longleftrightarrow> A
      [A5(A, B, C, D, E)]
  1.1.2.1.2.1.A5_axioms: A5(C, B, A, E, D)  [A5(A, B, C, D, E)]
  1.1.2.1.2.1.eq:
    C \<longleftrightarrow>
    B \<longleftrightarrow>
    A \<longleftrightarrow> E \<longleftrightarrow> D
      [A5(A, B, C, D, E)]
  1.1.2.1.2.2.1.1.A5_axioms: A5(D, B, C, E, A)  [A5(A, B, C, D, E)]
  1.1.2.1.2.2.1.1.eq:
    D \<longleftrightarrow>
    B \<longleftrightarrow>
    C \<longleftrightarrow> E \<longleftrightarrow> A
      [A5(A, B, C, D, E)]
  1.1.2.1.2.2.1.A5_axioms: A5(D, B, A, C, E)  [A5(A, B, C, D, E)]
  1.1.2.1.2.2.1.eq:
    D \<longleftrightarrow>
    B \<longleftrightarrow>
    A \<longleftrightarrow> C \<longleftrightarrow> E
      [A5(A, B, C, D, E)]
  1.1.2.1.2.2.A5_axioms: A5(D, B, E, A, C)  [A5(A, B, C, D, E)]
  1.1.2.1.2.2.eq:
    D \<longleftrightarrow>
    B \<longleftrightarrow>
    E \<longleftrightarrow> A \<longleftrightarrow> C
      [A5(A, B, C, D, E)]
  1.1.2.1.2.A5_axioms: A5(C, B, D, A, E)  [A5(A, B, C, D, E)]
  1.1.2.1.2.eq:
    C \<longleftrightarrow>
    B \<longleftrightarrow>
    D \<longleftrightarrow> A \<longleftrightarrow> E
      [A5(A, B, C, D, E)]
  1.1.2.1.A5_axioms: A5(E, B, C, A, D)  [A5(A, B, C, D, E)]
  1.1.2.1.eq:
    E \<longleftrightarrow>
    B \<longleftrightarrow>
    C \<longleftrightarrow> A \<longleftrightarrow> D
      [A5(A, B, C, D, E)]
  1.1.2.A5_axioms: A5(E, B, D, C, A)  [A5(A, B, C, D, E)]
  1.1.2.eq:
    E \<longleftrightarrow>
    B \<longleftrightarrow>
    D \<longleftrightarrow> C \<longleftrightarrow> A
      [A5(A, B, C, D, E)]
  1.1.A5_axioms: A5(A, B, E, C, D)  [A5(A, B, C, D, E)]
  1.1.eq:
    A \<longleftrightarrow>
    B \<longleftrightarrow>
    E \<longleftrightarrow> C \<longleftrightarrow> D
      [A5(A, B, C, D, E)]
  1.A5_axioms: A5(A, B, D, E, C)  [A5(A, B, C, D, E)]
  1.eq:
    A \<longleftrightarrow>
    B \<longleftrightarrow>
    D \<longleftrightarrow> E \<longleftrightarrow> C
      [A5(A, B, C, D, E)]
  A5_axioms: A5(A, B, C, D, E)  [A5(A, B, C, D, E)]
  eq: A \<longleftrightarrow>
      B \<longleftrightarrow>
      C \<longleftrightarrow> D \<longleftrightarrow> E
        [A5(A, B, C, D, E)]
locale trivial
  fixes P :: "o" 
    and Q :: "o" 
  assumes "trivial(P, Q)"
locale trivial
  fixes P :: "o" 
    and Q :: "o" 
  assumes "trivial(P, Q)"
val it = []: thm list
locale logic2
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "logic2((&&), lnot)"
locale logic_a
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "logic_a((&&), lnot)"
locale logic_b
  fixes land :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "&&" 55)
    and lnot :: "'a \<Rightarrow> 'a"   ("-- _" [60] 60)
  assumes "logic_b((&&), lnot)"
locale logic_o
  fixes land :: "o \<Rightarrow> o \<Rightarrow> o"   (infixl "&&" 55)
    and lnot :: "o \<Rightarrow> o"   ("-- _" [60] 60)
  assumes "PROP logic_o((&&), lnot)"
locale reflexive
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "reflexive((\<sqsubseteq>))"
locale mixin
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin((\<sqsubseteq>))"
locale mixin2
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin2((\<sqsubseteq>))"
locale mixin3
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin3((\<sqsubseteq>))"
locale mixin4_base
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin4_base((\<sqsubseteq>))"
locale mixin4_mixin
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin4_mixin((\<sqsubseteq>))"
locale mixin4_copy
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin4_copy((\<sqsubseteq>))"
locale A5
  fixes A :: "o" 
    and B :: "o" 
    and C :: "o" 
    and D :: "o" 
    and E :: "o" 
  assumes "A5(A, B, C, D, E)"
  notes
    "1.1.2.1.1.3.1.1.2.1.1.A5_axioms" =
      (\<open>A5(C, A, B, D, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.1.eq" =
      \<open>C \<longleftrightarrow>
             A \<longleftrightarrow>
             B \<longleftrightarrow> D \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.1.A5_axioms" =
      (\<open>A5(B, C, A, D, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.1.eq" =
      \<open>B \<longleftrightarrow>
             C \<longleftrightarrow>
             A \<longleftrightarrow> D \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.A5_axioms" =
      (\<open>A5(C, B, A, E, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.eq" =
      \<open>C \<longleftrightarrow>
             B \<longleftrightarrow>
             A \<longleftrightarrow> E \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.1.1.A5_axioms" =
      (\<open>A5(D, B, C, E, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.1.1.eq" =
      \<open>D \<longleftrightarrow>
             B \<longleftrightarrow>
             C \<longleftrightarrow> E \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.1.A5_axioms" =
      (\<open>A5(D, B, A, C, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.1.eq" =
      \<open>D \<longleftrightarrow>
             B \<longleftrightarrow>
             A \<longleftrightarrow> C \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.1.A5_axioms" =
      (\<open>A5(C, E, B, A, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.1.eq" =
      \<open>C \<longleftrightarrow>
             E \<longleftrightarrow>
             B \<longleftrightarrow> A \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.1.1.A5_axioms" =
      (\<open>A5(D, E, C, A, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.1.1.eq" =
      \<open>D \<longleftrightarrow>
             E \<longleftrightarrow>
             C \<longleftrightarrow> A \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.1.A5_axioms" =
      (\<open>A5(D, E, B, C, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.1.eq" =
      \<open>D \<longleftrightarrow>
             E \<longleftrightarrow>
             B \<longleftrightarrow> C \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.1.A5_axioms" =
      (\<open>A5(B, D, E, C, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.1.eq" =
      \<open>B \<longleftrightarrow>
             D \<longleftrightarrow>
             E \<longleftrightarrow> C \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.1.1.A5_axioms" =
      (\<open>A5(A, D, B, C, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.1.1.eq" =
      \<open>A \<longleftrightarrow>
             D \<longleftrightarrow>
             B \<longleftrightarrow> C \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.1.A5_axioms" =
      (\<open>A5(A, D, E, B, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.1.eq" =
      \<open>A \<longleftrightarrow>
             D \<longleftrightarrow>
             E \<longleftrightarrow> B \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.1.3.1.1.A5_axioms" =
      (\<open>A5(D, A, E, C, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.1.3.1.1.eq" =
      \<open>D \<longleftrightarrow>
             A \<longleftrightarrow>
             E \<longleftrightarrow> C \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.1.3.1.A5_axioms" =
      (\<open>A5(D, A, B, E, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.1.3.1.eq" =
      \<open>D \<longleftrightarrow>
             A \<longleftrightarrow>
             B \<longleftrightarrow> E \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.1.3.A5_axioms" =
      (\<open>A5(D, A, C, B, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.1.3.eq" =
      \<open>D \<longleftrightarrow>
             A \<longleftrightarrow>
             C \<longleftrightarrow> B \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.1.A5_axioms" =
      (\<open>A5(C, D, A, B, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.1.eq" =
      \<open>C \<longleftrightarrow>
             D \<longleftrightarrow>
             A \<longleftrightarrow> B \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.A5_axioms" =
      (\<open>A5(C, D, E, A, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.1.eq" =
      \<open>C \<longleftrightarrow>
             D \<longleftrightarrow>
             E \<longleftrightarrow> A \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.A5_axioms" =
      (\<open>A5(C, D, B, E, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.2.eq" =
      \<open>C \<longleftrightarrow>
             D \<longleftrightarrow>
             B \<longleftrightarrow> E \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.3.1.1.A5_axioms" =
      (\<open>A5(D, C, B, A, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.3.1.1.eq" =
      \<open>D \<longleftrightarrow>
             C \<longleftrightarrow>
             B \<longleftrightarrow> A \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.3.1.A5_axioms" =
      (\<open>A5(D, C, E, B, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.3.1.eq" =
      \<open>D \<longleftrightarrow>
             C \<longleftrightarrow>
             E \<longleftrightarrow> B \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.3.A5_axioms" =
      (\<open>A5(D, C, A, E, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.3.eq" =
      \<open>D \<longleftrightarrow>
             C \<longleftrightarrow>
             A \<longleftrightarrow> E \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.A5_axioms" =
      (\<open>A5(A, D, C, E, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.2.eq" =
      \<open>A \<longleftrightarrow>
             D \<longleftrightarrow>
             C \<longleftrightarrow> E \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.A5_axioms" =
      (\<open>A5(B, D, A, E, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.1.eq" =
      \<open>B \<longleftrightarrow>
             D \<longleftrightarrow>
             A \<longleftrightarrow> E \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.A5_axioms" =
      (\<open>A5(B, D, C, A, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.2.eq" =
      \<open>B \<longleftrightarrow>
             D \<longleftrightarrow>
             C \<longleftrightarrow> A \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.A5_axioms" =
      (\<open>A5(E, D, B, A, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.1.eq" =
      \<open>E \<longleftrightarrow>
             D \<longleftrightarrow>
             B \<longleftrightarrow> A \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.A5_axioms" =
      (\<open>A5(E, D, C, B, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.1.eq" =
      \<open>E \<longleftrightarrow>
             D \<longleftrightarrow>
             C \<longleftrightarrow> B \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.A5_axioms" =
      (\<open>A5(E, D, A, C, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.3.eq" =
      \<open>E \<longleftrightarrow>
             D \<longleftrightarrow>
             A \<longleftrightarrow> C \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.A5_axioms" =
      (\<open>A5(A, E, D, C, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.1.eq" =
      \<open>A \<longleftrightarrow>
             E \<longleftrightarrow>
             D \<longleftrightarrow> C \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.A5_axioms" =
      (\<open>A5(A, E, B, D, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.1.eq" =
      \<open>A \<longleftrightarrow>
             E \<longleftrightarrow>
             B \<longleftrightarrow> D \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.A5_axioms" =
      (\<open>A5(A, E, C, B, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.2.eq" =
      \<open>A \<longleftrightarrow>
             E \<longleftrightarrow>
             C \<longleftrightarrow> B \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.A5_axioms" =
      (\<open>A5(D, E, A, B, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.2.eq" =
      \<open>D \<longleftrightarrow>
             E \<longleftrightarrow>
             A \<longleftrightarrow> B \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.A5_axioms" =
      (\<open>A5(C, E, D, B, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.1.eq" =
      \<open>C \<longleftrightarrow>
             E \<longleftrightarrow>
             D \<longleftrightarrow> B \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.A5_axioms" =
      (\<open>A5(C, E, A, D, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.2.eq" =
      \<open>C \<longleftrightarrow>
             E \<longleftrightarrow>
             A \<longleftrightarrow> D \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.A5_axioms" =
      (\<open>A5(B, E, C, D, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.1.eq" =
      \<open>B \<longleftrightarrow>
             E \<longleftrightarrow>
             C \<longleftrightarrow> D \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.A5_axioms" =
      (\<open>A5(B, E, A, C, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.1.eq" =
      \<open>B \<longleftrightarrow>
             E \<longleftrightarrow>
             A \<longleftrightarrow> C \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.A5_axioms" =
      (\<open>A5(B, E, D, A, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.3.eq" =
      \<open>B \<longleftrightarrow>
             E \<longleftrightarrow>
             D \<longleftrightarrow> A \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.A5_axioms" =
      (\<open>A5(D, B, E, A, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.2.eq" =
      \<open>D \<longleftrightarrow>
             B \<longleftrightarrow>
             E \<longleftrightarrow> A \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.A5_axioms" =
      (\<open>A5(C, B, D, A, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.1.eq" =
      \<open>C \<longleftrightarrow>
             B \<longleftrightarrow>
             D \<longleftrightarrow> A \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.A5_axioms" =
      (\<open>A5(C, B, E, D, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.3.eq" =
      \<open>C \<longleftrightarrow>
             B \<longleftrightarrow>
             E \<longleftrightarrow> D \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.A5_axioms" =
      (\<open>A5(E, C, B, D, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.1.eq" =
      \<open>E \<longleftrightarrow>
             C \<longleftrightarrow>
             B \<longleftrightarrow> D \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.A5_axioms" =
      (\<open>A5(E, C, A, B, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.1.eq" =
      \<open>E \<longleftrightarrow>
             C \<longleftrightarrow>
             A \<longleftrightarrow> B \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.A5_axioms" =
      (\<open>A5(E, C, D, A, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.2.eq" =
      \<open>E \<longleftrightarrow>
             C \<longleftrightarrow>
             D \<longleftrightarrow> A \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.A5_axioms" =
      (\<open>A5(B, C, E, A, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.1.eq" =
      \<open>B \<longleftrightarrow>
             C \<longleftrightarrow>
             E \<longleftrightarrow> A \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.A5_axioms" =
      (\<open>A5(B, C, D, E, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.2.eq" =
      \<open>B \<longleftrightarrow>
             C \<longleftrightarrow>
             D \<longleftrightarrow> E \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.A5_axioms" =
      (\<open>A5(A, C, B, E, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.1.eq" =
      \<open>A \<longleftrightarrow>
             C \<longleftrightarrow>
             B \<longleftrightarrow> E \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.A5_axioms" =
      (\<open>A5(A, C, D, B, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.1.eq" =
      \<open>A \<longleftrightarrow>
             C \<longleftrightarrow>
             D \<longleftrightarrow> B \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.A5_axioms" =
      (\<open>A5(A, C, E, D, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.3.eq" =
      \<open>A \<longleftrightarrow>
             C \<longleftrightarrow>
             E \<longleftrightarrow> D \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.A5_axioms" =
      (\<open>A5(E, A, C, D, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.1.eq" =
      \<open>E \<longleftrightarrow>
             A \<longleftrightarrow>
             C \<longleftrightarrow> D \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.A5_axioms" =
      (\<open>A5(E, A, B, C, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.1.eq" =
      \<open>E \<longleftrightarrow>
             A \<longleftrightarrow>
             B \<longleftrightarrow> C \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.2.A5_axioms" =
      (\<open>A5(E, A, D, B, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.2.eq" =
      \<open>E \<longleftrightarrow>
             A \<longleftrightarrow>
             D \<longleftrightarrow> B \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.1.A5_axioms" =
      (\<open>A5(C, A, E, B, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.1.eq" =
      \<open>C \<longleftrightarrow>
             A \<longleftrightarrow>
             E \<longleftrightarrow> B \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.2.A5_axioms" =
      (\<open>A5(C, A, D, E, B)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.2.eq" =
      \<open>C \<longleftrightarrow>
             A \<longleftrightarrow>
             D \<longleftrightarrow> E \<longleftrightarrow> B
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.1.A5_axioms" =
      (\<open>A5(B, A, C, E, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.1.eq" =
      \<open>B \<longleftrightarrow>
             A \<longleftrightarrow>
             C \<longleftrightarrow> E \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.1.A5_axioms" =
      (\<open>A5(B, A, D, C, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.1.eq" =
      \<open>B \<longleftrightarrow>
             A \<longleftrightarrow>
             D \<longleftrightarrow> C \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.3.A5_axioms" =
      (\<open>A5(B, A, E, D, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.3.eq" =
      \<open>B \<longleftrightarrow>
             A \<longleftrightarrow>
             E \<longleftrightarrow> D \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.1.A5_axioms" =
      (\<open>A5(E, B, A, D, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.1.eq" =
      \<open>E \<longleftrightarrow>
             B \<longleftrightarrow>
             A \<longleftrightarrow> D \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.1.A5_axioms" =
      (\<open>A5(E, B, C, A, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.1.eq" =
      \<open>E \<longleftrightarrow>
             B \<longleftrightarrow>
             C \<longleftrightarrow> A \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.2.A5_axioms" =
      (\<open>A5(E, B, D, C, A)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.2.eq" =
      \<open>E \<longleftrightarrow>
             B \<longleftrightarrow>
             D \<longleftrightarrow> C \<longleftrightarrow> A
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.1.A5_axioms" =
      (\<open>A5(A, B, E, C, D)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.1.eq" =
      \<open>A \<longleftrightarrow>
             B \<longleftrightarrow>
             E \<longleftrightarrow> C \<longleftrightarrow> D
               [A5(A, B, C, D, E)]\<close>
  notes
    "1.A5_axioms" = (\<open>A5(A, B, D, E, C)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "1.eq" =
      \<open>A \<longleftrightarrow>
             B \<longleftrightarrow>
             D \<longleftrightarrow> E \<longleftrightarrow> C
               [A5(A, B, C, D, E)]\<close>
  notes
    "A5_axioms" = (\<open>A5(A, B, C, D, E)  [A5(A, B, C, D, E)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "eq" =
      \<open>A \<longleftrightarrow>
             B \<longleftrightarrow>
             C \<longleftrightarrow> D \<longleftrightarrow> E
               [A5(A, B, C, D, E)]\<close>
locale trivial
  fixes P :: "o" 
    and Q :: "o" 
  assumes "trivial(P, Q)"
  notes
    "x.trivial_axioms" = (\<open>trivial(?x, Q)  [trivial(P, Q)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "x.Q" =
      \<open>?x \<longleftrightarrow> ?x \<longleftrightarrow> Q
               [trivial(P, Q)]\<close>
  notes theorem "x.Q_triv" = \<open>Q  [trivial(P, Q)]\<close>
  notes
    "trivial_axioms" = (\<open>trivial(P, Q)  [trivial(P, Q)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "Q" =
      \<open>P \<longleftrightarrow> P \<longleftrightarrow> Q
               [trivial(P, Q)]\<close>
  notes theorem "Q_triv" = \<open>Q  [trivial(P, Q)]\<close>
True \<longleftrightarrow> True \<longleftrightarrow> Q  [trivial(P, Q)]
locale trivial
  fixes P :: "o" 
    and Q :: "o" 
  assumes "trivial(P, Q)"
  notes
    "x.trivial_axioms" = (\<open>trivial(?x, Q)  [trivial(P, Q)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "x.Q" =
      \<open>?x \<longleftrightarrow> ?x \<longleftrightarrow> Q
               [trivial(P, Q)]\<close>
  notes theorem "x.Q_triv" = \<open>Q  [trivial(P, Q)]\<close>
  notes
    "trivial_axioms" = (\<open>trivial(P, Q)  [trivial(P, Q)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "Q" =
      \<open>P \<longleftrightarrow> P \<longleftrightarrow> Q
               [trivial(P, Q)]\<close>
  notes theorem "Q_triv" = \<open>Q  [trivial(P, Q)]\<close>
locale mixin4_combined
  fixes le' :: "'a \<Rightarrow> 'a \<Rightarrow> o" 
    and le :: "'b \<Rightarrow> 'b \<Rightarrow> o" 
  assumes "mixin4_combined(le', le)"
?x + ?y + ?z = ?x + (?y + ?z)
semi((+))
0 + ?x = ?x
?x + 0 = ?x
?x + ?y + ?z = ?x + (?y + ?z)
?x \<or> ?y \<longleftrightarrow> \<not> (\<not> ?x \<and> \<not> ?y)
logic_o.lor_o((\<and>), Not, ?x, ?y) \<longleftrightarrow> ?x \<or> ?y
True \<longleftrightarrow> True
?x \<or> ?y \<longleftrightarrow> ?x \<or> ?y
locale mixin5_base
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin5_base((\<sqsubseteq>))"
locale mixin5_inherited
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin5_inherited((\<sqsubseteq>))"
reflexive.less(gle, ?x, ?y) \<longleftrightarrow>
gle(?x, ?y) \<and> ?x \<noteq> ?y
*** Failed to apply initial proof method (line 578 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy"):
*** goal (1 subgoal):
***  1. gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y
*** At command "by" (line 578 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy")
reflexive.less(gle, ?x, ?y) \<longleftrightarrow>
gle(?x, ?y) \<and> ?x \<noteq> ?y
reflexive.less(gle, ?x, ?y) \<longleftrightarrow>
gle(?x, ?y) \<and> ?x \<noteq> ?y
reflexive.less(gle, ?x, ?y) \<longleftrightarrow>
gle(?x, ?y) \<and> ?x \<noteq> ?y
*** Failed to apply initial proof method (line 647 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy"):
*** goal (1 subgoal):
***  1. gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y
*** At command "by" (line 647 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy")
locale mixin6_base
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin6_base((\<sqsubseteq>))"
locale mixin6_inherited
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin6_inherited((\<sqsubseteq>))"
reflexive.less(gle, ?x, ?y) \<longleftrightarrow>
gle(?x, ?y) \<and> ?x \<noteq> ?y
*** Failed to apply initial proof method (line 672 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy"):
*** goal (1 subgoal):
***  1. gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y
*** At command "by" (line 672 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy")
locale mixin7_base
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin7_base((\<sqsubseteq>))"
locale mixin7_inherited
  fixes
    le :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infix "\<sqsubseteq>" 50)
  assumes "mixin7_inherited((\<sqsubseteq>))"
reflexive.less(gle, ?x, ?y) \<longleftrightarrow>
gle(?x, ?y) \<and> ?x \<noteq> ?y
reflexive.less(gle, ?x, ?y) \<longleftrightarrow>
gle(?x, ?y) \<and> ?x \<noteq> ?y
*** Failed to apply initial proof method (line 705 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy"):
*** goal (1 subgoal):
***  1. gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y
*** At command "by" (line 705 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy")
locale mixin_thy_merge
  fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> o" 
    and le' :: "'b \<Rightarrow> 'b \<Rightarrow> o" 
  assumes "mixin_thy_merge(le, le')"
### Introduced fixed type variable(s): 'a in "glob_inv" or "glob_one" or "prod" or "x"
locale dgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
  assumes "dgrp(( ** ))"
locale lgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "lgrp(( ** ), one, inv)"
### Ambiguous input (line 772 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy") produces 3 parse trees:
### ("\<^const>IFOL.Trueprop"
###   ("\<^const>IFOL.eq" ("\<^const>Locale_Test1.minus" ("_position" x))
###     ("_appl" ("_position" glob_inv)
###       ("_args" ("\<^const>Locale_Test1.plus") ("_position" x)))))
### ("\<^const>IFOL.Trueprop"
###   ("\<^const>Locale_Test1.minus"
###     ("\<^const>IFOL.eq" ("_position" x)
###       ("_appl" ("_position" glob_inv)
###         ("_args" ("\<^const>Locale_Test1.plus") ("_position" x))))))
### ("\<^const>IFOL.Trueprop"
###   ("_appl"
###     ("\<^const>Locale_Test1.minus"
###       ("\<^const>IFOL.eq" ("_position" x) ("_position" glob_inv)))
###     ("_args" ("\<^const>Locale_Test1.plus") ("_position" x))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
locale lgrp
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "**" 65)
    and one :: "'a" 
    and inv :: "'a \<Rightarrow> 'a" 
  assumes "lgrp(( ** ), one, inv)"
  notes
    "semi_axioms" = (\<open>semi(( ** ))  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "assoc" =
      \<open>?x ** ?y ** ?z = ?x ** (?y ** ?z)
               [lgrp(( ** ), one, inv)]\<close>
  notes
    "right.rgrp_axioms" =
      (\<open>rgrp(( ** ), one, inv)  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes
    "right.rone" = \<open>?x ** one = ?x  [lgrp(( ** ), one, inv)]\<close>
  notes
    "right.rinv" =
      \<open>?x ** inv(?x) = one  [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "right.rcancel" =
      \<open>?y ** ?x = ?z ** ?x \<longleftrightarrow> ?y = ?z
               [lgrp(( ** ), one, inv)]\<close>
  notes
    "def.dgrp_axioms" =
      (\<open>dgrp(( ** ))  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "def.one_def" =
      \<open>one = glob_one(( ** ))  [lgrp(( ** ), one, inv)]\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "def.lone" = \<open>one ** ?x = ?x  [lgrp(( ** ), one, inv)]\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes
    "def.inv_def" =
      \<open>inv(?x) = glob_inv(( ** ), ?x)
               [lgrp(( ** ), one, inv)]\<close>
  notes (\<open>TERM _\<close>) ["attribute" "<attribute>"]
  notes theorem
    "def.linv" =
      \<open>inv(?x) ** ?x = one  [lgrp(( ** ), one, inv)]\<close>
  notes
    "lgrp_axioms" =
      (\<open>lgrp(( ** ), one, inv)  [lgrp(( ** ), one, inv)]\<close>)
      ["attribute" "<attribute>"]
  notes "lone" = \<open>one ** ?x = ?x  [lgrp(( ** ), one, inv)]\<close>
  notes
    "linv" = \<open>inv(?x) ** ?x = one  [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "lcancel" =
      \<open>?x ** ?y = ?x ** ?z \<longleftrightarrow> ?y = ?z
               [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "one_equation" =
      \<open>dgrp.one(( ** )) = one  [lgrp(( ** ), one, inv)]\<close>
  notes theorem
    "inv_equation" =
      \<open>dgrp.inv(( ** ), ?x) = inv(?x)
               [lgrp(( ** ), one, inv)]\<close>
locale roundup
  fixes x :: "o" 
  assumes "roundup(x)"
locale container
locale container
val it = []: thm list
True \<longleftrightarrow> True
### theory "FOL-ex.Locale_Test1"
### 2.714s elapsed time, 3.124s cpu time, 0.072s GC time
Loading theory "FOL-ex.Locale_Test2" (required by "FOL-ex.Locale_Test")
### theory "FOL-ex.Locale_Test2"
### 0.005s elapsed time, 0.012s cpu time, 0.000s GC time
Loading theory "FOL-ex.Locale_Test3" (required by "FOL-ex.Locale_Test")
### theory "FOL-ex.Locale_Test3"
### 0.005s elapsed time, 0.012s cpu time, 0.000s GC time
Loading theory "FOL-ex.Locale_Test"
### Removed duplicate interpretation after retrieving its mixins.
locale mixin_thy_merge
  fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> o" 
    and le' :: "'b \<Rightarrow> 'b \<Rightarrow> o" 
  assumes "mixin_thy_merge(le, le')"
### theory "FOL-ex.Locale_Test"
### 0.011s elapsed time, 0.024s cpu time, 0.000s GC time
zero + ?x = ?x  [\<And>x. zero + x = x, \<And>x. - x + x = zero]
dependencies:
  semi "(+)"
  right? : rgrp "(+)" "0" "minus"
  def? : dgrp "(+)"
  lgrp "(+)" "0" "minus"
  right? : rgrp "(+)" "zero" "minus"
  lgrp "(+)" "zero" "minus"
0 + ?x = ?x  [\<And>x zero. zero + x = x, \<And>x zero. - x + x = zero]
interpretations:
  loc : logic_o "pand" "pnot"
  y : logic_o "(\<or>)" "Not"
  x : logic_o "(\<and>)" "Not"
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline -o pdf -n outline -t /proof,/ML
*** Failed to apply initial proof method (line 705 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy"):
*** goal (1 subgoal):
***  1. gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y
*** At command "by" (line 705 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy")
*** Failed to apply initial proof method (line 672 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy"):
*** goal (1 subgoal):
***  1. gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y
*** At command "by" (line 672 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy")
*** Failed to apply initial proof method (line 647 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy"):
*** goal (1 subgoal):
***  1. gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y
*** At command "by" (line 647 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy")
*** Failed to apply initial proof method (line 578 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy"):
*** goal (1 subgoal):
***  1. gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y
*** At command "by" (line 578 of "~~/src/FOL/ex/Locale_Test/Locale_Test1.thy")