Loading theory "HOL-Library.Lattice_Syntax" (required by "SIFUM_Type_Systems.Preliminaries")
### theory "HOL-Library.Lattice_Syntax"
### 0.013s elapsed time, 0.028s cpu time, 0.000s GC time
Loading theory "SIFUM_Type_Systems.Preliminaries"
instantiation
  Sec :: complete_lattice
  Inf_Sec == Inf :: Sec set \<Rightarrow> Sec
  Sup_Sec == Sup :: Sec set \<Rightarrow> Sec
  bot_Sec == bot :: Sec
  sup_Sec == sup :: Sec \<Rightarrow> Sec \<Rightarrow> Sec
  top_Sec == top :: Sec
  inf_Sec == inf :: Sec \<Rightarrow> Sec \<Rightarrow> Sec
  less_eq_Sec == less_eq :: Sec \<Rightarrow> Sec \<Rightarrow> bool
  less_Sec == less :: Sec \<Rightarrow> Sec \<Rightarrow> bool
locale sifum_security
  fixes dma :: "'Var \<Rightarrow> Sec"
    and stop :: "'Com"
    and
    eval ::
      "((('Com \<times> (Mode \<Rightarrow> 'Var set)) \<times>
         ('Var \<Rightarrow> 'Val)) \<times>
        ('Com \<times> (Mode \<Rightarrow> 'Var set)) \<times>
        ('Var \<Rightarrow> 'Val)) set"
    and some_val :: "'Val"
    and some_val' :: "'Val"
  assumes "sifum_security stop eval some_val some_val'"
### theory "SIFUM_Type_Systems.Preliminaries"
### 1.617s elapsed time, 2.104s cpu time, 0.000s GC time
Loading theory "SIFUM_Type_Systems.Language"
Loading theory "SIFUM_Type_Systems.Security"
locale sifum_security
  fixes dma :: "'Var \<Rightarrow> Sec"
    and stop :: "'Com"
    and
    eval ::
      "((('Com \<times> (Mode \<Rightarrow> 'Var set)) \<times>
         ('Var \<Rightarrow> 'Val)) \<times>
        ('Com \<times> (Mode \<Rightarrow> 'Var set)) \<times>
        ('Var \<Rightarrow> 'Val)) set"
    and some_val :: "'Val"
    and some_val' :: "'Val"
  assumes "sifum_security stop eval some_val some_val'"
Proofs for inductive predicate(s) "mevalp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "{}"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Proofs for inductive predicate(s) "mm_equivp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "loc_reachp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  sound_mode_use ::
    "('Com \<times> (Mode \<Rightarrow> 'Var set)) list \<times>
     ('Var \<Rightarrow> 'Val)
     \<Rightarrow> bool"
### theory "SIFUM_Type_Systems.Security"
### 1.613s elapsed time, 3.196s cpu time, 0.408s GC time
Loading theory "SIFUM_Type_Systems.Compositionality"
locale sifum_security
  fixes dma :: "'Var \<Rightarrow> Sec"
    and stop :: "'Com"
    and
    eval ::
      "((('Com \<times> (Mode \<Rightarrow> 'Var set)) \<times>
         ('Var \<Rightarrow> 'Val)) \<times>
        ('Com \<times> (Mode \<Rightarrow> 'Var set)) \<times>
        ('Var \<Rightarrow> 'Val)) set"
    and some_val :: "'Val"
    and some_val' :: "'Val"
  assumes "sifum_security stop eval some_val some_val'"
Found termination order: "{}"
Found termination order: "{}"
### Ambiguous input (line 866 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_k_abv_indexed"
###     ("_tuple" ("_position" cms\<^sub>1)
###       ("_tuple_arg" ("_position" mem\<^sub>1)))
###     ("_indexdefault")
###     ("_tuple" ("_position" cms\<^sub>1')
###       ("_tuple_arg" ("_position" mem\<^sub>1')))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_abv"
###     ("_tuple" ("_position" cms\<^sub>1)
###       ("_tuple_arg" ("_position" mem\<^sub>1)))
###     ("_tuple" ("_position" cms\<^sub>1')
###       ("_tuple_arg" ("_position" mem\<^sub>1')))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 868 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" snd) ("_position" cms\<^sub>1')))
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" snd) ("_position" cms\<^sub>2'))))
###     ("\<^const>HOL.conj"
###       ("\<^const>local.meval_k_abv_indexed"
###         ("_tuple" ("_position" cms\<^sub>2)
###           ("_tuple_arg" ("_position" mem\<^sub>2)))
###         ("_indexdefault")
###         ("_tuple" ("_position" cms\<^sub>2')
###           ("_tuple_arg" ("_position" mem\<^sub>2'))))
###       ("_applC" ("_position" makes_compatible)
###         ("_cargs"
###           ("_tuple" ("_position" cms\<^sub>1')
###             ("_tuple_arg" ("_position" mem\<^sub>1')))
###           ("_cargs"
###             ("_tuple" ("_position" cms\<^sub>2')
###               ("_tuple_arg" ("_position" mem\<^sub>2')))
###             ("_position" mems')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" snd) ("_position" cms\<^sub>1')))
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" snd) ("_position" cms\<^sub>2'))))
###     ("\<^const>HOL.conj"
###       ("\<^const>local.meval_abv"
###         ("_tuple" ("_position" cms\<^sub>2)
###           ("_tuple_arg" ("_position" mem\<^sub>2)))
###         ("_tuple" ("_position" cms\<^sub>2')
###           ("_tuple_arg" ("_position" mem\<^sub>2'))))
###       ("_applC" ("_position" makes_compatible)
###         ("_cargs"
###           ("_tuple" ("_position" cms\<^sub>1')
###             ("_tuple_arg" ("_position" mem\<^sub>1')))
###           ("_cargs"
###             ("_tuple" ("_position" cms\<^sub>2')
###               ("_tuple_arg" ("_position" mem\<^sub>2')))
###             ("_position" mems')))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
locale sifum_lang
  fixes
    eval\<^sub>A ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'AExp \<Rightarrow> 'Val"
    and
    eval\<^sub>B ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'BExp \<Rightarrow> bool"
    and aexp_vars :: "'AExp \<Rightarrow> 'Var set"
    and bexp_vars :: "'BExp \<Rightarrow> 'Var set"
    and dma :: "'Var \<Rightarrow> Sec"
  assumes "sifum_lang eval\<^sub>A eval\<^sub>B aexp_vars bexp_vars"
locale sifum_lang
  fixes
    eval\<^sub>A ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'AExp \<Rightarrow> 'Val"
    and
    eval\<^sub>B ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'BExp \<Rightarrow> bool"
    and aexp_vars :: "'AExp \<Rightarrow> 'Var set"
    and bexp_vars :: "'BExp \<Rightarrow> 'Var set"
    and dma :: "'Var \<Rightarrow> Sec"
  assumes "sifum_lang eval\<^sub>A eval\<^sub>B aexp_vars bexp_vars"
### Ambiguous input (line 1808 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_k_abv_indexed"
###     ("_tuple" ("_position" cms) ("_tuple_arg" ("_position" mem)))
###     ("_indexdefault")
###     ("_tuple" ("_position" cms') ("_tuple_arg" ("_position" mem')))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_abv"
###     ("_tuple" ("_position" cms) ("_tuple_arg" ("_position" mem)))
###     ("_tuple" ("_position" cms') ("_tuple_arg" ("_position" mem')))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1821 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_k_abv_indexed"
###     ("_tuple" ("_position" cms) ("_tuple_arg" ("_position" mem)))
###     ("_indexdefault")
###     ("_tuple" ("_position" cms') ("_tuple_arg" ("_position" mem')))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_abv"
###     ("_tuple" ("_position" cms) ("_tuple_arg" ("_position" mem)))
###     ("_tuple" ("_position" cms') ("_tuple_arg" ("_position" mem')))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
consts
  update_modes ::
    "'Var ModeUpd
     \<Rightarrow> (Mode \<Rightarrow> 'Var set)
                   \<Rightarrow> Mode \<Rightarrow> 'Var set"
### Ambiguous input (line 1857 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_k_abv_indexed"
###     ("_tuple" ("_position" cms) ("_tuple_arg" ("_position" mem)))
###     ("_indexdefault")
###     ("_tuple" ("_position" cms') ("_tuple_arg" ("_position" mem')))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_abv"
###     ("_tuple" ("_position" cms) ("_tuple_arg" ("_position" mem)))
###     ("_tuple" ("_position" cms') ("_tuple_arg" ("_position" mem')))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "SIFUM_Type_Systems.Compositionality"
### 2.301s elapsed time, 4.384s cpu time, 0.756s GC time
Found termination order: "{}"
Found termination order: "{}"
Proofs for inductive predicate(s) "eval\<^sub>w_simplep"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  cxt_to_stmt ::
    "('Var, 'AExp, 'BExp) Stmt list
     \<Rightarrow> ('Var, 'AExp, 'BExp) Stmt
                   \<Rightarrow> ('Var, 'AExp, 'BExp) Stmt"
Proofs for inductive predicate(s) "eval\<^sub>wp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "SIFUM_Type_Systems.Language"
### 5.190s elapsed time, 10.140s cpu time, 1.164s GC time
Loading theory "SIFUM_Type_Systems.LocallySoundModeUse"
Loading theory "SIFUM_Type_Systems.TypeSystem"
locale sifum_modes
  fixes aexp_vars :: "'AExp \<Rightarrow> 'Var set"
    and bexp_vars :: "'BExp \<Rightarrow> 'Var set"
    and dma :: "'Var \<Rightarrow> Sec"
    and some_val :: "'Val"
    and some_val' :: "'Val"
    and
    ev\<^sub>A ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'AExp \<Rightarrow> 'Val"
    and
    ev\<^sub>B ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'BExp \<Rightarrow> bool"
  assumes
    "sifum_modes aexp_vars bexp_vars some_val some_val' ev\<^sub>A
      ev\<^sub>B"
locale sifum_modes
  fixes aexp_vars :: "'AExp \<Rightarrow> 'Var set"
    and bexp_vars :: "'BExp \<Rightarrow> 'Var set"
    and dma :: "'Var \<Rightarrow> Sec"
    and some_val :: "'Val"
    and some_val' :: "'Val"
    and
    ev\<^sub>A ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'AExp \<Rightarrow> 'Val"
    and
    ev\<^sub>B ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'BExp \<Rightarrow> bool"
  assumes
    "sifum_modes aexp_vars bexp_vars some_val some_val' ev\<^sub>A
      ev\<^sub>B"
locale sifum_types
  fixes aexp_vars :: "'AExp \<Rightarrow> 'Var set"
    and bexp_vars :: "'BExp \<Rightarrow> 'Var set"
    and dma :: "'Var \<Rightarrow> Sec"
    and some_val :: "'Val"
    and some_val' :: "'Val"
    and
    ev\<^sub>A ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'AExp \<Rightarrow> 'Val"
    and
    ev\<^sub>B ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'BExp \<Rightarrow> bool"
  assumes
    "sifum_types aexp_vars bexp_vars some_val some_val' ev\<^sub>A
      ev\<^sub>B"
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
### Ambiguous input (line 36 of "~~/afp/thys/SIFUM_Type_Systems/LocallySoundModeUse.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" annotate)
###       ("_cargs" ("_position" c)
###         ("\<^const>List.list.Cons" ("_position" a) ("_position" as))))
###     ("\<^const>Language.Stmt.ModeDecl"
###       ("_applC" ("_position" annotate)
###         ("_cargs" ("_position" c) ("_position" as)))
###       ("_position" a))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Language.Stmt.ModeDecl"
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" annotate)
###         ("_cargs" ("_position" c)
###           ("\<^const>List.list.Cons" ("_position" a) ("_position" as))))
###       ("_applC" ("_position" annotate)
###         ("_cargs" ("_position" c) ("_position" as))))
###     ("_position" a)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
Proofs for inductive predicate(s) "mode_type"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
locale sifum_types
  fixes aexp_vars :: "'AExp \<Rightarrow> 'Var set"
    and bexp_vars :: "'BExp \<Rightarrow> 'Var set"
    and dma :: "'Var \<Rightarrow> Sec"
    and some_val :: "'Val"
    and some_val' :: "'Val"
    and
    ev\<^sub>A ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'AExp \<Rightarrow> 'Val"
    and
    ev\<^sub>B ::
      "('Var \<Rightarrow> 'Val) \<Rightarrow> 'BExp \<Rightarrow> bool"
  assumes
    "sifum_types aexp_vars bexp_vars some_val some_val' ev\<^sub>A
      ev\<^sub>B"
### Ambiguous input (line 51 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^fixed>type_aexpr" ("_position" \<Gamma>) ("_position" e)
###     ("_applC" ("_position" max_dom)
###       ("_applC" ("_position" image)
###         ("_cargs"
###           ("_lambda" ("_position" x)
###             ("_applC" ("_position" to_total)
###               ("_cargs" ("_position" \<Gamma>) ("_position" x))))
###           ("_applC" ("_position" aexp_vars) ("_position" e)))))))
### ("\<^const>HOL.Trueprop"
###   ("_applC"
###     ("\<^fixed>type_aexpr" ("_position" \<Gamma>) ("_position" e)
###       ("_position" max_dom))
###     ("_applC" ("_position" image)
###       ("_cargs"
###         ("_lambda" ("_position" x)
###           ("_applC" ("_position" to_total)
###             ("_cargs" ("_position" \<Gamma>) ("_position" x))))
###         ("_applC" ("_position" aexp_vars) ("_position" e))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Proofs for inductive predicate(s) "type_aexpr"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### Ambiguous input (line 57 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^fixed>type_bexpr" ("_position" \<Gamma>) ("_position" e)
###     ("_applC" ("_position" max_dom)
###       ("_applC" ("_position" image)
###         ("_cargs"
###           ("_lambda" ("_position" x)
###             ("_applC" ("_position" to_total)
###               ("_cargs" ("_position" \<Gamma>) ("_position" x))))
###           ("_applC" ("_position" bexp_vars) ("_position" e)))))))
### ("\<^const>HOL.Trueprop"
###   ("_applC"
###     ("\<^fixed>type_bexpr" ("_position" \<Gamma>) ("_position" e)
###       ("_position" max_dom))
###     ("_applC" ("_position" image)
###       ("_cargs"
###         ("_lambda" ("_position" x)
###           ("_applC" ("_position" to_total)
###             ("_cargs" ("_position" \<Gamma>) ("_position" x))))
###         ("_applC" ("_position" bexp_vars) ("_position" e))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Proofs for inductive predicate(s) "type_bexpr"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "SIFUM_Type_Systems.LocallySoundModeUse"
### 1.942s elapsed time, 3.848s cpu time, 0.464s GC time
Found termination order: "{}"
Proofs for inductive predicate(s) "has_type"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "size <*mlex*> {}"
### Ambiguous input (line 121 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>Pure.eq"
###   ("\<^fixed>tyenv_eq_indexed" ("_position" mem\<^sub>1)
###     ("_index" ("_position" \<Gamma>)) ("_position" mem\<^sub>2))
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^fixed>tyenv_eq_indexed"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_indexdefault") ("_position" Low))
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>Pure.eq"
###   ("\<^fixed>tyenv_eq_indexed" ("_position" mem\<^sub>1)
###     ("_index" ("_position" \<Gamma>)) ("_position" mem\<^sub>2))
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_position" Low))
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>Pure.eq"
###   ("\<^fixed>tyenv_eq_indexed" ("_position" mem\<^sub>1)
###     ("_index" ("_position" \<Gamma>)) ("_position" mem\<^sub>2))
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^fixed>tyenv_eq_indexed"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_indexdefault") ("_position" Low))
###       ("\<^fixed>tyenv_eq_indexed"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_indexdefault")
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>Pure.eq"
###   ("\<^fixed>tyenv_eq_indexed" ("_position" mem\<^sub>1)
###     ("_index" ("_position" \<Gamma>)) ("_position" mem\<^sub>2))
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_position" Low))
###       ("\<^fixed>tyenv_eq_indexed"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_indexdefault")
###         ("_applC" ("_position" mem\<^sub>2) ("_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.
Proofs for inductive predicate(s) "\<R>\<^sub>1p"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### Ambiguous input (line 146 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.mm_equiv_abv2"
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###           ("_position" mem\<^sub>1))
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>2) ("_position" mds)
###           ("_position" mem\<^sub>2))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("_Ball" ("_position" x)
###           ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###           ("\<^const>HOL.eq"
###             ("_applC" ("_position" \<Gamma>') ("_position" x))
###             ("_applC" ("_position" Some) ("_position" High)))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>local.has_type" ("_position" \<Gamma>\<^sub>1)
###             ("_position" c\<^sub>1) ("_position" \<Gamma>')))
###         ("_asms"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>local.has_type" ("_position" \<Gamma>\<^sub>2)
###               ("_position" c\<^sub>2) ("_position" \<Gamma>')))
###           ("_asms"
###             ("\<^const>HOL.Trueprop"
###               ("_applC" ("_position" mds_consistent)
###                 ("_cargs" ("_position" mds)
###                   ("_position" \<Gamma>\<^sub>1))))
###             ("_asm"
###               ("\<^const>HOL.Trueprop"
###                 ("_applC" ("_position" mds_consistent)
###                   ("_cargs" ("_position" mds)
###                     ("_position" \<Gamma>\<^sub>2))))))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^fixed>\<R>\<^sub>2_abv_indexed"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("_index" ("_position" \<Gamma>'))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>2) ("_position" mds)
###         ("_position" mem\<^sub>2)))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.mm_equiv_abv2"
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###           ("_position" mem\<^sub>1))
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>2) ("_position" mds)
###           ("_position" mem\<^sub>2))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("_Ball" ("_position" x)
###           ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###           ("\<^const>local.tyenv_eq_indexed"
###             ("_applC" ("_position" \<Gamma>') ("_position" x))
###             ("_indexdefault")
###             ("_applC" ("_position" Some) ("_position" High)))))
###       ("_asms"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>local.has_type" ("_position" \<Gamma>\<^sub>1)
###             ("_position" c\<^sub>1) ("_position" \<Gamma>')))
###         ("_asms"
###           ("\<^const>HOL.Trueprop"
###             ("\<^const>local.has_type" ("_position" \<Gamma>\<^sub>2)
###               ("_position" c\<^sub>2) ("_position" \<Gamma>')))
###           ("_asms"
###             ("\<^const>HOL.Trueprop"
###               ("_applC" ("_position" mds_consistent)
###                 ("_cargs" ("_position" mds)
###                   ("_position" \<Gamma>\<^sub>1))))
###             ("_asm"
###               ("\<^const>HOL.Trueprop"
###                 ("_applC" ("_position" mds_consistent)
###                   ("_cargs" ("_position" mds)
###                     ("_position" \<Gamma>\<^sub>2))))))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^fixed>\<R>\<^sub>2_abv_indexed"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("_index" ("_position" \<Gamma>'))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>2) ("_position" mds)
###         ("_position" mem\<^sub>2)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Proofs for inductive predicate(s) "\<R>\<^sub>2p"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "\<R>\<^sub>3_aux"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "\<R>p"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### Ambiguous input (line 225 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>Pure.imp"
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>local.\<R>_abv_indexed"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("_index" ("_position" \<Gamma>))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>2) ("_position" mds')
###         ("_position" mem\<^sub>2))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq" ("_position" mds) ("_position" mds'))))
### ("\<^const>Pure.imp"
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>local.\<R>_abv_indexed"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("_index" ("_position" \<Gamma>))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>2) ("_position" mds')
###         ("_position" mem\<^sub>2))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds) ("_indexdefault")
###       ("_position" mds'))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  subst_abv mem ::
***   ('Var \<Rightarrow> 'Val option) \<Rightarrow> 'Var \<Rightarrow> 'Val
*** Operand:   {} :: ??'a set
*** 
*** At command "have" (line 288 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy")
### Ambiguous input (line 312 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 8 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" closed_glob_helper)
###       ("_cargs" ("_position" \<Gamma>')
###         ("_cargs"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds) ("_position" mem\<^sub>1))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds\<^sub>2) ("_position" mem\<^sub>2)))))
###     ("\<^const>HOL.All_binder" ("_position" x)
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>local.tyenv_eq_indexed"
###               ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###               ("_position" High))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder"
###             ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x)
###                         ("_position" v\<^sub>2))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>local.tyenv_eq_indexed"
###               ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###               ("_position" Low))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder" ("_position" v)
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x) ("_position" v))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" closed_glob_helper)
###       ("_cargs" ("_position" \<Gamma>')
###         ("_cargs"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds) ("_position" mem\<^sub>1))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds\<^sub>2) ("_position" mem\<^sub>2)))))
###     ("_indexdefault")
###     ("\<^const>HOL.All_binder" ("_position" x)
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>local.tyenv_eq_indexed"
###               ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###               ("_position" High))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder"
###             ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x)
###                         ("_position" v\<^sub>2))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>local.tyenv_eq_indexed"
###               ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###               ("_position" Low))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder" ("_position" v)
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x) ("_position" v))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" closed_glob_helper)
###       ("_cargs" ("_position" \<Gamma>')
###         ("_cargs"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds) ("_position" mem\<^sub>1))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds\<^sub>2) ("_position" mem\<^sub>2)))))
###     ("\<^const>HOL.All_binder" ("_position" x)
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###               ("_position" High))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder"
###             ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x)
###                         ("_position" v\<^sub>2))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>local.tyenv_eq_indexed"
###               ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###               ("_position" Low))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder" ("_position" v)
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x) ("_position" v))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" closed_glob_helper)
###       ("_cargs" ("_position" \<Gamma>')
###         ("_cargs"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds) ("_position" mem\<^sub>1))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds\<^sub>2) ("_position" mem\<^sub>2)))))
###     ("_indexdefault")
###     ("\<^const>HOL.All_binder" ("_position" x)
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###               ("_position" High))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder"
###             ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x)
###                         ("_position" v\<^sub>2))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>local.tyenv_eq_indexed"
###               ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###               ("_position" Low))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder" ("_position" v)
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x) ("_position" v))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" closed_glob_helper)
###       ("_cargs" ("_position" \<Gamma>')
###         ("_cargs"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds) ("_position" mem\<^sub>1))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds\<^sub>2) ("_position" mem\<^sub>2)))))
###     ("\<^const>HOL.All_binder" ("_position" x)
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>local.tyenv_eq_indexed"
###               ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###               ("_position" High))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder"
###             ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x)
###                         ("_position" v\<^sub>2))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###               ("_position" Low))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder" ("_position" v)
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x) ("_position" v))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" closed_glob_helper)
###       ("_cargs" ("_position" \<Gamma>')
###         ("_cargs"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds) ("_position" mem\<^sub>1))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds\<^sub>2) ("_position" mem\<^sub>2)))))
###     ("_indexdefault")
###     ("\<^const>HOL.All_binder" ("_position" x)
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>local.tyenv_eq_indexed"
###               ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###               ("_position" High))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder"
###             ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x)
###                         ("_position" v\<^sub>2))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###               ("_position" Low))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder" ("_position" v)
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x) ("_position" v))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" closed_glob_helper)
###       ("_cargs" ("_position" \<Gamma>')
###         ("_cargs"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds) ("_position" mem\<^sub>1))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds\<^sub>2) ("_position" mem\<^sub>2)))))
###     ("\<^const>HOL.All_binder" ("_position" x)
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###               ("_position" High))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder"
###             ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x)
###                         ("_position" v\<^sub>2))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###               ("_position" Low))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder" ("_position" v)
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x) ("_position" v))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" closed_glob_helper)
###       ("_cargs" ("_position" \<Gamma>')
###         ("_cargs"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds) ("_position" mem\<^sub>1))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds\<^sub>2) ("_position" mem\<^sub>2)))))
###     ("_indexdefault")
###     ("\<^const>HOL.All_binder" ("_position" x)
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###               ("_position" High))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder"
###             ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x)
###                         ("_position" v\<^sub>2))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))
###         ("\<^const>HOL.implies"
###           ("\<^const>HOL.conj"
###             ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###               ("_position" Low))
###             ("\<^const>Set.not_member" ("_position" x)
###               ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###           ("\<^const>HOL.All_binder" ("_position" v)
###             ("\<^const>Set.member"
###               ("_tuple"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>1)
###                     ("_updbind" ("_position" x) ("_position" v))))
###                 ("_tuple_arg"
###                   ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                     ("_position" mds)
###                     ("_Update" ("_position" mem\<^sub>2)
###                       ("_updbind" ("_position" x) ("_position" v))))))
###               ("_applC" ("_position" \<R>\<^sub>3)
###                 ("_position" \<Gamma>')))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Found termination order: "{}"
### Ambiguous input (line 320 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.conj"
###       ("\<^const>HOL.implies"
###         ("\<^const>HOL.conj"
###           ("\<^const>local.tyenv_eq_indexed"
###             ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###             ("_position" High))
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###         ("\<^const>HOL.All_binder"
###           ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###           ("\<^const>Set.member"
###             ("_tuple"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>1)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###               ("_tuple_arg"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>2)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###             ("_applC" ("_position" \<R>\<^sub>3) ("_position" \<Gamma>')))))
###       ("\<^const>HOL.implies"
###         ("\<^const>HOL.conj"
###           ("\<^const>local.tyenv_eq_indexed"
###             ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###             ("_position" Low))
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###         ("\<^const>HOL.All_binder" ("_position" v)
###           ("\<^const>Set.member"
###             ("_tuple"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>1)
###                   ("_updbind" ("_position" x) ("_position" v))))
###               ("_tuple_arg"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>2)
###                     ("_updbind" ("_position" x) ("_position" v))))))
###             ("_applC" ("_position" \<R>\<^sub>3)
###               ("_position" \<Gamma>'))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.conj"
###       ("\<^const>HOL.implies"
###         ("\<^const>HOL.conj"
###           ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###             ("_position" High))
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###         ("\<^const>HOL.All_binder"
###           ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###           ("\<^const>Set.member"
###             ("_tuple"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>1)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###               ("_tuple_arg"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>2)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###             ("_applC" ("_position" \<R>\<^sub>3) ("_position" \<Gamma>')))))
###       ("\<^const>HOL.implies"
###         ("\<^const>HOL.conj"
###           ("\<^const>local.tyenv_eq_indexed"
###             ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###             ("_position" Low))
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###         ("\<^const>HOL.All_binder" ("_position" v)
###           ("\<^const>Set.member"
###             ("_tuple"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>1)
###                   ("_updbind" ("_position" x) ("_position" v))))
###               ("_tuple_arg"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>2)
###                     ("_updbind" ("_position" x) ("_position" v))))))
###             ("_applC" ("_position" \<R>\<^sub>3)
###               ("_position" \<Gamma>'))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.conj"
###       ("\<^const>HOL.implies"
###         ("\<^const>HOL.conj"
###           ("\<^const>local.tyenv_eq_indexed"
###             ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###             ("_position" High))
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###         ("\<^const>HOL.All_binder"
###           ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###           ("\<^const>Set.member"
###             ("_tuple"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>1)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###               ("_tuple_arg"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>2)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###             ("_applC" ("_position" \<R>\<^sub>3) ("_position" \<Gamma>')))))
###       ("\<^const>HOL.implies"
###         ("\<^const>HOL.conj"
###           ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###             ("_position" Low))
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###         ("\<^const>HOL.All_binder" ("_position" v)
###           ("\<^const>Set.member"
###             ("_tuple"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>1)
###                   ("_updbind" ("_position" x) ("_position" v))))
###               ("_tuple_arg"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>2)
###                     ("_updbind" ("_position" x) ("_position" v))))))
###             ("_applC" ("_position" \<R>\<^sub>3)
###               ("_position" \<Gamma>'))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.conj"
###       ("\<^const>HOL.implies"
###         ("\<^const>HOL.conj"
###           ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###             ("_position" High))
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###         ("\<^const>HOL.All_binder"
###           ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###           ("\<^const>Set.member"
###             ("_tuple"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>1)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###               ("_tuple_arg"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>2)
###                     ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###             ("_applC" ("_position" \<R>\<^sub>3) ("_position" \<Gamma>')))))
###       ("\<^const>HOL.implies"
###         ("\<^const>HOL.conj"
###           ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###             ("_position" Low))
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###         ("\<^const>HOL.All_binder" ("_position" v)
###           ("\<^const>Set.member"
###             ("_tuple"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>1)
###                   ("_updbind" ("_position" x) ("_position" v))))
###               ("_tuple_arg"
###                 ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                   ("_position" mds)
###                   ("_Update" ("_position" mem\<^sub>2)
###                     ("_updbind" ("_position" x) ("_position" v))))))
###             ("_applC" ("_position" \<R>\<^sub>3)
###               ("_position" \<Gamma>'))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 397 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_indexdefault") ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 405 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_indexdefault") ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 423 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.has_type" ("_position" \<Gamma>) ("_position" c)
###         ("_position" \<Gamma>')))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>local.tyenv_eq_indexed" ("_position" c) ("_indexdefault")
###           ("_position" Stop)))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>local.context_le" ("_position" \<Gamma>)
###       ("_position" \<Gamma>'))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.has_type" ("_position" \<Gamma>) ("_position" c)
###         ("_position" \<Gamma>')))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>HOL.eq" ("_position" c) ("_position" Stop)))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>local.context_le" ("_position" \<Gamma>)
###       ("_position" \<Gamma>'))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 540 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" bisim_helper)
###       ("_cargs"
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###           ("_position" mem\<^sub>1))
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###           ("_position" mds\<^sub>2) ("_position" mem\<^sub>2))))
###     ("_indexdefault")
###     ("\<^const>local.low_mds_eq_indexed" ("_position" mem\<^sub>1)
###       ("_index" ("_position" mds)) ("_position" mem\<^sub>2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" bisim_helper)
###       ("_cargs"
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###           ("_position" mem\<^sub>1))
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###           ("_position" mds\<^sub>2) ("_position" mem\<^sub>2))))
###     ("\<^const>local.low_mds_eq_indexed" ("_position" mem\<^sub>1)
###       ("_index" ("_position" mds)) ("_position" mem\<^sub>2))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Found termination order: "{}"
### Ambiguous input (line 656 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c) ("_indexdefault")
###     ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1212 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_position" Low))
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_indexdefault")
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_indexdefault") ("_position" Low))
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_indexdefault")
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_position" Low))
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_indexdefault") ("_position" Low))
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_applC" ("_position" mem\<^sub>2) ("_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.
### Ambiguous input (line 1224 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_position" Low))
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_indexdefault")
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_indexdefault") ("_position" Low))
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_indexdefault")
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_position" Low))
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_applC" ("_position" mem\<^sub>2) ("_position" x))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.All_binder" ("_position" x)
###     ("\<^const>HOL.implies"
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_indexdefault") ("_position" Low))
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" mem\<^sub>1) ("_position" x))
###         ("_applC" ("_position" mem\<^sub>2) ("_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.
### Ambiguous input (line 1230 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" \<Gamma>\<^sub>0) ("_position" x))
###     ("_position" None)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" \<Gamma>\<^sub>0) ("_position" x))
###     ("_indexdefault") ("_position" None)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1236 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("_applC" ("_position" list_all)
###         ("_cargs"
###           ("_lambda" ("_position" c)
###             ("_applC"
###               ("\<^fixed>type_global"
###                 ("_applC" ("_position" \<Gamma>\<^sub>0)
###                   ("_Finset" ("_position" c))))
###               ("_position" \<Gamma>\<^sub>0)))
###           ("_position" cs))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>HOL.All_binder" ("_position" mem)
###           ("_applC" ("_position" sound_mode_use)
###             ("_tuple"
###               ("_applC" ("_position" add_initial_modes) ("_position" cs))
###               ("_tuple_arg" ("_position" mem))))))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" type_global) ("_position" cs))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("_applC" ("_position" list_all)
###         ("_cargs"
###           ("_lambda" ("_position" c)
###             ("\<^fixed>type_global"
###               ("_applC" ("_position" \<Gamma>\<^sub>0)
###                 ("_cargs" ("_Finset" ("_position" c))
###                   ("_position" \<Gamma>\<^sub>0)))))
###           ("_position" cs))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>HOL.All_binder" ("_position" mem)
###           ("_applC" ("_position" sound_mode_use)
###             ("_tuple"
###               ("_applC" ("_position" add_initial_modes) ("_position" cs))
###               ("_tuple_arg" ("_position" mem))))))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" type_global) ("_position" cs))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("_applC" ("_position" list_all)
###         ("_cargs"
###           ("_lambda" ("_position" c)
###             ("_applC"
###               ("\<^fixed>type_global" ("_position" \<Gamma>\<^sub>0))
###               ("_cargs" ("_Finset" ("_position" c))
###                 ("_position" \<Gamma>\<^sub>0))))
###           ("_position" cs))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>HOL.All_binder" ("_position" mem)
###           ("_applC" ("_position" sound_mode_use)
###             ("_tuple"
###               ("_applC" ("_position" add_initial_modes) ("_position" cs))
###               ("_tuple_arg" ("_position" mem))))))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" type_global) ("_position" cs))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("_applC" ("_position" list_all)
###         ("_cargs"
###           ("_lambda" ("_position" c)
###             ("\<^const>local.has_type" ("_position" \<Gamma>\<^sub>0)
###               ("_position" c) ("_position" \<Gamma>\<^sub>0)))
###           ("_position" cs))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>HOL.All_binder" ("_position" mem)
###           ("_applC" ("_position" sound_mode_use)
###             ("_tuple"
###               ("_applC" ("_position" add_initial_modes) ("_position" cs))
###               ("_tuple_arg" ("_position" mem))))))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" type_global) ("_position" cs))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Proofs for inductive predicate(s) "type_global"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### Ambiguous input (line 1246 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("_bigimpl"
###   ("_asm"
###     ("\<^const>HOL.Trueprop"
###       ("_applC"
###         ("\<^const>local.type_global"
###           ("_applC" ("_position" \<Gamma>\<^sub>0)
###             ("_Finset" ("_position" c))))
###         ("_position" \<Gamma>\<^sub>0))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" com_sifum_secure) ("_position" c))))
### ("_bigimpl"
###   ("_asm"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.type_global"
###         ("_applC" ("_position" \<Gamma>\<^sub>0)
###           ("_cargs" ("_Finset" ("_position" c))
###             ("_position" \<Gamma>\<^sub>0))))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" com_sifum_secure) ("_position" c))))
### ("_bigimpl"
###   ("_asm"
###     ("\<^const>HOL.Trueprop"
###       ("_applC"
###         ("\<^const>local.type_global" ("_position" \<Gamma>\<^sub>0))
###         ("_cargs" ("_Finset" ("_position" c))
###           ("_position" \<Gamma>\<^sub>0)))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" com_sifum_secure) ("_position" c))))
### ("_bigimpl"
###   ("_asm"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.has_type" ("_position" \<Gamma>\<^sub>0)
###         ("_position" c) ("_position" \<Gamma>\<^sub>0))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" ("_position" com_sifum_secure) ("_position" c))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1253 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("_applC" ("_position" mds_consistent)
###         ("_cargs" ("_position" mds) ("_position" \<Gamma>\<^sub>0))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low)))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Set.not_member" ("_position" x)
###       ("_applC" ("_position" mds) ("_position" AsmNoRead)))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("_applC" ("_position" mds_consistent)
###         ("_cargs" ("_position" mds) ("_position" \<Gamma>\<^sub>0))))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low)))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Set.not_member" ("_position" x)
###       ("_applC" ("_position" mds) ("_position" AsmNoRead)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "SIFUM_Type_Systems.TypeSystem"
### 5.167s elapsed time, 10.260s cpu time, 0.824s GC time
### Metis: Falling back on "metis (full_types)"...
### Metis: Falling back on "metis (full_types)"...
### Ambiguous input (line 977 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_k_abv_indexed"
###     ("_tuple" ("_position" cms\<^sub>2)
###       ("_tuple_arg" ("_position" mem\<^sub>2)))
###     ("_indexdefault")
###     ("_tuple" ("_position" cms\<^sub>2')
###       ("_tuple_arg" ("_position" mem\<^sub>2')))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_abv"
###     ("_tuple" ("_position" cms\<^sub>2)
###       ("_tuple_arg" ("_position" mem\<^sub>2)))
###     ("_tuple" ("_position" cms\<^sub>2')
###       ("_tuple_arg" ("_position" mem\<^sub>2')))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "Set.Collect_empty_eq"
### Ambiguous input (line 1933 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.meval_k_abv_indexed"
###       ("_tuple" ("_position" cms\<^sub>1)
###         ("_tuple_arg" ("_position" mem\<^sub>1)))
###       ("_index" ("_position" k))
###       ("_tuple" ("_position" cms\<^sub>1'')
###         ("_tuple_arg" ("_position" mem\<^sub>1''))))
###     ("\<^const>local.meval_k_abv_indexed"
###       ("_tuple" ("_position" cms\<^sub>1'')
###         ("_tuple_arg" ("_position" mem\<^sub>1'')))
###       ("_indexdefault")
###       ("_tuple" ("_position" cms\<^sub>1')
###         ("_tuple_arg" ("_position" mem\<^sub>1'))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.meval_k_abv_indexed"
###       ("_tuple" ("_position" cms\<^sub>1)
###         ("_tuple_arg" ("_position" mem\<^sub>1)))
###       ("_index" ("_position" k))
###       ("_tuple" ("_position" cms\<^sub>1'')
###         ("_tuple_arg" ("_position" mem\<^sub>1''))))
###     ("\<^const>local.meval_abv"
###       ("_tuple" ("_position" cms\<^sub>1'')
###         ("_tuple_arg" ("_position" mem\<^sub>1'')))
###       ("_tuple" ("_position" cms\<^sub>1')
###         ("_tuple_arg" ("_position" mem\<^sub>1'))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1935 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_k_abv_indexed"
###     ("_tuple" ("_position" cms\<^sub>1'')
###       ("_tuple_arg" ("_position" mem\<^sub>1'')))
###     ("_indexdefault")
###     ("_tuple" ("_position" cms\<^sub>1')
###       ("_tuple_arg" ("_position" mem\<^sub>1')))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.meval_abv"
###     ("_tuple" ("_position" cms\<^sub>1'')
###       ("_tuple_arg" ("_position" mem\<^sub>1'')))
###     ("_tuple" ("_position" cms\<^sub>1')
###       ("_tuple_arg" ("_position" mem\<^sub>1')))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1946 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" snd) ("_position" cms\<^sub>1')))
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" snd) ("_position" cms\<^sub>2'))))
###     ("\<^const>HOL.conj"
###       ("\<^const>local.meval_k_abv_indexed"
###         ("_tuple" ("_position" cms\<^sub>2'')
###           ("_tuple_arg" ("_position" mem\<^sub>2'')))
###         ("_indexdefault")
###         ("_tuple" ("_position" cms\<^sub>2')
###           ("_tuple_arg" ("_position" mem\<^sub>2'))))
###       ("_applC" ("_position" makes_compatible)
###         ("_cargs"
###           ("_tuple" ("_position" cms\<^sub>1')
###             ("_tuple_arg" ("_position" mem\<^sub>1')))
###           ("_cargs"
###             ("_tuple" ("_position" cms\<^sub>2')
###               ("_tuple_arg" ("_position" mem\<^sub>2')))
###             ("_position" mems')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" snd) ("_position" cms\<^sub>1')))
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" snd) ("_position" cms\<^sub>2'))))
###     ("\<^const>HOL.conj"
###       ("\<^const>local.meval_abv"
###         ("_tuple" ("_position" cms\<^sub>2'')
###           ("_tuple_arg" ("_position" mem\<^sub>2'')))
###         ("_tuple" ("_position" cms\<^sub>2')
###           ("_tuple_arg" ("_position" mem\<^sub>2'))))
###       ("_applC" ("_position" makes_compatible)
###         ("_cargs"
###           ("_tuple" ("_position" cms\<^sub>1')
###             ("_tuple_arg" ("_position" mem\<^sub>1')))
###           ("_cargs"
###             ("_tuple" ("_position" cms\<^sub>2')
###               ("_tuple_arg" ("_position" mem\<^sub>2')))
###             ("_position" mems')))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "local.loc_reach.refl", "Product_Type.surjective_pairing"
### Metis: Unused theorems: "local.dom_uniq_1"
### Metis: Unused theorems: "local.annotate.simps_1", "local.annotate.simps_2"
### Metis: Unused theorems: "local.annotate.simps_1", "local.annotate.simps_2"
### Metis: Unused theorems: "local.annotate.simps_1", "local.annotate.simps_2"
### Ambiguous input (line 215 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 238 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds\<^sub>2) ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds\<^sub>2)
###     ("_indexdefault") ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "local.while.hyps_1"
### Metis: Unused theorems: "local.while.hyps_1"
### Metis: Unused theorems: "local.while.hyps_1"
### Ambiguous input (line 255 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>2) ("_position" c\<^sub>1)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>2)
###     ("_indexdefault") ("_position" c\<^sub>1)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 261 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>Pure.all_binder"
###   ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###   ("_bigimpl"
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High)))
###       ("_asm"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))))
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###           ("_Update" ("_position" mem\<^sub>1)
###             ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###         ("_index" ("_position" \<Gamma>'))
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>2) ("_position" mds)
###           ("_Update" ("_position" mem\<^sub>2)
###             ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))))
### ("\<^const>Pure.all_binder"
###   ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###   ("_bigimpl"
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High)))
###       ("_asm"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.not_member" ("_position" x)
###             ("_applC" ("_position" mds) ("_position" AsmNoWrite))))))
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###           ("_Update" ("_position" mem\<^sub>1)
###             ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###         ("_index" ("_position" \<Gamma>'))
###         ("\<^const>local.conf_abv" ("_position" c\<^sub>2) ("_position" mds)
###           ("_Update" ("_position" mem\<^sub>2)
###             ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 266 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>2)))))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v)))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>2)))))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v)))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>2)))))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v)))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>2)))))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>local.\<R>\<^sub>1_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v)))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 297 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>local.\<R>\<^sub>2_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>2)))))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>local.\<R>\<^sub>2_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v)))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>local.\<R>\<^sub>2_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>2)))))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>local.\<R>\<^sub>2_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v)))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>local.\<R>\<^sub>2_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>2)))))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>local.\<R>\<^sub>2_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v)))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>local.\<R>\<^sub>2_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v\<^sub>2)))))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>local.\<R>\<^sub>2_abv_indexed"
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>1)
###               ("_updbind" ("_position" x) ("_position" v))))
###           ("_index" ("_position" \<Gamma>'))
###           ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###             ("_position" mds)
###             ("_Update" ("_position" mem\<^sub>2)
###               ("_updbind" ("_position" x) ("_position" v)))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 353 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 365 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 378 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>local.tyenv_eq_indexed"
###           ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" High))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder"
###         ("_idts" ("_position" v\<^sub>1) ("_position" v\<^sub>2))
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v\<^sub>1))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v\<^sub>2))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))
###     ("\<^const>HOL.implies"
###       ("\<^const>HOL.conj"
###         ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###           ("_position" Low))
###         ("\<^const>Set.not_member" ("_position" x)
###           ("_applC" ("_position" mds) ("_position" AsmNoWrite))))
###       ("\<^const>HOL.All_binder" ("_position" v)
###         ("\<^const>Set.member"
###           ("_tuple"
###             ("\<^const>local.conf_abv" ("_position" c\<^sub>1)
###               ("_position" mds)
###               ("_Update" ("_position" mem\<^sub>1)
###                 ("_updbind" ("_position" x) ("_position" v))))
###             ("_tuple_arg"
###               ("\<^const>local.conf_abv" ("_position" c\<^sub>2)
###                 ("_position" mds)
###                 ("_Update" ("_position" mem\<^sub>2)
###                   ("_updbind" ("_position" x) ("_position" v))))))
###           ("_applC" ("_position" \<R>) ("_position" \<Gamma>')))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 454 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" c') ("_position" Stop))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_position" Stop))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" c') ("_position" Stop))
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_position" Stop))
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 460 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" c') ("_position" Stop))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_position" Stop))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" c') ("_position" Stop))
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_position" Stop))
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 466 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" c') ("_position" Stop))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_position" Stop))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" c') ("_position" Stop))
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_position" Stop))
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 484 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))
###     ("\<^const>HOL.eq" ("_position" c')
###       ("_applC" ("_position" If)
###         ("_cargs" ("_position" e)
###           ("_cargs"
###             ("\<^const>Language.Stmt.Seq" ("_position" c)
###               ("_applC" ("_position" While)
###                 ("_cargs" ("_position" e) ("_position" c))))
###             ("_position" Stop)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))
###     ("\<^const>HOL.eq" ("_position" c')
###       ("_applC" ("_position" If)
###         ("_cargs" ("_position" e)
###           ("_cargs"
###             ("\<^const>Language.Stmt.Seq" ("_position" c)
###               ("_applC" ("_position" While)
###                 ("_cargs" ("_position" e) ("_position" c))))
###             ("_position" Stop)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_applC" ("_position" If)
###         ("_cargs" ("_position" e)
###           ("_cargs"
###             ("\<^const>Language.Stmt.Seq" ("_position" c)
###               ("_applC" ("_position" While)
###                 ("_cargs" ("_position" e) ("_position" c))))
###             ("_position" Stop)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_applC" ("_position" If)
###         ("_cargs" ("_position" e)
###           ("_cargs"
###             ("\<^const>Language.Stmt.Seq" ("_position" c)
###               ("_applC" ("_position" While)
###                 ("_cargs" ("_position" e) ("_position" c))))
###             ("_position" Stop)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 493 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1) ("_indexdefault")
###   ("_position" Stop))
### ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 494 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 495 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_position" c\<^sub>2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("_position" c\<^sub>2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>HOL.eq" ("_position" mds') ("_position" mds))
###     ("\<^const>HOL.eq" ("_position" c') ("_position" c\<^sub>2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###       ("_position" mds))
###     ("\<^const>HOL.eq" ("_position" c') ("_position" c\<^sub>2))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 499 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 502 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1') ("_position" mds')
###         ("_position" mem')))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1')
###         ("_position" c\<^sub>2)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1') ("_position" mds')
###         ("_position" mem')))
###     ("\<^const>HOL.eq" ("_position" c')
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1')
###         ("_position" c\<^sub>2)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 513 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1') ("_position" mds')
###         ("_position" mem')))
###     ("\<^const>HOL.eq" ("_position" c')
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1')
###         ("_position" c\<^sub>2)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1') ("_position" mds')
###         ("_position" mem')))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c') ("_indexdefault")
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1')
###         ("_position" c\<^sub>2)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 555 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>') ("_position" x)) ("_indexdefault")
###       ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>HOL.eq" ("_applC" ("_position" \<Gamma>') ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 628 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1) ("_indexdefault")
###   ("_position" Stop))
### ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 629 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 751 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 751 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 751 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mem\<^sub>1') ("_position" mem\<^sub>1)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mem\<^sub>1')
###     ("_indexdefault") ("_position" mem\<^sub>1)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 762 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 762 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 762 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mem\<^sub>1')
###     ("_Update" ("_position" mem\<^sub>1)
###       ("_updbind" ("_position" x)
###         ("_applC" ("_position" ev\<^sub>A)
###           ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mem\<^sub>1')
###     ("_indexdefault")
###     ("_Update" ("_position" mem\<^sub>1)
###       ("_updbind" ("_position" x)
###         ("_applC" ("_position" ev\<^sub>A)
###           ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 767 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_position" High)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_indexdefault") ("_position" High)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 772 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_indexdefault") ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 773 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" t) ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" t) ("_indexdefault")
###     ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 775 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_applC" ("_position" dma) ("_position" x))
###     ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" dma) ("_position" x)) ("_indexdefault")
###     ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 776 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" to_total)
###       ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###     ("_indexdefault") ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 778 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" v)
###     ("_applC" ("_position" aexp_vars) ("_position" e))
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" to_total)
###         ("_cargs" ("_position" \<Gamma>) ("_position" v)))
###       ("_position" Low))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" v)
###     ("_applC" ("_position" aexp_vars) ("_position" e))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" to_total)
###         ("_cargs" ("_position" \<Gamma>) ("_position" v)))
###       ("_indexdefault") ("_position" Low))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 793 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 793 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mem\<^sub>1')
###     ("_Update" ("_position" mem\<^sub>1)
###       ("_updbind" ("_position" x)
###         ("_applC" ("_position" ev\<^sub>A)
###           ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mem\<^sub>1')
###     ("_indexdefault")
###     ("_Update" ("_position" mem\<^sub>1)
###       ("_updbind" ("_position" x)
###         ("_applC" ("_position" ev\<^sub>A)
###           ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 797 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 797 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 797 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mem\<^sub>1')
###     ("_Update" ("_position" mem\<^sub>1)
###       ("_updbind" ("_position" x)
###         ("_applC" ("_position" ev\<^sub>A)
###           ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mem\<^sub>1')
###     ("_indexdefault")
###     ("_Update" ("_position" mem\<^sub>1)
###       ("_updbind" ("_position" x)
###         ("_applC" ("_position" ev\<^sub>A)
###           ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1061 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>2) ("_position" c\<^sub>1)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>2)
###     ("_indexdefault") ("_position" c\<^sub>1)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 831 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 831 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 831 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mem\<^sub>1')
###     ("_Update" ("_position" mem\<^sub>1)
###       ("_updbind" ("_position" x)
###         ("_applC" ("_position" ev\<^sub>A)
###           ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mem\<^sub>1')
###     ("_indexdefault")
###     ("_Update" ("_position" mem\<^sub>1)
###       ("_updbind" ("_position" x)
###         ("_applC" ("_position" ev\<^sub>A)
###           ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1157 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1) ("_indexdefault")
###   ("_position" Stop))
### ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1161 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 841 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>Pure.imp"
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" ev\<^sub>B)
###         ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###       ("_indexdefault")
###       ("_applC" ("_position" ev\<^sub>B)
###         ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
###   ("\<^const>HOL.Trueprop" ("_position" ?case)))
### ("\<^const>Pure.imp"
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" ev\<^sub>B)
###         ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###       ("_applC" ("_position" ev\<^sub>B)
###         ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
###   ("\<^const>HOL.Trueprop" ("_position" ?case)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "Set.mem_Collect_eq", "Product_Type.case_prodI"
### Ambiguous input (line 1173 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1174 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 926 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###     ("_applC" ("_position" If)
###       ("_cargs" ("_position" e)
###         ("_cargs"
###           ("\<^const>Language.Stmt.Seq" ("_position" c)
###             ("_applC" ("_position" While)
###               ("_cargs" ("_position" e) ("_position" c))))
###           ("_position" Stop))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault")
###     ("_applC" ("_position" If)
###       ("_cargs" ("_position" e)
###         ("_cargs"
###           ("\<^const>Language.Stmt.Seq" ("_position" c)
###             ("_applC" ("_position" While)
###               ("_cargs" ("_position" e) ("_position" c))))
###           ("_position" Stop))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 927 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 928 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mem\<^sub>1') ("_position" mem\<^sub>1)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mem\<^sub>1')
###     ("_indexdefault") ("_position" mem\<^sub>1)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1175 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1097 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1) ("_indexdefault")
###   ("_position" Stop))
### ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1098 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1099 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" cn)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" cn)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1099 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1099 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mem\<^sub>1') ("_position" mem\<^sub>1)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mem\<^sub>1')
###     ("_indexdefault") ("_position" mem\<^sub>1)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1106 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>2) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>2)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1122 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>) ("_position" x)) ("_indexdefault")
###       ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>))
###     ("\<^const>HOL.eq" ("_applC" ("_position" \<Gamma>) ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1128 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>) ("_position" x)) ("_indexdefault")
###       ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>))
###     ("\<^const>HOL.eq" ("_applC" ("_position" \<Gamma>) ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1128 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 986 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>\<^sub>1'))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>\<^sub>1') ("_position" x))
###       ("_indexdefault") ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>\<^sub>1'))
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" \<Gamma>\<^sub>1') ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 989 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>') ("_position" x)) ("_indexdefault")
###       ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>HOL.eq" ("_applC" ("_position" \<Gamma>') ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1137 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1''')
###       ("_position" cn))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1''')
###       ("_position" cn))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "local.intro\<^sub>2_1", "local.intro\<^sub>2_2", "local.intro\<^sub>2_3"
### Ambiguous input (line 1152 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1''')
###       ("_position" cn))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1''')
###       ("_position" cn))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 999 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1)
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 999 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>2)
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>2''')
###       ("_position" c))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>2)
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>2''')
###       ("_position" c))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1134 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>2) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>2)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1134 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1008 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c''))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1)
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c''))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1008 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>2)
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>2''')
###       ("_position" c''))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>2)
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>2''')
###       ("_position" c''))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1018 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c''))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1)
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###       ("_position" c''))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1018 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>2)
###     ("_indexdefault")
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>2''')
###       ("_position" c''))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>2)
###     ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>2''')
###       ("_position" c''))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1064 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1) ("_indexdefault")
###   ("_position" Stop))
### ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1065 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1078 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1'')
###         ("_position" mds') ("_position" mem\<^sub>1')))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###       ("_indexdefault")
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###         ("_position" c)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1'')
###         ("_position" mds') ("_position" mem\<^sub>1')))
###     ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###         ("_position" c)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1092 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1'')
###         ("_position" mds') ("_position" mem\<^sub>1')))
###     ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###         ("_position" c)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1'')
###         ("_position" mds') ("_position" mem\<^sub>1')))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###       ("_indexdefault")
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###         ("_position" c)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 865 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" t) ("_position" High)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" t) ("_indexdefault")
###     ("_position" High)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 917 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" t) ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" t) ("_indexdefault")
###     ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 918 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###     ("_indexdefault")
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 867 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>local.tyenv_eq_indexed"
###   ("_applC" ("_position" ev\<^sub>B)
###     ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###   ("_indexdefault")
###   ("_applC" ("_position" ev\<^sub>B)
###     ("_cargs" ("_position" mem\<^sub>2) ("_position" e))))
### ("\<^const>HOL.eq"
###   ("_applC" ("_position" ev\<^sub>B)
###     ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###   ("_applC" ("_position" ev\<^sub>B)
###     ("_cargs" ("_position" mem\<^sub>2) ("_position" e))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 868 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###     ("_indexdefault")
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 872 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" t) ("_position" High)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" t) ("_indexdefault")
###     ("_position" High)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 877 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" th)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" th)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "local.if_type_8"
### Ambiguous input (line 884 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>') ("_position" x)) ("_indexdefault")
###       ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>HOL.eq" ("_applC" ("_position" \<Gamma>') ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 885 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" t) ("_position" High)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" t) ("_indexdefault")
###     ("_position" High)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 888 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>') ("_position" x)) ("_indexdefault")
###       ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>HOL.eq" ("_applC" ("_position" \<Gamma>') ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 895 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" el)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" el)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 904 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>') ("_position" x)) ("_indexdefault")
###       ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>HOL.eq" ("_applC" ("_position" \<Gamma>') ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 905 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" t) ("_position" High)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" t) ("_indexdefault")
###     ("_position" High)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 909 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>local.tyenv_eq_indexed"
###       ("_applC" ("_position" \<Gamma>') ("_position" x)) ("_indexdefault")
###       ("_applC" ("_position" Some) ("_position" High)))))
### ("\<^const>HOL.Trueprop"
###   ("_Ball" ("_position" x)
###     ("_applC" ("_position" dom) ("_position" \<Gamma>'))
###     ("\<^const>HOL.eq" ("_applC" ("_position" \<Gamma>') ("_position" x))
###       ("_applC" ("_position" Some) ("_position" High)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 913 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" el)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" el)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "local.if_type_8"
### Ambiguous input (line 892 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" th)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" th)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 843 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###     ("_indexdefault")
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###     ("_applC" ("_position" ev\<^sub>B)
###       ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 846 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" th)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" th)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "local.if_type_8"
### Ambiguous input (line 850 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" el)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" el)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Metis: Unused theorems: "local.if_type_8"
### Ambiguous input (line 814 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" to_total)
###       ("_cargs"
###         ("_MapUpd" ("_position" \<Gamma>)
###           ("_maplet" ("_position" x) ("_position" t)))
###         ("_position" x)))
###     ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" to_total)
###       ("_cargs"
###         ("_MapUpd" ("_position" \<Gamma>)
###           ("_maplet" ("_position" x) ("_position" t)))
###         ("_position" x)))
###     ("_indexdefault") ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 815 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>Pure.all_binder" ("_position" x)
###   ("\<^const>Pure.imp"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" aexp_vars) ("_position" e))))
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>HOL.eq"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_position" Low)))))
### ("\<^const>Pure.all_binder" ("_position" x)
###   ("\<^const>Pure.imp"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.member" ("_position" x)
###         ("_applC" ("_position" aexp_vars) ("_position" e))))
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>local.tyenv_eq_indexed"
###         ("_applC" ("_position" to_total)
###           ("_cargs" ("_position" \<Gamma>) ("_position" x)))
###         ("_indexdefault") ("_position" Low)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 817 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" ev\<^sub>A)
###       ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###     ("_indexdefault")
###     ("_applC" ("_position" ev\<^sub>A)
###       ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" ev\<^sub>A)
###       ("_cargs" ("_position" mem\<^sub>1) ("_position" e)))
###     ("_applC" ("_position" ev\<^sub>A)
###       ("_cargs" ("_position" mem\<^sub>2) ("_position" e)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 821 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" to_total)
###       ("_cargs"
###         ("_MapUpd" ("_position" \<Gamma>)
###           ("_maplet" ("_position" x) ("_position" t)))
###         ("_position" y)))
###     ("_position" Low)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" to_total)
###       ("_cargs"
###         ("_MapUpd" ("_position" \<Gamma>)
###           ("_maplet" ("_position" x) ("_position" t)))
###         ("_position" y)))
###     ("_indexdefault") ("_position" Low)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 822 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed"
###     ("_applC" ("_position" mem\<^sub>1) ("_position" y)) ("_indexdefault")
###     ("_applC" ("_position" mem\<^sub>2) ("_position" y))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_applC" ("_position" mem\<^sub>1) ("_position" y))
###     ("_applC" ("_position" mem\<^sub>2) ("_position" y))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 690 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1) ("_indexdefault")
###   ("_position" Stop))
### ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 691 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 692 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1') ("_position" c\<^sub>2)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###     ("_indexdefault") ("_position" c\<^sub>2)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 692 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mds') ("_position" mds)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mds') ("_indexdefault")
###     ("_position" mds)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 692 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" mem\<^sub>1') ("_position" mem\<^sub>1)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" mem\<^sub>1')
###     ("_indexdefault") ("_position" mem\<^sub>1)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 695 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 707 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 712 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1'')
###         ("_position" mds') ("_position" mem\<^sub>1')))
###     ("\<^const>HOL.eq" ("_position" c\<^sub>1')
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###         ("_position" c\<^sub>2)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.conj"
###     ("\<^const>local.eval_abv2"
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
###         ("_position" mem\<^sub>1))
###       ("\<^const>local.conf_abv" ("_position" c\<^sub>1'')
###         ("_position" mds') ("_position" mem\<^sub>1')))
###     ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
###       ("_indexdefault")
###       ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
###         ("_position" c\<^sub>2)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1072 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 1074 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
###     ("_indexdefault") ("_position" Stop)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SIFUM_Type_Systems/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SIFUM_Type_Systems/outline -o pdf -n outline -t /proof,/ML
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  subst_abv mem ::
***   ('Var \<Rightarrow> 'Val option) \<Rightarrow> 'Var \<Rightarrow> 'Val
*** Operand:   {} :: ??'a set
*** 
*** At command "have" (line 288 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy")