Mctt.Frontend.Parser

From Coq Require Import List Arith.PeanoNat String.

From Mctt Require Import Syntax.

Parameter loc : Type.

From Coq.extraction Require Extraction.
From Coq.Lists Require List.
From Coq.PArith Require Import BinPos.
From Coq.NArith Require Import BinNat.
From MenhirLib Require Main.
From MenhirLib Require Version.
Import List.ListNotations.

Definition version_check : unit := MenhirLib.Version.require_20240715.

Unset Elimination Schemes.

Inductive token : Type :=
| ZERO : (loc)%type -> token
| VAR : (loc*string)%type -> token
| TYPE : (loc)%type -> token
| SUCC : (loc)%type -> token
| RPAREN : (loc)%type -> token
| RETURN : (loc)%type -> token
| REFL : (loc)%type -> token
| REC : (loc)%type -> token
| RANGLE : (loc)%type -> token
| PI : (loc)%type -> token
| NAT : (loc)%type -> token
| LPAREN : (loc)%type -> token
| LET : (loc)%type -> token
| LANGLE : (loc)%type -> token
| LAMBDA : (loc)%type -> token
| INT : (loc*nat)%type -> token
| IN : (loc)%type -> token
| EQ : (loc)%type -> token
| EOF : (loc)%type -> token
| END : (loc)%type -> token
| DOT : (loc)%type -> token
| DEF : (loc)%type -> token
| DARROW : (loc)%type -> token
| COMMA : (loc)%type -> token
| COLON : (loc)%type -> token
| BAR : (loc)%type -> token
| AT : (loc)%type -> token
| AS : (loc)%type -> token
| ARROW : (loc)%type -> token.

Module Import Gram <: MenhirLib.Grammar.T.

Local Obligation Tactic := let x := fresh in intro x; case x; reflexivity.

Inductive terminal' : Set :=
| ARROW't
| AS't
| AT't
| BAR't
| COLON't
| COMMA't
| DARROW't
| DEF't
| DOT't
| END't
| EOF't
| EQ't
| IN't
| INT't
| LAMBDA't
| LANGLE't
| LET't
| LPAREN't
| NAT't
| PI't
| RANGLE't
| REC't
| REFL't
| RETURN't
| RPAREN't
| SUCC't
| TYPE't
| VAR't
| ZERO't.
Definition terminal := terminal'.

Global Program Instance terminalNum : MenhirLib.Alphabet.Numbered terminal :=
  { inj := fun x => match x return _ with
    | ARROW't => 1%positive
    | AS't => 2%positive
    | AT't => 3%positive
    | BAR't => 4%positive
    | COLON't => 5%positive
    | COMMA't => 6%positive
    | DARROW't => 7%positive
    | DEF't => 8%positive
    | DOT't => 9%positive
    | END't => 10%positive
    | EOF't => 11%positive
    | EQ't => 12%positive
    | IN't => 13%positive
    | INT't => 14%positive
    | LAMBDA't => 15%positive
    | LANGLE't => 16%positive
    | LET't => 17%positive
    | LPAREN't => 18%positive
    | NAT't => 19%positive
    | PI't => 20%positive
    | RANGLE't => 21%positive
    | REC't => 22%positive
    | REFL't => 23%positive
    | RETURN't => 24%positive
    | RPAREN't => 25%positive
    | SUCC't => 26%positive
    | TYPE't => 27%positive
    | VAR't => 28%positive
    | ZERO't => 29%positive
    end;
    surj := (fun n => match n return _ with
    | 1%positive => ARROW't
    | 2%positive => AS't
    | 3%positive => AT't
    | 4%positive => BAR't
    | 5%positive => COLON't
    | 6%positive => COMMA't
    | 7%positive => DARROW't
    | 8%positive => DEF't
    | 9%positive => DOT't
    | 10%positive => END't
    | 11%positive => EOF't
    | 12%positive => EQ't
    | 13%positive => IN't
    | 14%positive => INT't
    | 15%positive => LAMBDA't
    | 16%positive => LANGLE't
    | 17%positive => LET't
    | 18%positive => LPAREN't
    | 19%positive => NAT't
    | 20%positive => PI't
    | 21%positive => RANGLE't
    | 22%positive => REC't
    | 23%positive => REFL't
    | 24%positive => RETURN't
    | 25%positive => RPAREN't
    | 26%positive => SUCC't
    | 27%positive => TYPE't
    | 28%positive => VAR't
    | 29%positive => ZERO't
    | _ => ARROW't
    end)%Z;
    inj_bound := 29%positive }.
Global Instance TerminalAlph : MenhirLib.Alphabet.Alphabet terminal := _.

Inductive nonterminal' : Set :=
| app_obj'nt
| atomic_obj'nt
| eq_obj'nt
| fnbinder'nt
| let_defn'nt
| let_defns'nt
| obj'nt
| optional_as_nat'nt
| param'nt
| params'nt
| prog'nt.
Definition nonterminal := nonterminal'.

Global Program Instance nonterminalNum : MenhirLib.Alphabet.Numbered nonterminal :=
  { inj := fun x => match x return _ with
    | app_obj'nt => 1%positive
    | atomic_obj'nt => 2%positive
    | eq_obj'nt => 3%positive
    | fnbinder'nt => 4%positive
    | let_defn'nt => 5%positive
    | let_defns'nt => 6%positive
    | obj'nt => 7%positive
    | optional_as_nat'nt => 8%positive
    | param'nt => 9%positive
    | params'nt => 10%positive
    | prog'nt => 11%positive
    end;
    surj := (fun n => match n return _ with
    | 1%positive => app_obj'nt
    | 2%positive => atomic_obj'nt
    | 3%positive => eq_obj'nt
    | 4%positive => fnbinder'nt
    | 5%positive => let_defn'nt
    | 6%positive => let_defns'nt
    | 7%positive => obj'nt
    | 8%positive => optional_as_nat'nt
    | 9%positive => param'nt
    | 10%positive => params'nt
    | 11%positive => prog'nt
    | _ => app_obj'nt
    end)%Z;
    inj_bound := 11%positive }.
Global Instance NonTerminalAlph : MenhirLib.Alphabet.Alphabet nonterminal := _.

Include MenhirLib.Grammar.Symbol.

Definition terminal_semantic_type (t:terminal) : Type:=
  match t with
  | ZERO't => (loc)%type
  | VAR't => (loc*string)%type
  | TYPE't => (loc)%type
  | SUCC't => (loc)%type
  | RPAREN't => (loc)%type
  | RETURN't => (loc)%type
  | REFL't => (loc)%type
  | REC't => (loc)%type
  | RANGLE't => (loc)%type
  | PI't => (loc)%type
  | NAT't => (loc)%type
  | LPAREN't => (loc)%type
  | LET't => (loc)%type
  | LANGLE't => (loc)%type
  | LAMBDA't => (loc)%type
  | INT't => (loc*nat)%type
  | IN't => (loc)%type
  | EQ't => (loc)%type
  | EOF't => (loc)%type
  | END't => (loc)%type
  | DOT't => (loc)%type
  | DEF't => (loc)%type
  | DARROW't => (loc)%type
  | COMMA't => (loc)%type
  | COLON't => (loc)%type
  | BAR't => (loc)%type
  | AT't => (loc)%type
  | AS't => (loc)%type
  | ARROW't => (loc)%type
  end.

Definition nonterminal_semantic_type (nt:nonterminal) : Type:=
  match nt with
  | prog'nt => (Cst.obj * Cst.obj)%type
  | params'nt => (list (string * Cst.obj))%type
  | param'nt => (string * Cst.obj)%type
  | optional_as_nat'nt => (unit)%type
  | obj'nt => (Cst.obj)%type
  | let_defns'nt => (list ((string * Cst.obj) * Cst.obj))%type
  | let_defn'nt => ((string * Cst.obj) * Cst.obj)%type
  | fnbinder'nt => (string -> Cst.obj -> Cst.obj -> Cst.obj)%type
  | eq_obj'nt => (Cst.obj)%type
  | atomic_obj'nt => (Cst.obj)%type
  | app_obj'nt => (Cst.obj)%type
  end.

Definition symbol_semantic_type (s:symbol) : Type:=
  match s with
  | T t => terminal_semantic_type t
  | NT nt => nonterminal_semantic_type nt
  end.

Definition token := token.

Definition token_term (tok : token) : terminal :=
  match tok with
  | ZERO _ => ZERO't
  | VAR _ => VAR't
  | TYPE _ => TYPE't
  | SUCC _ => SUCC't
  | RPAREN _ => RPAREN't
  | RETURN _ => RETURN't
  | REFL _ => REFL't
  | REC _ => REC't
  | RANGLE _ => RANGLE't
  | PI _ => PI't
  | NAT _ => NAT't
  | LPAREN _ => LPAREN't
  | LET _ => LET't
  | LANGLE _ => LANGLE't
  | LAMBDA _ => LAMBDA't
  | INT _ => INT't
  | IN _ => IN't
  | EQ _ => EQ't
  | EOF _ => EOF't
  | END _ => END't
  | DOT _ => DOT't
  | DEF _ => DEF't
  | DARROW _ => DARROW't
  | COMMA _ => COMMA't
  | COLON _ => COLON't
  | BAR _ => BAR't
  | AT _ => AT't
  | AS _ => AS't
  | ARROW _ => ARROW't
  end.

Definition token_sem (tok : token) : symbol_semantic_type (T (token_term tok)) :=
  match tok with
  | ZERO x => x
  | VAR x => x
  | TYPE x => x
  | SUCC x => x
  | RPAREN x => x
  | RETURN x => x
  | REFL x => x
  | REC x => x
  | RANGLE x => x
  | PI x => x
  | NAT x => x
  | LPAREN x => x
  | LET x => x
  | LANGLE x => x
  | LAMBDA x => x
  | INT x => x
  | IN x => x
  | EQ x => x
  | EOF x => x
  | END x => x
  | DOT x => x
  | DEF x => x
  | DARROW x => x
  | COMMA x => x
  | COLON x => x
  | BAR x => x
  | AT x => x
  | AS x => x
  | ARROW x => x
  end.

Inductive production' : Set :=
| Prod'prog'0
| Prod'params'1
| Prod'params'0
| Prod'param'0
| Prod'optional_as_nat'1
| Prod'optional_as_nat'0
| Prod'obj'6
| Prod'obj'5
| Prod'obj'4
| Prod'obj'3
| Prod'obj'2
| Prod'obj'1
| Prod'obj'0
| Prod'let_defns'1
| Prod'let_defns'0
| Prod'let_defn'0
| Prod'fnbinder'1
| Prod'fnbinder'0
| Prod'eq_obj'1
| Prod'eq_obj'0
| Prod'atomic_obj'5
| Prod'atomic_obj'4
| Prod'atomic_obj'3
| Prod'atomic_obj'2
| Prod'atomic_obj'1
| Prod'atomic_obj'0
| Prod'app_obj'1
| Prod'app_obj'0.
Definition production := production'.

Global Program Instance productionNum : MenhirLib.Alphabet.Numbered production :=
  { inj := fun x => match x return _ with
    | Prod'prog'0 => 1%positive
    | Prod'params'1 => 2%positive
    | Prod'params'0 => 3%positive
    | Prod'param'0 => 4%positive
    | Prod'optional_as_nat'1 => 5%positive
    | Prod'optional_as_nat'0 => 6%positive
    | Prod'obj'6 => 7%positive
    | Prod'obj'5 => 8%positive
    | Prod'obj'4 => 9%positive
    | Prod'obj'3 => 10%positive
    | Prod'obj'2 => 11%positive
    | Prod'obj'1 => 12%positive
    | Prod'obj'0 => 13%positive
    | Prod'let_defns'1 => 14%positive
    | Prod'let_defns'0 => 15%positive
    | Prod'let_defn'0 => 16%positive
    | Prod'fnbinder'1 => 17%positive
    | Prod'fnbinder'0 => 18%positive
    | Prod'eq_obj'1 => 19%positive
    | Prod'eq_obj'0 => 20%positive
    | Prod'atomic_obj'5 => 21%positive
    | Prod'atomic_obj'4 => 22%positive
    | Prod'atomic_obj'3 => 23%positive
    | Prod'atomic_obj'2 => 24%positive
    | Prod'atomic_obj'1 => 25%positive
    | Prod'atomic_obj'0 => 26%positive
    | Prod'app_obj'1 => 27%positive
    | Prod'app_obj'0 => 28%positive
    end;
    surj := (fun n => match n return _ with
    | 1%positive => Prod'prog'0
    | 2%positive => Prod'params'1
    | 3%positive => Prod'params'0
    | 4%positive => Prod'param'0
    | 5%positive => Prod'optional_as_nat'1
    | 6%positive => Prod'optional_as_nat'0
    | 7%positive => Prod'obj'6
    | 8%positive => Prod'obj'5
    | 9%positive => Prod'obj'4
    | 10%positive => Prod'obj'3
    | 11%positive => Prod'obj'2
    | 12%positive => Prod'obj'1
    | 13%positive => Prod'obj'0
    | 14%positive => Prod'let_defns'1
    | 15%positive => Prod'let_defns'0
    | 16%positive => Prod'let_defn'0
    | 17%positive => Prod'fnbinder'1
    | 18%positive => Prod'fnbinder'0
    | 19%positive => Prod'eq_obj'1
    | 20%positive => Prod'eq_obj'0
    | 21%positive => Prod'atomic_obj'5
    | 22%positive => Prod'atomic_obj'4
    | 23%positive => Prod'atomic_obj'3
    | 24%positive => Prod'atomic_obj'2
    | 25%positive => Prod'atomic_obj'1
    | 26%positive => Prod'atomic_obj'0
    | 27%positive => Prod'app_obj'1
    | 28%positive => Prod'app_obj'0
    | _ => Prod'prog'0
    end)%Z;
    inj_bound := 28%positive }.
Global Instance ProductionAlph : MenhirLib.Alphabet.Alphabet production := _.

Definition prod_contents (p:production) :
  { p:nonterminal * list symbol &
    MenhirLib.Grammar.arrows_right
      (symbol_semantic_type (NT (fst p)))
      (List.map symbol_semantic_type (snd p)) }
 :=
  let box := existT (fun p =>
    MenhirLib.Grammar.arrows_right
      (symbol_semantic_type (NT (fst p)))
      (List.map symbol_semantic_type (snd p)) )
  in
  match p with
  | Prod'app_obj'0 => box
    (app_obj'nt, [NT atomic_obj'nt; NT app_obj'nt]%list)
    (fun atomic_obj app_obj =>
                                 ( Cst.app app_obj atomic_obj )
)
  | Prod'app_obj'1 => box
    (app_obj'nt, [NT atomic_obj'nt]%list)
    (fun atomic_obj =>
atomic_obj
)
  | Prod'atomic_obj'0 => box
    (atomic_obj'nt, [T INT't; T AT't; T TYPE't]%list)
    (fun n _2 _1 =>
                        ( Cst.typ (snd n) )
)
  | Prod'atomic_obj'1 => box
    (atomic_obj'nt, [T NAT't]%list)
    (fun _1 =>
         ( Cst.nat )
)
  | Prod'atomic_obj'2 => box
    (atomic_obj'nt, [T ZERO't]%list)
    (fun _1 =>
          ( Cst.zero )
)
  | Prod'atomic_obj'3 => box
    (atomic_obj'nt, [T INT't]%list)
    (fun n =>
             ( nat_rect (fun _ => Cst.obj) Cst.zero (fun _ => Cst.succ) (snd n) )
)
  | Prod'atomic_obj'4 => box
    (atomic_obj'nt, [T VAR't]%list)
    (fun x =>
             ( Cst.var (snd x) )
)
  | Prod'atomic_obj'5 => box
    (atomic_obj'nt, [T RPAREN't; NT obj'nt; T LPAREN't]%list)
    (fun _3 obj _1 =>
obj
)
  | Prod'eq_obj'0 => box
    (eq_obj'nt, [NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt]%list)
    (fun rhs _5 typ _3 _2 lhs =>
                                                            ( Cst.prop_eq lhs typ rhs )
)
  | Prod'eq_obj'1 => box
    (eq_obj'nt, [NT app_obj'nt]%list)
    (fun app_obj =>
app_obj
)
  | Prod'fnbinder'0 => box
    (fnbinder'nt, [T PI't]%list)
    (fun _1 =>
        ( Cst.pi )
)
  | Prod'fnbinder'1 => box
    (fnbinder'nt, [T LAMBDA't]%list)
    (fun _1 =>
            ( Cst.fn )
)
  | Prod'let_defn'0 => box
    (let_defn'nt, [T RPAREN't; NT obj'nt; T DEF't; NT param'nt; T LPAREN't]%list)
    (fun _5 obj _3 param _1 =>
                                        ( (param, obj) )
)
  | Prod'let_defns'0 => box
    (let_defns'nt, [NT let_defn'nt; NT let_defns'nt]%list)
    (fun let_defn let_defns =>
                                 ( let_defn :: let_defns )
)
  | Prod'let_defns'1 => box
    (let_defns'nt, [NT let_defn'nt]%list)
    (fun let_defn =>
                  ( [let_defn] )
)
  | Prod'obj'0 => box
    (obj'nt, [NT obj'nt; T ARROW't; NT params'nt; NT fnbinder'nt]%list)
    (fun obj _3 params fnbinder =>
                                             ( List.fold_left (fun acc arg => fnbinder (fst arg) (snd arg) acc) params obj )
)
  | Prod'obj'1 => box
    (obj'nt, [NT eq_obj'nt]%list)
    (fun eq_obj =>
eq_obj
)
  | Prod'obj'2 => box
    (obj'nt, [T END't; NT obj'nt; T DARROW't; T VAR't; T COMMA't; T VAR't; T SUCC't; T BAR't; NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list)
    (fun _19 es _17 sr _15 sx _13 _12 ez _10 _9 _8 em _6 mx _4 _3 escr _1 =>
         ( Cst.natrec escr (snd mx) em ez (snd sx) (snd sr) es )
)
  | Prod'obj'3 => box
    (obj'nt, [T END't; NT obj'nt; T DARROW't; T VAR't; T REFL't; T BAR't; NT obj'nt; T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list)
    (fun _23 er _21 rx _19 _18 em _16 mz my mx _12 _11 rhs _9 typ _7 _6 lhs _4 _3 escr _1 =>
         ( Cst.eqrec escr (snd mx) (snd my) (snd mz) em (snd rx) er lhs typ rhs )
)
  | Prod'obj'4 => box
    (obj'nt, [NT atomic_obj'nt; NT atomic_obj'nt; T REFL't]%list)
    (fun e typ _1 =>
                                            ( Cst.refl typ e )
)
  | Prod'obj'5 => box
    (obj'nt, [NT atomic_obj'nt; T SUCC't]%list)
    (fun atomic_obj _1 =>
                          ( Cst.succ atomic_obj )
)
  | Prod'obj'6 => box
    (obj'nt, [NT obj'nt; T IN't; NT let_defns'nt; T LET't]%list)
    (fun body _3 ds _1 =>
                                         ( List.fold_left (fun acc arg => Cst.app acc (snd arg)) (List.rev ds) (List.fold_left (fun acc arg => Cst.fn (fst (fst arg)) (snd (fst arg)) acc) ds body) )
)
  | Prod'optional_as_nat'0 => box
    (optional_as_nat'nt, [T NAT't; T AS't]%list)
    (fun _2 _1 =>
             ( tt )
)
  | Prod'optional_as_nat'1 => box
    (optional_as_nat'nt, []%list)
    (
    ( tt )
)
  | Prod'param'0 => box
    (param'nt, [T RPAREN't; NT obj'nt; T COLON't; T VAR't; T LPAREN't]%list)
    (fun _5 obj _3 x _1 =>
                                     ( (snd x, obj) )
)
  | Prod'params'0 => box
    (params'nt, [NT param'nt; NT params'nt]%list)
    (fun param params =>
                           ( param :: params )
)
  | Prod'params'1 => box
    (params'nt, [NT param'nt]%list)
    (fun param =>
               ( [param] )
)
  | Prod'prog'0 => box
    (prog'nt, [T EOF't; NT obj'nt; T COLON't; NT obj'nt]%list)
    (fun _4 typ _2 exp =>
(exp, typ)
)
  end.

Definition prod_lhs (p:production) :=
  fst (projT1 (prod_contents p)).
Definition prod_rhs_rev (p:production) :=
  snd (projT1 (prod_contents p)).
Definition prod_action (p:production) :=
  projT2 (prod_contents p).

Include MenhirLib.Grammar.Defs.

End Gram.

Module Aut <: MenhirLib.Automaton.T.

Local Obligation Tactic := let x := fresh in intro x; case x; reflexivity.

Module Gram := Gram.
Module GramDefs := Gram.

Definition nullable_nterm (nt:nonterminal) : bool :=
  match nt with
  | prog'nt => false
  | params'nt => false
  | param'nt => false
  | optional_as_nat'nt => true
  | obj'nt => false
  | let_defns'nt => false
  | let_defn'nt => false
  | fnbinder'nt => false
  | eq_obj'nt => false
  | atomic_obj'nt => false
  | app_obj'nt => false
  end.

Definition first_nterm (nt:nonterminal) : list terminal :=
  match nt with
  | prog'nt => [ZERO't; VAR't; TYPE't; SUCC't; REFL't; REC't; PI't; NAT't; LPAREN't; LET't; LAMBDA't; INT't]%list
  | params'nt => [LPAREN't]%list
  | param'nt => [LPAREN't]%list
  | optional_as_nat'nt => [AS't]%list
  | obj'nt => [ZERO't; VAR't; TYPE't; SUCC't; REFL't; REC't; PI't; NAT't; LPAREN't; LET't; LAMBDA't; INT't]%list
  | let_defns'nt => [LPAREN't]%list
  | let_defn'nt => [LPAREN't]%list
  | fnbinder'nt => [PI't; LAMBDA't]%list
  | eq_obj'nt => [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't]%list
  | atomic_obj'nt => [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't]%list
  | app_obj'nt => [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't]%list
  end.

Inductive noninitstate' : Set :=
| Nis'94
| Nis'93
| Nis'92
| Nis'91
| Nis'89
| Nis'88
| Nis'87
| Nis'86
| Nis'85
| Nis'84
| Nis'83
| Nis'82
| Nis'81
| Nis'80
| Nis'79
| Nis'78
| Nis'77
| Nis'76
| Nis'75
| Nis'74
| Nis'73
| Nis'72
| Nis'71
| Nis'70
| Nis'69
| Nis'68
| Nis'67
| Nis'66
| Nis'65
| Nis'64
| Nis'63
| Nis'62
| Nis'61
| Nis'60
| Nis'59
| Nis'58
| Nis'57
| Nis'56
| Nis'55
| Nis'54
| Nis'53
| Nis'52
| Nis'51
| Nis'50
| Nis'49
| Nis'48
| Nis'47
| Nis'46
| Nis'45
| Nis'44
| Nis'43
| Nis'42
| Nis'41
| Nis'40
| Nis'39
| Nis'38
| Nis'37
| Nis'36
| Nis'35
| Nis'34
| Nis'33
| Nis'32
| Nis'31
| Nis'30
| Nis'29
| Nis'28
| Nis'27
| Nis'26
| Nis'25
| Nis'24
| Nis'23
| Nis'22
| Nis'21
| Nis'20
| Nis'19
| Nis'18
| Nis'17
| Nis'16
| Nis'15
| Nis'14
| Nis'13
| Nis'12
| Nis'11
| Nis'10
| Nis'9
| Nis'8
| Nis'7
| Nis'6
| Nis'5
| Nis'4
| Nis'3
| Nis'2
| Nis'1.
Definition noninitstate := noninitstate'.

Global Program Instance noninitstateNum : MenhirLib.Alphabet.Numbered noninitstate :=
  { inj := fun x => match x return _ with
    | Nis'94 => 1%positive
    | Nis'93 => 2%positive
    | Nis'92 => 3%positive
    | Nis'91 => 4%positive
    | Nis'89 => 5%positive
    | Nis'88 => 6%positive
    | Nis'87 => 7%positive
    | Nis'86 => 8%positive
    | Nis'85 => 9%positive
    | Nis'84 => 10%positive
    | Nis'83 => 11%positive
    | Nis'82 => 12%positive
    | Nis'81 => 13%positive
    | Nis'80 => 14%positive
    | Nis'79 => 15%positive
    | Nis'78 => 16%positive
    | Nis'77 => 17%positive
    | Nis'76 => 18%positive
    | Nis'75 => 19%positive
    | Nis'74 => 20%positive
    | Nis'73 => 21%positive
    | Nis'72 => 22%positive
    | Nis'71 => 23%positive
    | Nis'70 => 24%positive
    | Nis'69 => 25%positive
    | Nis'68 => 26%positive
    | Nis'67 => 27%positive
    | Nis'66 => 28%positive
    | Nis'65 => 29%positive
    | Nis'64 => 30%positive
    | Nis'63 => 31%positive
    | Nis'62 => 32%positive
    | Nis'61 => 33%positive
    | Nis'60 => 34%positive
    | Nis'59 => 35%positive
    | Nis'58 => 36%positive
    | Nis'57 => 37%positive
    | Nis'56 => 38%positive
    | Nis'55 => 39%positive
    | Nis'54 => 40%positive
    | Nis'53 => 41%positive
    | Nis'52 => 42%positive
    | Nis'51 => 43%positive
    | Nis'50 => 44%positive
    | Nis'49 => 45%positive
    | Nis'48 => 46%positive
    | Nis'47 => 47%positive
    | Nis'46 => 48%positive
    | Nis'45 => 49%positive
    | Nis'44 => 50%positive
    | Nis'43 => 51%positive
    | Nis'42 => 52%positive
    | Nis'41 => 53%positive
    | Nis'40 => 54%positive
    | Nis'39 => 55%positive
    | Nis'38 => 56%positive
    | Nis'37 => 57%positive
    | Nis'36 => 58%positive
    | Nis'35 => 59%positive
    | Nis'34 => 60%positive
    | Nis'33 => 61%positive
    | Nis'32 => 62%positive
    | Nis'31 => 63%positive
    | Nis'30 => 64%positive
    | Nis'29 => 65%positive
    | Nis'28 => 66%positive
    | Nis'27 => 67%positive
    | Nis'26 => 68%positive
    | Nis'25 => 69%positive
    | Nis'24 => 70%positive
    | Nis'23 => 71%positive
    | Nis'22 => 72%positive
    | Nis'21 => 73%positive
    | Nis'20 => 74%positive
    | Nis'19 => 75%positive
    | Nis'18 => 76%positive
    | Nis'17 => 77%positive
    | Nis'16 => 78%positive
    | Nis'15 => 79%positive
    | Nis'14 => 80%positive
    | Nis'13 => 81%positive
    | Nis'12 => 82%positive
    | Nis'11 => 83%positive
    | Nis'10 => 84%positive
    | Nis'9 => 85%positive
    | Nis'8 => 86%positive
    | Nis'7 => 87%positive
    | Nis'6 => 88%positive
    | Nis'5 => 89%positive
    | Nis'4 => 90%positive
    | Nis'3 => 91%positive
    | Nis'2 => 92%positive
    | Nis'1 => 93%positive
    end;
    surj := (fun n => match n return _ with
    | 1%positive => Nis'94
    | 2%positive => Nis'93
    | 3%positive => Nis'92
    | 4%positive => Nis'91
    | 5%positive => Nis'89
    | 6%positive => Nis'88
    | 7%positive => Nis'87
    | 8%positive => Nis'86
    | 9%positive => Nis'85
    | 10%positive => Nis'84
    | 11%positive => Nis'83
    | 12%positive => Nis'82
    | 13%positive => Nis'81
    | 14%positive => Nis'80
    | 15%positive => Nis'79
    | 16%positive => Nis'78
    | 17%positive => Nis'77
    | 18%positive => Nis'76
    | 19%positive => Nis'75
    | 20%positive => Nis'74
    | 21%positive => Nis'73
    | 22%positive => Nis'72
    | 23%positive => Nis'71
    | 24%positive => Nis'70
    | 25%positive => Nis'69
    | 26%positive => Nis'68
    | 27%positive => Nis'67
    | 28%positive => Nis'66
    | 29%positive => Nis'65
    | 30%positive => Nis'64
    | 31%positive => Nis'63
    | 32%positive => Nis'62
    | 33%positive => Nis'61
    | 34%positive => Nis'60
    | 35%positive => Nis'59
    | 36%positive => Nis'58
    | 37%positive => Nis'57
    | 38%positive => Nis'56
    | 39%positive => Nis'55
    | 40%positive => Nis'54
    | 41%positive => Nis'53
    | 42%positive => Nis'52
    | 43%positive => Nis'51
    | 44%positive => Nis'50
    | 45%positive => Nis'49
    | 46%positive => Nis'48
    | 47%positive => Nis'47
    | 48%positive => Nis'46
    | 49%positive => Nis'45
    | 50%positive => Nis'44
    | 51%positive => Nis'43
    | 52%positive => Nis'42
    | 53%positive => Nis'41
    | 54%positive => Nis'40
    | 55%positive => Nis'39
    | 56%positive => Nis'38
    | 57%positive => Nis'37
    | 58%positive => Nis'36
    | 59%positive => Nis'35
    | 60%positive => Nis'34
    | 61%positive => Nis'33
    | 62%positive => Nis'32
    | 63%positive => Nis'31
    | 64%positive => Nis'30
    | 65%positive => Nis'29
    | 66%positive => Nis'28
    | 67%positive => Nis'27
    | 68%positive => Nis'26
    | 69%positive => Nis'25
    | 70%positive => Nis'24
    | 71%positive => Nis'23
    | 72%positive => Nis'22
    | 73%positive => Nis'21
    | 74%positive => Nis'20
    | 75%positive => Nis'19
    | 76%positive => Nis'18
    | 77%positive => Nis'17
    | 78%positive => Nis'16
    | 79%positive => Nis'15
    | 80%positive => Nis'14
    | 81%positive => Nis'13
    | 82%positive => Nis'12
    | 83%positive => Nis'11
    | 84%positive => Nis'10
    | 85%positive => Nis'9
    | 86%positive => Nis'8
    | 87%positive => Nis'7
    | 88%positive => Nis'6
    | 89%positive => Nis'5
    | 90%positive => Nis'4
    | 91%positive => Nis'3
    | 92%positive => Nis'2
    | 93%positive => Nis'1
    | _ => Nis'94
    end)%Z;
    inj_bound := 93%positive }.
Global Instance NonInitStateAlph : MenhirLib.Alphabet.Alphabet noninitstate := _.

Definition last_symb_of_non_init_state (noninitstate:noninitstate) : symbol :=
  match noninitstate with
  | Nis'1 => T ZERO't
  | Nis'2 => T VAR't
  | Nis'3 => T TYPE't
  | Nis'4 => T AT't
  | Nis'5 => T INT't
  | Nis'6 => T SUCC't
  | Nis'7 => T NAT't
  | Nis'8 => T LPAREN't
  | Nis'9 => T REFL't
  | Nis'10 => T INT't
  | Nis'11 => NT atomic_obj'nt
  | Nis'12 => NT atomic_obj'nt
  | Nis'13 => T REC't
  | Nis'14 => T PI't
  | Nis'15 => T LET't
  | Nis'16 => T LPAREN't
  | Nis'17 => T LPAREN't
  | Nis'18 => T VAR't
  | Nis'19 => T COLON't
  | Nis'20 => T LAMBDA't
  | Nis'21 => NT obj'nt
  | Nis'22 => T RPAREN't
  | Nis'23 => NT fnbinder'nt
  | Nis'24 => NT params'nt
  | Nis'25 => T ARROW't
  | Nis'26 => NT obj'nt
  | Nis'27 => NT eq_obj'nt
  | Nis'28 => NT atomic_obj'nt
  | Nis'29 => NT app_obj'nt
  | Nis'30 => T EQ't
  | Nis'31 => T LANGLE't
  | Nis'32 => NT obj'nt
  | Nis'33 => T RANGLE't
  | Nis'34 => NT app_obj'nt
  | Nis'35 => NT atomic_obj'nt
  | Nis'36 => NT param'nt
  | Nis'37 => NT param'nt
  | Nis'38 => NT param'nt
  | Nis'39 => T DEF't
  | Nis'40 => NT obj'nt
  | Nis'41 => T RPAREN't
  | Nis'42 => NT let_defns'nt
  | Nis'43 => T IN't
  | Nis'44 => NT obj'nt
  | Nis'45 => NT let_defn'nt
  | Nis'46 => NT let_defn'nt
  | Nis'47 => NT obj'nt
  | Nis'48 => T AS't
  | Nis'49 => T NAT't
  | Nis'50 => T LPAREN't
  | Nis'51 => NT app_obj'nt
  | Nis'52 => T EQ't
  | Nis'53 => T LANGLE't
  | Nis'54 => NT obj'nt
  | Nis'55 => T RANGLE't
  | Nis'56 => NT app_obj'nt
  | Nis'57 => T RPAREN't
  | Nis'58 => T RETURN't
  | Nis'59 => T VAR't
  | Nis'60 => T VAR't
  | Nis'61 => T VAR't
  | Nis'62 => T DOT't
  | Nis'63 => NT obj'nt
  | Nis'64 => T BAR't
  | Nis'65 => T REFL't
  | Nis'66 => T VAR't
  | Nis'67 => T DARROW't
  | Nis'68 => NT obj'nt
  | Nis'69 => T END't
  | Nis'70 => NT optional_as_nat'nt
  | Nis'71 => T RETURN't
  | Nis'72 => T VAR't
  | Nis'73 => T DOT't
  | Nis'74 => NT obj'nt
  | Nis'75 => T BAR't
  | Nis'76 => T ZERO't
  | Nis'77 => T DARROW't
  | Nis'78 => NT obj'nt
  | Nis'79 => T BAR't
  | Nis'80 => T SUCC't
  | Nis'81 => T VAR't
  | Nis'82 => T COMMA't
  | Nis'83 => T VAR't
  | Nis'84 => T DARROW't
  | Nis'85 => NT obj'nt
  | Nis'86 => T END't
  | Nis'87 => NT obj'nt
  | Nis'88 => T RPAREN't
  | Nis'89 => NT atomic_obj'nt
  | Nis'91 => NT obj'nt
  | Nis'92 => T COLON't
  | Nis'93 => NT obj'nt
  | Nis'94 => T EOF't
  end.

Inductive initstate' : Set :=
| Init'0.
Definition initstate := initstate'.

Global Program Instance initstateNum : MenhirLib.Alphabet.Numbered initstate :=
  { inj := fun x => match x return _ with
    | Init'0 => 1%positive
    end;
    surj := (fun n => match n return _ with
    | 1%positive => Init'0
    | _ => Init'0
    end)%Z;
    inj_bound := 1%positive }.
Global Instance InitStateAlph : MenhirLib.Alphabet.Alphabet initstate := _.

Include MenhirLib.Automaton.Types.

Definition start_nt (init:initstate) : nonterminal :=
  match init with
  | Init'0 => prog'nt
  end.

Definition action_table (state:state) : action :=
  match state with
  | Init Init'0 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'1 => Default_reduce_act Prod'atomic_obj'2
  | Ninit Nis'2 => Default_reduce_act Prod'atomic_obj'4
  | Ninit Nis'3 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | AT't => Shift_act Nis'4 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'4 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | INT't => Shift_act Nis'5 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'5 => Default_reduce_act Prod'atomic_obj'0
  | Ninit Nis'6 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'7 => Default_reduce_act Prod'atomic_obj'1
  | Ninit Nis'8 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'9 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'10 => Default_reduce_act Prod'atomic_obj'3
  | Ninit Nis'11 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'12 => Default_reduce_act Prod'obj'4
  | Ninit Nis'13 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'14 => Default_reduce_act Prod'fnbinder'0
  | Ninit Nis'15 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | LPAREN't => Shift_act Nis'16 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'16 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | LPAREN't => Shift_act Nis'17 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'17 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | VAR't => Shift_act Nis'18 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'18 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | COLON't => Shift_act Nis'19 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'19 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'20 => Default_reduce_act Prod'fnbinder'1
  | Ninit Nis'21 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | RPAREN't => Shift_act Nis'22 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'22 => Default_reduce_act Prod'param'0
  | Ninit Nis'23 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | LPAREN't => Shift_act Nis'17 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'24 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | LPAREN't => Shift_act Nis'17 (eq_refl _)
    | ARROW't => Shift_act Nis'25 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'25 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'26 => Default_reduce_act Prod'obj'0
  | Ninit Nis'27 => Default_reduce_act Prod'obj'1
  | Ninit Nis'28 => Default_reduce_act Prod'app_obj'1
  | Ninit Nis'29 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Reduce_act Prod'eq_obj'1
    | RPAREN't => Reduce_act Prod'eq_obj'1
    | RETURN't => Reduce_act Prod'eq_obj'1
    | REFL't => Reduce_act Prod'eq_obj'1
    | REC't => Reduce_act Prod'eq_obj'1
    | RANGLE't => Reduce_act Prod'eq_obj'1
    | PI't => Reduce_act Prod'eq_obj'1
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Reduce_act Prod'eq_obj'1
    | LANGLE't => Reduce_act Prod'eq_obj'1
    | LAMBDA't => Reduce_act Prod'eq_obj'1
    | INT't => Shift_act Nis'10 (eq_refl _)
    | IN't => Reduce_act Prod'eq_obj'1
    | EQ't => Shift_act Nis'30 (eq_refl _)
    | EOF't => Reduce_act Prod'eq_obj'1
    | END't => Reduce_act Prod'eq_obj'1
    | DOT't => Reduce_act Prod'eq_obj'1
    | DEF't => Reduce_act Prod'eq_obj'1
    | DARROW't => Reduce_act Prod'eq_obj'1
    | COMMA't => Reduce_act Prod'eq_obj'1
    | COLON't => Reduce_act Prod'eq_obj'1
    | BAR't => Reduce_act Prod'eq_obj'1
    | AT't => Reduce_act Prod'eq_obj'1
    | AS't => Reduce_act Prod'eq_obj'1
    | ARROW't => Reduce_act Prod'eq_obj'1
    end)
  | Ninit Nis'30 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | LANGLE't => Shift_act Nis'31 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'31 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'32 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | RANGLE't => Shift_act Nis'33 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'33 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'34 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Reduce_act Prod'eq_obj'0
    | RPAREN't => Reduce_act Prod'eq_obj'0
    | RETURN't => Reduce_act Prod'eq_obj'0
    | REFL't => Reduce_act Prod'eq_obj'0
    | REC't => Reduce_act Prod'eq_obj'0
    | RANGLE't => Reduce_act Prod'eq_obj'0
    | PI't => Reduce_act Prod'eq_obj'0
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Reduce_act Prod'eq_obj'0
    | LANGLE't => Reduce_act Prod'eq_obj'0
    | LAMBDA't => Reduce_act Prod'eq_obj'0
    | INT't => Shift_act Nis'10 (eq_refl _)
    | IN't => Reduce_act Prod'eq_obj'0
    | EQ't => Reduce_act Prod'eq_obj'0
    | EOF't => Reduce_act Prod'eq_obj'0
    | END't => Reduce_act Prod'eq_obj'0
    | DOT't => Reduce_act Prod'eq_obj'0
    | DEF't => Reduce_act Prod'eq_obj'0
    | DARROW't => Reduce_act Prod'eq_obj'0
    | COMMA't => Reduce_act Prod'eq_obj'0
    | COLON't => Reduce_act Prod'eq_obj'0
    | BAR't => Reduce_act Prod'eq_obj'0
    | AT't => Reduce_act Prod'eq_obj'0
    | AS't => Reduce_act Prod'eq_obj'0
    | ARROW't => Reduce_act Prod'eq_obj'0
    end)
  | Ninit Nis'35 => Default_reduce_act Prod'app_obj'0
  | Ninit Nis'36 => Default_reduce_act Prod'params'0
  | Ninit Nis'37 => Default_reduce_act Prod'params'1
  | Ninit Nis'38 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | DEF't => Shift_act Nis'39 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'39 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'40 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | RPAREN't => Shift_act Nis'41 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'41 => Default_reduce_act Prod'let_defn'0
  | Ninit Nis'42 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | LPAREN't => Shift_act Nis'16 (eq_refl _)
    | IN't => Shift_act Nis'43 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'43 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'44 => Default_reduce_act Prod'obj'6
  | Ninit Nis'45 => Default_reduce_act Prod'let_defns'0
  | Ninit Nis'46 => Default_reduce_act Prod'let_defns'1
  | Ninit Nis'47 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | RETURN't => Reduce_act Prod'optional_as_nat'1
    | AS't => Shift_act Nis'48 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'48 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | NAT't => Shift_act Nis'49 (eq_refl _)
    | LPAREN't => Shift_act Nis'50 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'49 => Default_reduce_act Prod'optional_as_nat'0
  | Ninit Nis'50 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'51 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | EQ't => Shift_act Nis'52 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'52 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | LANGLE't => Shift_act Nis'53 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'53 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'54 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | RANGLE't => Shift_act Nis'55 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'55 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'56 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | RPAREN't => Shift_act Nis'57 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'57 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | RETURN't => Shift_act Nis'58 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'58 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | VAR't => Shift_act Nis'59 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'59 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | VAR't => Shift_act Nis'60 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'60 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | VAR't => Shift_act Nis'61 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'61 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | DOT't => Shift_act Nis'62 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'62 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'63 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | BAR't => Shift_act Nis'64 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'64 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | REFL't => Shift_act Nis'65 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'65 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | VAR't => Shift_act Nis'66 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'66 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | DARROW't => Shift_act Nis'67 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'67 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'68 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | END't => Shift_act Nis'69 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'69 => Default_reduce_act Prod'obj'3
  | Ninit Nis'70 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | RETURN't => Shift_act Nis'71 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'71 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | VAR't => Shift_act Nis'72 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'72 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | DOT't => Shift_act Nis'73 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'73 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'74 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | BAR't => Shift_act Nis'75 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'75 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'76 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'76 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | DARROW't => Shift_act Nis'77 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'77 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'78 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | BAR't => Shift_act Nis'79 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'79 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | SUCC't => Shift_act Nis'80 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'80 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | VAR't => Shift_act Nis'81 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'81 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | COMMA't => Shift_act Nis'82 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'82 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | VAR't => Shift_act Nis'83 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'83 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | DARROW't => Shift_act Nis'84 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'84 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'85 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | END't => Shift_act Nis'86 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'86 => Default_reduce_act Prod'obj'2
  | Ninit Nis'87 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | RPAREN't => Shift_act Nis'88 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'88 => Default_reduce_act Prod'atomic_obj'5
  | Ninit Nis'89 => Default_reduce_act Prod'obj'5
  | Ninit Nis'91 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | COLON't => Shift_act Nis'92 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'92 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | ZERO't => Shift_act Nis'1 (eq_refl _)
    | VAR't => Shift_act Nis'2 (eq_refl _)
    | TYPE't => Shift_act Nis'3 (eq_refl _)
    | SUCC't => Shift_act Nis'6 (eq_refl _)
    | REFL't => Shift_act Nis'9 (eq_refl _)
    | REC't => Shift_act Nis'13 (eq_refl _)
    | PI't => Shift_act Nis'14 (eq_refl _)
    | NAT't => Shift_act Nis'7 (eq_refl _)
    | LPAREN't => Shift_act Nis'8 (eq_refl _)
    | LET't => Shift_act Nis'15 (eq_refl _)
    | LAMBDA't => Shift_act Nis'20 (eq_refl _)
    | INT't => Shift_act Nis'10 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'93 => Lookahead_act (fun terminal:terminal =>
    match terminal return lookahead_action terminal with
    | EOF't => Shift_act Nis'94 (eq_refl _)
    | _ => Fail_act
    end)
  | Ninit Nis'94 => Default_reduce_act Prod'prog'0
  end.

Definition goto_table (state:state) (nt:nonterminal) :=
  match state, nt return option { s:noninitstate | NT nt = last_symb_of_non_init_state s } with
  | Init Init'0, prog'nt => None | Init Init'0, obj'nt => Some (exist _ Nis'91 (eq_refl _))
  | Init Init'0, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Init Init'0, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Init Init'0, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Init Init'0, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'6, atomic_obj'nt => Some (exist _ Nis'89 (eq_refl _))
  | Ninit Nis'8, obj'nt => Some (exist _ Nis'87 (eq_refl _))
  | Ninit Nis'8, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'8, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'8, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'8, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'9, atomic_obj'nt => Some (exist _ Nis'11 (eq_refl _))
  | Ninit Nis'11, atomic_obj'nt => Some (exist _ Nis'12 (eq_refl _))
  | Ninit Nis'13, obj'nt => Some (exist _ Nis'47 (eq_refl _))
  | Ninit Nis'13, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'13, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'13, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'13, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'15, let_defns'nt => Some (exist _ Nis'42 (eq_refl _))
  | Ninit Nis'15, let_defn'nt => Some (exist _ Nis'46 (eq_refl _))
  | Ninit Nis'16, param'nt => Some (exist _ Nis'38 (eq_refl _))
  | Ninit Nis'19, obj'nt => Some (exist _ Nis'21 (eq_refl _))
  | Ninit Nis'19, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'19, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'19, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'19, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'23, params'nt => Some (exist _ Nis'24 (eq_refl _))
  | Ninit Nis'23, param'nt => Some (exist _ Nis'37 (eq_refl _))
  | Ninit Nis'24, param'nt => Some (exist _ Nis'36 (eq_refl _))
  | Ninit Nis'25, obj'nt => Some (exist _ Nis'26 (eq_refl _))
  | Ninit Nis'25, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'25, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'25, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'25, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'29, atomic_obj'nt => Some (exist _ Nis'35 (eq_refl _))
  | Ninit Nis'31, obj'nt => Some (exist _ Nis'32 (eq_refl _))
  | Ninit Nis'31, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'31, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'31, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'31, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'33, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'33, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
  | Ninit Nis'34, atomic_obj'nt => Some (exist _ Nis'35 (eq_refl _))
  | Ninit Nis'39, obj'nt => Some (exist _ Nis'40 (eq_refl _))
  | Ninit Nis'39, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'39, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'39, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'39, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'42, let_defn'nt => Some (exist _ Nis'45 (eq_refl _))
  | Ninit Nis'43, obj'nt => Some (exist _ Nis'44 (eq_refl _))
  | Ninit Nis'43, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'43, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'43, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'43, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'47, optional_as_nat'nt => Some (exist _ Nis'70 (eq_refl _))
  | Ninit Nis'50, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'50, app_obj'nt => Some (exist _ Nis'51 (eq_refl _))
  | Ninit Nis'51, atomic_obj'nt => Some (exist _ Nis'35 (eq_refl _))
  | Ninit Nis'53, obj'nt => Some (exist _ Nis'54 (eq_refl _))
  | Ninit Nis'53, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'53, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'53, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'53, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'55, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'55, app_obj'nt => Some (exist _ Nis'56 (eq_refl _))
  | Ninit Nis'56, atomic_obj'nt => Some (exist _ Nis'35 (eq_refl _))
  | Ninit Nis'62, obj'nt => Some (exist _ Nis'63 (eq_refl _))
  | Ninit Nis'62, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'62, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'62, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'62, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'67, obj'nt => Some (exist _ Nis'68 (eq_refl _))
  | Ninit Nis'67, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'67, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'67, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'67, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'73, obj'nt => Some (exist _ Nis'74 (eq_refl _))
  | Ninit Nis'73, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'73, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'73, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'73, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'77, obj'nt => Some (exist _ Nis'78 (eq_refl _))
  | Ninit Nis'77, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'77, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'77, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'77, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'84, obj'nt => Some (exist _ Nis'85 (eq_refl _))
  | Ninit Nis'84, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'84, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'84, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'84, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | Ninit Nis'92, obj'nt => Some (exist _ Nis'93 (eq_refl _))
  | Ninit Nis'92, fnbinder'nt => Some (exist _ Nis'23 (eq_refl _))
  | Ninit Nis'92, eq_obj'nt => Some (exist _ Nis'27 (eq_refl _))
  | Ninit Nis'92, atomic_obj'nt => Some (exist _ Nis'28 (eq_refl _))
  | Ninit Nis'92, app_obj'nt => Some (exist _ Nis'29 (eq_refl _))
  | _, _ => None
  end.

Definition past_symb_of_non_init_state (noninitstate:noninitstate) : list symbol :=
  match noninitstate with
  | Nis'1 => []%list
  | Nis'2 => []%list
  | Nis'3 => []%list
  | Nis'4 => [T TYPE't]%list
  | Nis'5 => [T AT't; T TYPE't]%list
  | Nis'6 => []%list
  | Nis'7 => []%list
  | Nis'8 => []%list
  | Nis'9 => []%list
  | Nis'10 => []%list
  | Nis'11 => [T REFL't]%list
  | Nis'12 => [NT atomic_obj'nt; T REFL't]%list
  | Nis'13 => []%list
  | Nis'14 => []%list
  | Nis'15 => []%list
  | Nis'16 => []%list
  | Nis'17 => []%list
  | Nis'18 => [T LPAREN't]%list
  | Nis'19 => [T VAR't; T LPAREN't]%list
  | Nis'20 => []%list
  | Nis'21 => [T COLON't; T VAR't; T LPAREN't]%list
  | Nis'22 => [NT obj'nt; T COLON't; T VAR't; T LPAREN't]%list
  | Nis'23 => []%list
  | Nis'24 => [NT fnbinder'nt]%list
  | Nis'25 => [NT params'nt; NT fnbinder'nt]%list
  | Nis'26 => [T ARROW't; NT params'nt; NT fnbinder'nt]%list
  | Nis'27 => []%list
  | Nis'28 => []%list
  | Nis'29 => []%list
  | Nis'30 => [NT app_obj'nt]%list
  | Nis'31 => [T EQ't; NT app_obj'nt]%list
  | Nis'32 => [T LANGLE't; T EQ't; NT app_obj'nt]%list
  | Nis'33 => [NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt]%list
  | Nis'34 => [T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt]%list
  | Nis'35 => [NT app_obj'nt]%list
  | Nis'36 => [NT params'nt]%list
  | Nis'37 => []%list
  | Nis'38 => [T LPAREN't]%list
  | Nis'39 => [NT param'nt; T LPAREN't]%list
  | Nis'40 => [T DEF't; NT param'nt; T LPAREN't]%list
  | Nis'41 => [NT obj'nt; T DEF't; NT param'nt; T LPAREN't]%list
  | Nis'42 => [T LET't]%list
  | Nis'43 => [NT let_defns'nt; T LET't]%list
  | Nis'44 => [T IN't; NT let_defns'nt; T LET't]%list
  | Nis'45 => [NT let_defns'nt]%list
  | Nis'46 => []%list
  | Nis'47 => [T REC't]%list
  | Nis'48 => [NT obj'nt; T REC't]%list
  | Nis'49 => [T AS't]%list
  | Nis'50 => [T AS't; NT obj'nt; T REC't]%list
  | Nis'51 => [T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'52 => [NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'53 => [T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'54 => [T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'55 => [NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'56 => [T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'57 => [NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'58 => [T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'59 => [T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'60 => [T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'61 => [T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'62 => [T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'63 => [T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'64 => [NT obj'nt; T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'65 => [T BAR't; NT obj'nt; T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'66 => [T REFL't; T BAR't; NT obj'nt; T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'67 => [T VAR't; T REFL't; T BAR't; NT obj'nt; T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'68 => [T DARROW't; T VAR't; T REFL't; T BAR't; NT obj'nt; T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'69 => [NT obj'nt; T DARROW't; T VAR't; T REFL't; T BAR't; NT obj'nt; T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RANGLE't; NT obj'nt; T LANGLE't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
  | Nis'70 => [NT obj'nt; T REC't]%list
  | Nis'71 => [NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'72 => [T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'73 => [T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'74 => [T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'75 => [NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'76 => [T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'77 => [T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'78 => [T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'79 => [NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'80 => [T BAR't; NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'81 => [T SUCC't; T BAR't; NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'82 => [T VAR't; T SUCC't; T BAR't; NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'83 => [T COMMA't; T VAR't; T SUCC't; T BAR't; NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'84 => [T VAR't; T COMMA't; T VAR't; T SUCC't; T BAR't; NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'85 => [T DARROW't; T VAR't; T COMMA't; T VAR't; T SUCC't; T BAR't; NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'86 => [NT obj'nt; T DARROW't; T VAR't; T COMMA't; T VAR't; T SUCC't; T BAR't; NT obj'nt; T DARROW't; T ZERO't; T BAR't; NT obj'nt; T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
  | Nis'87 => [T LPAREN't]%list
  | Nis'88 => [NT obj'nt; T LPAREN't]%list
  | Nis'89 => [T SUCC't]%list
  | Nis'91 => []%list
  | Nis'92 => [NT obj'nt]%list
  | Nis'93 => [T COLON't; NT obj'nt]%list
  | Nis'94 => [NT obj'nt; T COLON't; NT obj'nt]%list
  end.
Extract Constant past_symb_of_non_init_state => "fun _ -> assert false".

Definition state_set_1 (s:state) : bool :=
  match s with
  | Init Init'0 | Ninit Nis'6 | Ninit Nis'8 | Ninit Nis'9 | Ninit Nis'11 | Ninit Nis'13 | Ninit Nis'19 | Ninit Nis'25 | Ninit Nis'29 | Ninit Nis'31 | Ninit Nis'33 | Ninit Nis'34 | Ninit Nis'39 | Ninit Nis'43 | Ninit Nis'50 | Ninit Nis'51 | Ninit Nis'53 | Ninit Nis'55 | Ninit Nis'56 | Ninit Nis'62 | Ninit Nis'67 | Ninit Nis'73 | Ninit Nis'77 | Ninit Nis'84 | Ninit Nis'92 => true
  | _ => false
  end.
Extract Inlined Constant state_set_1 => "assert false".

Definition state_set_2 (s:state) : bool :=
  match s with
  | Ninit Nis'3 => true
  | _ => false
  end.
Extract Inlined Constant state_set_2 => "assert false".

Definition state_set_3 (s:state) : bool :=
  match s with
  | Ninit Nis'4 => true
  | _ => false
  end.
Extract Inlined Constant state_set_3 => "assert false".

Definition state_set_4 (s:state) : bool :=
  match s with
  | Init Init'0 | Ninit Nis'8 | Ninit Nis'13 | Ninit Nis'19 | Ninit Nis'25 | Ninit Nis'31 | Ninit Nis'39 | Ninit Nis'43 | Ninit Nis'53 | Ninit Nis'62 | Ninit Nis'67 | Ninit Nis'73 | Ninit Nis'77 | Ninit Nis'84 | Ninit Nis'92 => true
  | _ => false
  end.
Extract Inlined Constant state_set_4 => "assert false".

Definition state_set_5 (s:state) : bool :=
  match s with
  | Ninit Nis'9 => true
  | _ => false
  end.
Extract Inlined Constant state_set_5 => "assert false".

Definition state_set_6 (s:state) : bool :=
  match s with
  | Ninit Nis'11 => true
  | _ => false
  end.
Extract Inlined Constant state_set_6 => "assert false".

Definition state_set_7 (s:state) : bool :=
  match s with
  | Ninit Nis'15 | Ninit Nis'42 => true
  | _ => false
  end.
Extract Inlined Constant state_set_7 => "assert false".

Definition state_set_8 (s:state) : bool :=
  match s with
  | Ninit Nis'16 | Ninit Nis'23 | Ninit Nis'24 => true
  | _ => false
  end.
Extract Inlined Constant state_set_8 => "assert false".

Definition state_set_9 (s:state) : bool :=
  match s with
  | Ninit Nis'17 => true
  | _ => false
  end.
Extract Inlined Constant state_set_9 => "assert false".

Definition state_set_10 (s:state) : bool :=
  match s with
  | Ninit Nis'18 => true
  | _ => false
  end.
Extract Inlined Constant state_set_10 => "assert false".

Definition state_set_11 (s:state) : bool :=
  match s with
  | Ninit Nis'19 => true
  | _ => false
  end.
Extract Inlined Constant state_set_11 => "assert false".

Definition state_set_12 (s:state) : bool :=
  match s with
  | Ninit Nis'21 => true
  | _ => false
  end.
Extract Inlined Constant state_set_12 => "assert false".

Definition state_set_13 (s:state) : bool :=
  match s with
  | Ninit Nis'23 => true
  | _ => false
  end.
Extract Inlined Constant state_set_13 => "assert false".

Definition state_set_14 (s:state) : bool :=
  match s with
  | Ninit Nis'24 => true
  | _ => false
  end.
Extract Inlined Constant state_set_14 => "assert false".

Definition state_set_15 (s:state) : bool :=
  match s with
  | Ninit Nis'25 => true
  | _ => false
  end.
Extract Inlined Constant state_set_15 => "assert false".

Definition state_set_16 (s:state) : bool :=
  match s with
  | Init Init'0 | Ninit Nis'8 | Ninit Nis'13 | Ninit Nis'19 | Ninit Nis'25 | Ninit Nis'31 | Ninit Nis'33 | Ninit Nis'39 | Ninit Nis'43 | Ninit Nis'50 | Ninit Nis'53 | Ninit Nis'55 | Ninit Nis'62 | Ninit Nis'67 | Ninit Nis'73 | Ninit Nis'77 | Ninit Nis'84 | Ninit Nis'92 => true
  | _ => false
  end.
Extract Inlined Constant state_set_16 => "assert false".

Definition state_set_17 (s:state) : bool :=
  match s with
  | Ninit Nis'29 => true
  | _ => false
  end.
Extract Inlined Constant state_set_17 => "assert false".

Definition state_set_18 (s:state) : bool :=
  match s with
  | Ninit Nis'30 => true
  | _ => false
  end.
Extract Inlined Constant state_set_18 => "assert false".

Definition state_set_19 (s:state) : bool :=
  match s with
  | Ninit Nis'31 => true
  | _ => false
  end.
Extract Inlined Constant state_set_19 => "assert false".

Definition state_set_20 (s:state) : bool :=
  match s with
  | Ninit Nis'32 => true
  | _ => false
  end.
Extract Inlined Constant state_set_20 => "assert false".

Definition state_set_21 (s:state) : bool :=
  match s with
  | Ninit Nis'33 => true
  | _ => false
  end.
Extract Inlined Constant state_set_21 => "assert false".

Definition state_set_22 (s:state) : bool :=
  match s with
  | Ninit Nis'29 | Ninit Nis'34 | Ninit Nis'51 | Ninit Nis'56 => true
  | _ => false
  end.
Extract Inlined Constant state_set_22 => "assert false".

Definition state_set_23 (s:state) : bool :=
  match s with
  | Ninit Nis'16 => true
  | _ => false
  end.
Extract Inlined Constant state_set_23 => "assert false".

Definition state_set_24 (s:state) : bool :=
  match s with
  | Ninit Nis'38 => true
  | _ => false
  end.
Extract Inlined Constant state_set_24 => "assert false".

Definition state_set_25 (s:state) : bool :=
  match s with
  | Ninit Nis'39 => true
  | _ => false
  end.
Extract Inlined Constant state_set_25 => "assert false".

Definition state_set_26 (s:state) : bool :=
  match s with
  | Ninit Nis'40 => true
  | _ => false
  end.
Extract Inlined Constant state_set_26 => "assert false".

Definition state_set_27 (s:state) : bool :=
  match s with
  | Ninit Nis'15 => true
  | _ => false
  end.
Extract Inlined Constant state_set_27 => "assert false".

Definition state_set_28 (s:state) : bool :=
  match s with
  | Ninit Nis'42 => true
  | _ => false
  end.
Extract Inlined Constant state_set_28 => "assert false".

Definition state_set_29 (s:state) : bool :=
  match s with
  | Ninit Nis'43 => true
  | _ => false
  end.
Extract Inlined Constant state_set_29 => "assert false".

Definition state_set_30 (s:state) : bool :=
  match s with
  | Ninit Nis'13 => true
  | _ => false
  end.
Extract Inlined Constant state_set_30 => "assert false".

Definition state_set_31 (s:state) : bool :=
  match s with
  | Ninit Nis'47 => true
  | _ => false
  end.
Extract Inlined Constant state_set_31 => "assert false".

Definition state_set_32 (s:state) : bool :=
  match s with
  | Ninit Nis'48 => true
  | _ => false
  end.
Extract Inlined Constant state_set_32 => "assert false".

Definition state_set_33 (s:state) : bool :=
  match s with
  | Ninit Nis'50 => true
  | _ => false
  end.
Extract Inlined Constant state_set_33 => "assert false".

Definition state_set_34 (s:state) : bool :=
  match s with
  | Ninit Nis'51 => true
  | _ => false
  end.
Extract Inlined Constant state_set_34 => "assert false".

Definition state_set_35 (s:state) : bool :=
  match s with
  | Ninit Nis'52 => true
  | _ => false
  end.
Extract Inlined Constant state_set_35 => "assert false".

Definition state_set_36 (s:state) : bool :=
  match s with
  | Ninit Nis'53 => true
  | _ => false
  end.
Extract Inlined Constant state_set_36 => "assert false".

Definition state_set_37 (s:state) : bool :=
  match s with
  | Ninit Nis'54 => true
  | _ => false
  end.
Extract Inlined Constant state_set_37 => "assert false".

Definition state_set_38 (s:state) : bool :=
  match s with
  | Ninit Nis'55 => true
  | _ => false
  end.
Extract Inlined Constant state_set_38 => "assert false".

Definition state_set_39 (s:state) : bool :=
  match s with
  | Ninit Nis'56 => true
  | _ => false
  end.
Extract Inlined Constant state_set_39 => "assert false".

Definition state_set_40 (s:state) : bool :=
  match s with
  | Ninit Nis'57 => true
  | _ => false
  end.
Extract Inlined Constant state_set_40 => "assert false".

Definition state_set_41 (s:state) : bool :=
  match s with
  | Ninit Nis'58 => true
  | _ => false
  end.
Extract Inlined Constant state_set_41 => "assert false".

Definition state_set_42 (s:state) : bool :=
  match s with
  | Ninit Nis'59 => true
  | _ => false
  end.
Extract Inlined Constant state_set_42 => "assert false".

Definition state_set_43 (s:state) : bool :=
  match s with
  | Ninit Nis'60 => true
  | _ => false
  end.
Extract Inlined Constant state_set_43 => "assert false".

Definition state_set_44 (s:state) : bool :=
  match s with
  | Ninit Nis'61 => true
  | _ => false
  end.
Extract Inlined Constant state_set_44 => "assert false".

Definition state_set_45 (s:state) : bool :=
  match s with
  | Ninit Nis'62 => true
  | _ => false
  end.
Extract Inlined Constant state_set_45 => "assert false".

Definition state_set_46 (s:state) : bool :=
  match s with
  | Ninit Nis'63 => true
  | _ => false
  end.
Extract Inlined Constant state_set_46 => "assert false".

Definition state_set_47 (s:state) : bool :=
  match s with
  | Ninit Nis'64 => true
  | _ => false
  end.
Extract Inlined Constant state_set_47 => "assert false".

Definition state_set_48 (s:state) : bool :=
  match s with
  | Ninit Nis'65 => true
  | _ => false
  end.
Extract Inlined Constant state_set_48 => "assert false".

Definition state_set_49 (s:state) : bool :=
  match s with
  | Ninit Nis'66 => true
  | _ => false
  end.
Extract Inlined Constant state_set_49 => "assert false".

Definition state_set_50 (s:state) : bool :=
  match s with
  | Ninit Nis'67 => true
  | _ => false
  end.
Extract Inlined Constant state_set_50 => "assert false".

Definition state_set_51 (s:state) : bool :=
  match s with
  | Ninit Nis'68 => true
  | _ => false
  end.
Extract Inlined Constant state_set_51 => "assert false".

Definition state_set_52 (s:state) : bool :=
  match s with
  | Ninit Nis'70 => true
  | _ => false
  end.
Extract Inlined Constant state_set_52 => "assert false".

Definition state_set_53 (s:state) : bool :=
  match s with
  | Ninit Nis'71 => true
  | _ => false
  end.
Extract Inlined Constant state_set_53 => "assert false".

Definition state_set_54 (s:state) : bool :=
  match s with
  | Ninit Nis'72 => true
  | _ => false
  end.
Extract Inlined Constant state_set_54 => "assert false".

Definition state_set_55 (s:state) : bool :=
  match s with
  | Ninit Nis'73 => true
  | _ => false
  end.
Extract Inlined Constant state_set_55 => "assert false".

Definition state_set_56 (s:state) : bool :=
  match s with
  | Ninit Nis'74 => true
  | _ => false
  end.
Extract Inlined Constant state_set_56 => "assert false".

Definition state_set_57 (s:state) : bool :=
  match s with
  | Ninit Nis'75 => true
  | _ => false
  end.
Extract Inlined Constant state_set_57 => "assert false".

Definition state_set_58 (s:state) : bool :=
  match s with
  | Ninit Nis'76 => true
  | _ => false
  end.
Extract Inlined Constant state_set_58 => "assert false".

Definition state_set_59 (s:state) : bool :=
  match s with
  | Ninit Nis'77 => true
  | _ => false
  end.
Extract Inlined Constant state_set_59 => "assert false".

Definition state_set_60 (s:state) : bool :=
  match s with
  | Ninit Nis'78 => true
  | _ => false
  end.
Extract Inlined Constant state_set_60 => "assert false".

Definition state_set_61 (s:state) : bool :=
  match s with
  | Ninit Nis'79 => true
  | _ => false
  end.
Extract Inlined Constant state_set_61 => "assert false".

Definition state_set_62 (s:state) : bool :=
  match s with
  | Ninit Nis'80 => true
  | _ => false
  end.
Extract Inlined Constant state_set_62 => "assert false".

Definition state_set_63 (s:state) : bool :=
  match s with
  | Ninit Nis'81 => true
  | _ => false
  end.
Extract Inlined Constant state_set_63 => "assert false".

Definition state_set_64 (s:state) : bool :=
  match s with
  | Ninit Nis'82 => true
  | _ => false
  end.
Extract Inlined Constant state_set_64 => "assert false".

Definition state_set_65 (s:state) : bool :=
  match s with
  | Ninit Nis'83 => true
  | _ => false
  end.
Extract Inlined Constant state_set_65 => "assert false".

Definition state_set_66 (s:state) : bool :=
  match s with
  | Ninit Nis'84 => true
  | _ => false
  end.
Extract Inlined Constant state_set_66 => "assert false".

Definition state_set_67 (s:state) : bool :=
  match s with
  | Ninit Nis'85 => true
  | _ => false
  end.
Extract Inlined Constant state_set_67 => "assert false".

Definition state_set_68 (s:state) : bool :=
  match s with
  | Ninit Nis'8 => true
  | _ => false
  end.
Extract Inlined Constant state_set_68 => "assert false".

Definition state_set_69 (s:state) : bool :=
  match s with
  | Ninit Nis'87 => true
  | _ => false
  end.
Extract Inlined Constant state_set_69 => "assert false".

Definition state_set_70 (s:state) : bool :=
  match s with
  | Ninit Nis'6 => true
  | _ => false
  end.
Extract Inlined Constant state_set_70 => "assert false".

Definition state_set_71 (s:state) : bool :=
  match s with
  | Init Init'0 => true
  | _ => false
  end.
Extract Inlined Constant state_set_71 => "assert false".

Definition state_set_72 (s:state) : bool :=
  match s with
  | Ninit Nis'91 => true
  | _ => false
  end.
Extract Inlined Constant state_set_72 => "assert false".

Definition state_set_73 (s:state) : bool :=
  match s with
  | Ninit Nis'92 => true
  | _ => false
  end.
Extract Inlined Constant state_set_73 => "assert false".

Definition state_set_74 (s:state) : bool :=
  match s with
  | Ninit Nis'93 => true
  | _ => false
  end.
Extract Inlined Constant state_set_74 => "assert false".

Definition past_state_of_non_init_state (s:noninitstate) : list (state -> bool) :=
  match s with
  | Nis'1 => [state_set_1]%list
  | Nis'2 => [state_set_1]%list
  | Nis'3 => [state_set_1]%list
  | Nis'4 => [state_set_2; state_set_1]%list
  | Nis'5 => [state_set_3; state_set_2; state_set_1]%list
  | Nis'6 => [state_set_4]%list
  | Nis'7 => [state_set_1]%list
  | Nis'8 => [state_set_1]%list
  | Nis'9 => [state_set_4]%list
  | Nis'10 => [state_set_1]%list
  | Nis'11 => [state_set_5; state_set_4]%list
  | Nis'12 => [state_set_6; state_set_5; state_set_4]%list
  | Nis'13 => [state_set_4]%list
  | Nis'14 => [state_set_4]%list
  | Nis'15 => [state_set_4]%list
  | Nis'16 => [state_set_7]%list
  | Nis'17 => [state_set_8]%list
  | Nis'18 => [state_set_9; state_set_8]%list
  | Nis'19 => [state_set_10; state_set_9; state_set_8]%list
  | Nis'20 => [state_set_4]%list
  | Nis'21 => [state_set_11; state_set_10; state_set_9; state_set_8]%list
  | Nis'22 => [state_set_12; state_set_11; state_set_10; state_set_9; state_set_8]%list
  | Nis'23 => [state_set_4]%list
  | Nis'24 => [state_set_13; state_set_4]%list
  | Nis'25 => [state_set_14; state_set_13; state_set_4]%list
  | Nis'26 => [state_set_15; state_set_14; state_set_13; state_set_4]%list
  | Nis'27 => [state_set_4]%list
  | Nis'28 => [state_set_16]%list
  | Nis'29 => [state_set_4]%list
  | Nis'30 => [state_set_17; state_set_4]%list
  | Nis'31 => [state_set_18; state_set_17; state_set_4]%list
  | Nis'32 => [state_set_19; state_set_18; state_set_17; state_set_4]%list
  | Nis'33 => [state_set_20; state_set_19; state_set_18; state_set_17; state_set_4]%list
  | Nis'34 => [state_set_21; state_set_20; state_set_19; state_set_18; state_set_17; state_set_4]%list
  | Nis'35 => [state_set_22; state_set_16]%list
  | Nis'36 => [state_set_14; state_set_13]%list
  | Nis'37 => [state_set_13]%list
  | Nis'38 => [state_set_23; state_set_7]%list
  | Nis'39 => [state_set_24; state_set_23; state_set_7]%list
  | Nis'40 => [state_set_25; state_set_24; state_set_23; state_set_7]%list
  | Nis'41 => [state_set_26; state_set_25; state_set_24; state_set_23; state_set_7]%list
  | Nis'42 => [state_set_27; state_set_4]%list
  | Nis'43 => [state_set_28; state_set_27; state_set_4]%list
  | Nis'44 => [state_set_29; state_set_28; state_set_27; state_set_4]%list
  | Nis'45 => [state_set_28; state_set_27]%list
  | Nis'46 => [state_set_27]%list
  | Nis'47 => [state_set_30; state_set_4]%list
  | Nis'48 => [state_set_31; state_set_30; state_set_4]%list
  | Nis'49 => [state_set_32; state_set_31]%list
  | Nis'50 => [state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'51 => [state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'52 => [state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'53 => [state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'54 => [state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'55 => [state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'56 => [state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'57 => [state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'58 => [state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'59 => [state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'60 => [state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'61 => [state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'62 => [state_set_44; state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'63 => [state_set_45; state_set_44; state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'64 => [state_set_46; state_set_45; state_set_44; state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'65 => [state_set_47; state_set_46; state_set_45; state_set_44; state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'66 => [state_set_48; state_set_47; state_set_46; state_set_45; state_set_44; state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'67 => [state_set_49; state_set_48; state_set_47; state_set_46; state_set_45; state_set_44; state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'68 => [state_set_50; state_set_49; state_set_48; state_set_47; state_set_46; state_set_45; state_set_44; state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'69 => [state_set_51; state_set_50; state_set_49; state_set_48; state_set_47; state_set_46; state_set_45; state_set_44; state_set_43; state_set_42; state_set_41; state_set_40; state_set_39; state_set_38; state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_30; state_set_4]%list
  | Nis'70 => [state_set_31; state_set_30; state_set_4]%list
  | Nis'71 => [state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'72 => [state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'73 => [state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'74 => [state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'75 => [state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'76 => [state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'77 => [state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'78 => [state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'79 => [state_set_60; state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'80 => [state_set_61; state_set_60; state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'81 => [state_set_62; state_set_61; state_set_60; state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'82 => [state_set_63; state_set_62; state_set_61; state_set_60; state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'83 => [state_set_64; state_set_63; state_set_62; state_set_61; state_set_60; state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'84 => [state_set_65; state_set_64; state_set_63; state_set_62; state_set_61; state_set_60; state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'85 => [state_set_66; state_set_65; state_set_64; state_set_63; state_set_62; state_set_61; state_set_60; state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'86 => [state_set_67; state_set_66; state_set_65; state_set_64; state_set_63; state_set_62; state_set_61; state_set_60; state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_52; state_set_31; state_set_30; state_set_4]%list
  | Nis'87 => [state_set_68; state_set_1]%list
  | Nis'88 => [state_set_69; state_set_68; state_set_1]%list
  | Nis'89 => [state_set_70; state_set_4]%list
  | Nis'91 => [state_set_71]%list
  | Nis'92 => [state_set_72; state_set_71]%list
  | Nis'93 => [state_set_73; state_set_72; state_set_71]%list
  | Nis'94 => [state_set_74; state_set_73; state_set_72; state_set_71]%list
  end.
Extract Constant past_state_of_non_init_state => "fun _ -> assert false".

Definition lookahead_set_1 : list terminal :=
  [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't; EQ't; COLON't]%list.
Extract Inlined Constant lookahead_set_1 => "assert false".

Definition lookahead_set_2 : list terminal :=
  [COLON't]%list.
Extract Inlined Constant lookahead_set_2 => "assert false".

Definition lookahead_set_3 : list terminal :=
  [LPAREN't]%list.
Extract Inlined Constant lookahead_set_3 => "assert false".

Definition lookahead_set_4 : list terminal :=
  [ZERO't; VAR't; TYPE't; SUCC't; RPAREN't; RETURN't; REFL't; REC't; RANGLE't; PI't; NAT't; LPAREN't; LET't; LANGLE't; LAMBDA't; INT't; IN't; EQ't; EOF't; END't; DOT't; DEF't; DARROW't; COMMA't; COLON't; BAR't; AT't; AS't; ARROW't]%list.
Extract Inlined Constant lookahead_set_4 => "assert false".

Definition lookahead_set_5 : list terminal :=
  [ZERO't; VAR't; TYPE't; RPAREN't; RETURN't; RANGLE't; NAT't; LPAREN't; INT't; EQ't; EOF't; END't; COLON't; BAR't; AS't]%list.
Extract Inlined Constant lookahead_set_5 => "assert false".

Definition lookahead_set_6 : list terminal :=
  [RPAREN't; RETURN't; RANGLE't; EOF't; END't; COLON't; BAR't; AS't]%list.
Extract Inlined Constant lookahead_set_6 => "assert false".

Definition lookahead_set_7 : list terminal :=
  [ZERO't; VAR't; TYPE't; RPAREN't; NAT't; LPAREN't; INT't; EQ't]%list.
Extract Inlined Constant lookahead_set_7 => "assert false".

Definition lookahead_set_8 : list terminal :=
  [RPAREN't]%list.
Extract Inlined Constant lookahead_set_8 => "assert false".

Definition lookahead_set_9 : list terminal :=
  [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't]%list.
Extract Inlined Constant lookahead_set_9 => "assert false".

Definition lookahead_set_10 : list terminal :=
  [ZERO't; VAR't; TYPE't; RETURN't; NAT't; LPAREN't; INT't; EQ't; AS't]%list.
Extract Inlined Constant lookahead_set_10 => "assert false".

Definition lookahead_set_11 : list terminal :=
  [RETURN't; AS't]%list.
Extract Inlined Constant lookahead_set_11 => "assert false".

Definition lookahead_set_12 : list terminal :=
  [LPAREN't; IN't]%list.
Extract Inlined Constant lookahead_set_12 => "assert false".

Definition lookahead_set_13 : list terminal :=
  [DEF't]%list.
Extract Inlined Constant lookahead_set_13 => "assert false".

Definition lookahead_set_14 : list terminal :=
  [LPAREN't; DEF't; ARROW't]%list.
Extract Inlined Constant lookahead_set_14 => "assert false".

Definition lookahead_set_15 : list terminal :=
  [LPAREN't; ARROW't]%list.
Extract Inlined Constant lookahead_set_15 => "assert false".

Definition lookahead_set_16 : list terminal :=
  [ZERO't; VAR't; TYPE't; RANGLE't; NAT't; LPAREN't; INT't; EQ't]%list.
Extract Inlined Constant lookahead_set_16 => "assert false".

Definition lookahead_set_17 : list terminal :=
  [RANGLE't]%list.
Extract Inlined Constant lookahead_set_17 => "assert false".

Definition lookahead_set_18 : list terminal :=
  [ZERO't; VAR't; TYPE't; RPAREN't; RETURN't; RANGLE't; NAT't; LPAREN't; INT't; EOF't; END't; COLON't; BAR't; AS't]%list.
Extract Inlined Constant lookahead_set_18 => "assert false".

Definition lookahead_set_19 : list terminal :=
  [RETURN't]%list.
Extract Inlined Constant lookahead_set_19 => "assert false".

Definition lookahead_set_20 : list terminal :=
  [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't; EQ't]%list.
Extract Inlined Constant lookahead_set_20 => "assert false".

Definition lookahead_set_21 : list terminal :=
  [ZERO't; VAR't; TYPE't; RPAREN't; NAT't; LPAREN't; INT't]%list.
Extract Inlined Constant lookahead_set_21 => "assert false".

Definition lookahead_set_22 : list terminal :=
  [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't; EQ't; BAR't]%list.
Extract Inlined Constant lookahead_set_22 => "assert false".

Definition lookahead_set_23 : list terminal :=
  [BAR't]%list.
Extract Inlined Constant lookahead_set_23 => "assert false".

Definition lookahead_set_24 : list terminal :=
  [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't; EQ't; END't]%list.
Extract Inlined Constant lookahead_set_24 => "assert false".

Definition lookahead_set_25 : list terminal :=
  [END't]%list.
Extract Inlined Constant lookahead_set_25 => "assert false".

Definition lookahead_set_26 : list terminal :=
  [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; INT't; EQ't; EOF't]%list.
Extract Inlined Constant lookahead_set_26 => "assert false".

Definition lookahead_set_27 : list terminal :=
  [EOF't]%list.
Extract Inlined Constant lookahead_set_27 => "assert false".

Definition items_of_state_0 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_1 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_1 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_1 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_1 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_1 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_1 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_1 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_1 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
    {| prod_item := Prod'prog'0; dot_pos_item := 0; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_0 => "assert false".

Definition items_of_state_1 : list item :=
  [ {| prod_item := Prod'atomic_obj'2; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_1 => "assert false".

Definition items_of_state_2 : list item :=
  [ {| prod_item := Prod'atomic_obj'4; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_2 => "assert false".

Definition items_of_state_3 : list item :=
  [ {| prod_item := Prod'atomic_obj'0; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_3 => "assert false".

Definition items_of_state_4 : list item :=
  [ {| prod_item := Prod'atomic_obj'0; dot_pos_item := 2; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_4 => "assert false".

Definition items_of_state_5 : list item :=
  [ {| prod_item := Prod'atomic_obj'0; dot_pos_item := 3; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_5 => "assert false".

Definition items_of_state_6 : list item :=
  [ {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_6 => "assert false".

Definition items_of_state_7 : list item :=
  [ {| prod_item := Prod'atomic_obj'1; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_7 => "assert false".

Definition items_of_state_8 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |} ]%list.
Extract Inlined Constant items_of_state_8 => "assert false".

Definition items_of_state_9 : list item :=
  [ {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_9 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_9 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_9 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_9 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_9 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_9 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_9 => "assert false".

Definition items_of_state_10 : list item :=
  [ {| prod_item := Prod'atomic_obj'3; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_10 => "assert false".

Definition items_of_state_11 : list item :=
  [ {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_11 => "assert false".

Definition items_of_state_12 : list item :=
  [ {| prod_item := Prod'obj'4; dot_pos_item := 3; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_12 => "assert false".

Definition items_of_state_13 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_10 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_10 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_10 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_10 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_10 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_10 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_10 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_10 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |} ]%list.
Extract Inlined Constant items_of_state_13 => "assert false".

Definition items_of_state_14 : list item :=
  [ {| prod_item := Prod'fnbinder'0; dot_pos_item := 1; lookaheads_item := lookahead_set_3 |} ]%list.
Extract Inlined Constant items_of_state_14 => "assert false".

Definition items_of_state_15 : list item :=
  [ {| prod_item := Prod'let_defn'0; dot_pos_item := 0; lookaheads_item := lookahead_set_12 |};
    {| prod_item := Prod'let_defns'0; dot_pos_item := 0; lookaheads_item := lookahead_set_12 |};
    {| prod_item := Prod'let_defns'1; dot_pos_item := 0; lookaheads_item := lookahead_set_12 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_15 => "assert false".

Definition items_of_state_16 : list item :=
  [ {| prod_item := Prod'let_defn'0; dot_pos_item := 1; lookaheads_item := lookahead_set_12 |};
    {| prod_item := Prod'param'0; dot_pos_item := 0; lookaheads_item := lookahead_set_13 |} ]%list.
Extract Inlined Constant items_of_state_16 => "assert false".

Definition items_of_state_17 : list item :=
  [ {| prod_item := Prod'param'0; dot_pos_item := 1; lookaheads_item := lookahead_set_14 |} ]%list.
Extract Inlined Constant items_of_state_17 => "assert false".

Definition items_of_state_18 : list item :=
  [ {| prod_item := Prod'param'0; dot_pos_item := 2; lookaheads_item := lookahead_set_14 |} ]%list.
Extract Inlined Constant items_of_state_18 => "assert false".

Definition items_of_state_19 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'param'0; dot_pos_item := 3; lookaheads_item := lookahead_set_14 |} ]%list.
Extract Inlined Constant items_of_state_19 => "assert false".

Definition items_of_state_20 : list item :=
  [ {| prod_item := Prod'fnbinder'1; dot_pos_item := 1; lookaheads_item := lookahead_set_3 |} ]%list.
Extract Inlined Constant items_of_state_20 => "assert false".

Definition items_of_state_21 : list item :=
  [ {| prod_item := Prod'param'0; dot_pos_item := 4; lookaheads_item := lookahead_set_14 |} ]%list.
Extract Inlined Constant items_of_state_21 => "assert false".

Definition items_of_state_22 : list item :=
  [ {| prod_item := Prod'param'0; dot_pos_item := 5; lookaheads_item := lookahead_set_14 |} ]%list.
Extract Inlined Constant items_of_state_22 => "assert false".

Definition items_of_state_23 : list item :=
  [ {| prod_item := Prod'obj'0; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'param'0; dot_pos_item := 0; lookaheads_item := lookahead_set_15 |};
    {| prod_item := Prod'params'0; dot_pos_item := 0; lookaheads_item := lookahead_set_15 |};
    {| prod_item := Prod'params'1; dot_pos_item := 0; lookaheads_item := lookahead_set_15 |} ]%list.
Extract Inlined Constant items_of_state_23 => "assert false".

Definition items_of_state_24 : list item :=
  [ {| prod_item := Prod'obj'0; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'param'0; dot_pos_item := 0; lookaheads_item := lookahead_set_15 |};
    {| prod_item := Prod'params'0; dot_pos_item := 1; lookaheads_item := lookahead_set_15 |} ]%list.
Extract Inlined Constant items_of_state_24 => "assert false".

Definition items_of_state_25 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 3; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_25 => "assert false".

Definition items_of_state_26 : list item :=
  [ {| prod_item := Prod'obj'0; dot_pos_item := 4; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_26 => "assert false".

Definition items_of_state_27 : list item :=
  [ {| prod_item := Prod'obj'1; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_27 => "assert false".

Definition items_of_state_28 : list item :=
  [ {| prod_item := Prod'app_obj'1; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_28 => "assert false".

Definition items_of_state_29 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_29 => "assert false".

Definition items_of_state_30 : list item :=
  [ {| prod_item := Prod'eq_obj'0; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_30 => "assert false".

Definition items_of_state_31 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 3; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |} ]%list.
Extract Inlined Constant items_of_state_31 => "assert false".

Definition items_of_state_32 : list item :=
  [ {| prod_item := Prod'eq_obj'0; dot_pos_item := 4; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_32 => "assert false".

Definition items_of_state_33 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 5; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_33 => "assert false".

Definition items_of_state_34 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 1; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_18 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 6; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_34 => "assert false".

Definition items_of_state_35 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 2; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_35 => "assert false".

Definition items_of_state_36 : list item :=
  [ {| prod_item := Prod'params'0; dot_pos_item := 2; lookaheads_item := lookahead_set_15 |} ]%list.
Extract Inlined Constant items_of_state_36 => "assert false".

Definition items_of_state_37 : list item :=
  [ {| prod_item := Prod'params'1; dot_pos_item := 1; lookaheads_item := lookahead_set_15 |} ]%list.
Extract Inlined Constant items_of_state_37 => "assert false".

Definition items_of_state_38 : list item :=
  [ {| prod_item := Prod'let_defn'0; dot_pos_item := 2; lookaheads_item := lookahead_set_12 |} ]%list.
Extract Inlined Constant items_of_state_38 => "assert false".

Definition items_of_state_39 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'let_defn'0; dot_pos_item := 3; lookaheads_item := lookahead_set_12 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |} ]%list.
Extract Inlined Constant items_of_state_39 => "assert false".

Definition items_of_state_40 : list item :=
  [ {| prod_item := Prod'let_defn'0; dot_pos_item := 4; lookaheads_item := lookahead_set_12 |} ]%list.
Extract Inlined Constant items_of_state_40 => "assert false".

Definition items_of_state_41 : list item :=
  [ {| prod_item := Prod'let_defn'0; dot_pos_item := 5; lookaheads_item := lookahead_set_12 |} ]%list.
Extract Inlined Constant items_of_state_41 => "assert false".

Definition items_of_state_42 : list item :=
  [ {| prod_item := Prod'let_defn'0; dot_pos_item := 0; lookaheads_item := lookahead_set_12 |};
    {| prod_item := Prod'let_defns'0; dot_pos_item := 1; lookaheads_item := lookahead_set_12 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_42 => "assert false".

Definition items_of_state_43 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_5 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 3; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_43 => "assert false".

Definition items_of_state_44 : list item :=
  [ {| prod_item := Prod'obj'6; dot_pos_item := 4; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_44 => "assert false".

Definition items_of_state_45 : list item :=
  [ {| prod_item := Prod'let_defns'0; dot_pos_item := 2; lookaheads_item := lookahead_set_12 |} ]%list.
Extract Inlined Constant items_of_state_45 => "assert false".

Definition items_of_state_46 : list item :=
  [ {| prod_item := Prod'let_defns'1; dot_pos_item := 1; lookaheads_item := lookahead_set_12 |} ]%list.
Extract Inlined Constant items_of_state_46 => "assert false".

Definition items_of_state_47 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'optional_as_nat'0; dot_pos_item := 0; lookaheads_item := lookahead_set_19 |};
    {| prod_item := Prod'optional_as_nat'1; dot_pos_item := 0; lookaheads_item := lookahead_set_19 |} ]%list.
Extract Inlined Constant items_of_state_47 => "assert false".

Definition items_of_state_48 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 3; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'optional_as_nat'0; dot_pos_item := 1; lookaheads_item := lookahead_set_19 |} ]%list.
Extract Inlined Constant items_of_state_48 => "assert false".

Definition items_of_state_49 : list item :=
  [ {| prod_item := Prod'optional_as_nat'0; dot_pos_item := 2; lookaheads_item := lookahead_set_19 |} ]%list.
Extract Inlined Constant items_of_state_49 => "assert false".

Definition items_of_state_50 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 4; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_50 => "assert false".

Definition items_of_state_51 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 1; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_20 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 5; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_51 => "assert false".

Definition items_of_state_52 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 6; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_52 => "assert false".

Definition items_of_state_53 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_16 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 7; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |} ]%list.
Extract Inlined Constant items_of_state_53 => "assert false".

Definition items_of_state_54 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 8; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_54 => "assert false".

Definition items_of_state_55 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 9; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_55 => "assert false".

Definition items_of_state_56 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 1; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_21 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 10; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_56 => "assert false".

Definition items_of_state_57 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 11; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_57 => "assert false".

Definition items_of_state_58 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 12; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_58 => "assert false".

Definition items_of_state_59 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 13; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_59 => "assert false".

Definition items_of_state_60 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 14; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_60 => "assert false".

Definition items_of_state_61 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 15; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_61 => "assert false".

Definition items_of_state_62 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 16; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |} ]%list.
Extract Inlined Constant items_of_state_62 => "assert false".

Definition items_of_state_63 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 17; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_63 => "assert false".

Definition items_of_state_64 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 18; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_64 => "assert false".

Definition items_of_state_65 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 19; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_65 => "assert false".

Definition items_of_state_66 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 20; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_66 => "assert false".

Definition items_of_state_67 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 21; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |} ]%list.
Extract Inlined Constant items_of_state_67 => "assert false".

Definition items_of_state_68 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 22; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_68 => "assert false".

Definition items_of_state_69 : list item :=
  [ {| prod_item := Prod'obj'3; dot_pos_item := 23; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_69 => "assert false".

Definition items_of_state_70 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 3; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_70 => "assert false".

Definition items_of_state_71 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 4; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_71 => "assert false".

Definition items_of_state_72 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 5; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_72 => "assert false".

Definition items_of_state_73 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 6; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |} ]%list.
Extract Inlined Constant items_of_state_73 => "assert false".

Definition items_of_state_74 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 7; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_74 => "assert false".

Definition items_of_state_75 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 8; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_75 => "assert false".

Definition items_of_state_76 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 9; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_76 => "assert false".

Definition items_of_state_77 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_22 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 10; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |} ]%list.
Extract Inlined Constant items_of_state_77 => "assert false".

Definition items_of_state_78 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 11; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_78 => "assert false".

Definition items_of_state_79 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 12; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_79 => "assert false".

Definition items_of_state_80 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 13; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_80 => "assert false".

Definition items_of_state_81 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 14; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_81 => "assert false".

Definition items_of_state_82 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 15; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_82 => "assert false".

Definition items_of_state_83 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 16; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_83 => "assert false".

Definition items_of_state_84 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_24 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 17; lookaheads_item := lookahead_set_6 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |} ]%list.
Extract Inlined Constant items_of_state_84 => "assert false".

Definition items_of_state_85 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 18; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_85 => "assert false".

Definition items_of_state_86 : list item :=
  [ {| prod_item := Prod'obj'2; dot_pos_item := 19; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_86 => "assert false".

Definition items_of_state_87 : list item :=
  [ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 2; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_87 => "assert false".

Definition items_of_state_88 : list item :=
  [ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 3; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_88 => "assert false".

Definition items_of_state_89 : list item :=
  [ {| prod_item := Prod'obj'5; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_89 => "assert false".

Definition items_of_state_91 : list item :=
  [ {| prod_item := Prod'prog'0; dot_pos_item := 1; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_91 => "assert false".

Definition items_of_state_92 : list item :=
  [ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_26 |};
    {| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_26 |};
    {| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_26 |};
    {| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_26 |};
    {| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_26 |};
    {| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_26 |};
    {| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_26 |};
    {| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_26 |};
    {| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'fnbinder'0; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'fnbinder'1; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
    {| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
    {| prod_item := Prod'prog'0; dot_pos_item := 2; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_92 => "assert false".

Definition items_of_state_93 : list item :=
  [ {| prod_item := Prod'prog'0; dot_pos_item := 3; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_93 => "assert false".

Definition items_of_state_94 : list item :=
  [ {| prod_item := Prod'prog'0; dot_pos_item := 4; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_94 => "assert false".

Definition items_of_state (s:state) : list item :=
  match s with
  | Init Init'0 => items_of_state_0
  | Ninit Nis'1 => items_of_state_1
  | Ninit Nis'2 => items_of_state_2
  | Ninit Nis'3 => items_of_state_3
  | Ninit Nis'4 => items_of_state_4
  | Ninit Nis'5 => items_of_state_5
  | Ninit Nis'6 => items_of_state_6
  | Ninit Nis'7 => items_of_state_7
  | Ninit Nis'8 => items_of_state_8
  | Ninit Nis'9 => items_of_state_9
  | Ninit Nis'10 => items_of_state_10
  | Ninit Nis'11 => items_of_state_11
  | Ninit Nis'12 => items_of_state_12
  | Ninit Nis'13 => items_of_state_13
  | Ninit Nis'14 => items_of_state_14
  | Ninit Nis'15 => items_of_state_15
  | Ninit Nis'16 => items_of_state_16
  | Ninit Nis'17 => items_of_state_17
  | Ninit Nis'18 => items_of_state_18
  | Ninit Nis'19 => items_of_state_19
  | Ninit Nis'20 => items_of_state_20
  | Ninit Nis'21 => items_of_state_21
  | Ninit Nis'22 => items_of_state_22
  | Ninit Nis'23 => items_of_state_23
  | Ninit Nis'24 => items_of_state_24
  | Ninit Nis'25 => items_of_state_25
  | Ninit Nis'26 => items_of_state_26
  | Ninit Nis'27 => items_of_state_27
  | Ninit Nis'28 => items_of_state_28
  | Ninit Nis'29 => items_of_state_29
  | Ninit Nis'30 => items_of_state_30
  | Ninit Nis'31 => items_of_state_31
  | Ninit Nis'32 => items_of_state_32
  | Ninit Nis'33 => items_of_state_33
  | Ninit Nis'34 => items_of_state_34
  | Ninit Nis'35 => items_of_state_35
  | Ninit Nis'36 => items_of_state_36
  | Ninit Nis'37 => items_of_state_37
  | Ninit Nis'38 => items_of_state_38
  | Ninit Nis'39 => items_of_state_39
  | Ninit Nis'40 => items_of_state_40
  | Ninit Nis'41 => items_of_state_41
  | Ninit Nis'42 => items_of_state_42
  | Ninit Nis'43 => items_of_state_43
  | Ninit Nis'44 => items_of_state_44
  | Ninit Nis'45 => items_of_state_45
  | Ninit Nis'46 => items_of_state_46
  | Ninit Nis'47 => items_of_state_47
  | Ninit Nis'48 => items_of_state_48
  | Ninit Nis'49 => items_of_state_49
  | Ninit Nis'50 => items_of_state_50
  | Ninit Nis'51 => items_of_state_51
  | Ninit Nis'52 => items_of_state_52
  | Ninit Nis'53 => items_of_state_53
  | Ninit Nis'54 => items_of_state_54
  | Ninit Nis'55 => items_of_state_55
  | Ninit Nis'56 => items_of_state_56
  | Ninit Nis'57 => items_of_state_57
  | Ninit Nis'58 => items_of_state_58
  | Ninit Nis'59 => items_of_state_59
  | Ninit Nis'60 => items_of_state_60
  | Ninit Nis'61 => items_of_state_61
  | Ninit Nis'62 => items_of_state_62
  | Ninit Nis'63 => items_of_state_63
  | Ninit Nis'64 => items_of_state_64
  | Ninit Nis'65 => items_of_state_65
  | Ninit Nis'66 => items_of_state_66
  | Ninit Nis'67 => items_of_state_67
  | Ninit Nis'68 => items_of_state_68
  | Ninit Nis'69 => items_of_state_69
  | Ninit Nis'70 => items_of_state_70
  | Ninit Nis'71 => items_of_state_71
  | Ninit Nis'72 => items_of_state_72
  | Ninit Nis'73 => items_of_state_73
  | Ninit Nis'74 => items_of_state_74
  | Ninit Nis'75 => items_of_state_75
  | Ninit Nis'76 => items_of_state_76
  | Ninit Nis'77 => items_of_state_77
  | Ninit Nis'78 => items_of_state_78
  | Ninit Nis'79 => items_of_state_79
  | Ninit Nis'80 => items_of_state_80
  | Ninit Nis'81 => items_of_state_81
  | Ninit Nis'82 => items_of_state_82
  | Ninit Nis'83 => items_of_state_83
  | Ninit Nis'84 => items_of_state_84
  | Ninit Nis'85 => items_of_state_85
  | Ninit Nis'86 => items_of_state_86
  | Ninit Nis'87 => items_of_state_87
  | Ninit Nis'88 => items_of_state_88
  | Ninit Nis'89 => items_of_state_89
  | Ninit Nis'91 => items_of_state_91
  | Ninit Nis'92 => items_of_state_92
  | Ninit Nis'93 => items_of_state_93
  | Ninit Nis'94 => items_of_state_94
  end.
Extract Constant items_of_state => "fun _ -> assert false".

Definition N_of_state (s:state) : N :=
  match s with
  | Init Init'0 => 0%N
  | Ninit Nis'1 => 1%N
  | Ninit Nis'2 => 2%N
  | Ninit Nis'3 => 3%N
  | Ninit Nis'4 => 4%N
  | Ninit Nis'5 => 5%N
  | Ninit Nis'6 => 6%N
  | Ninit Nis'7 => 7%N
  | Ninit Nis'8 => 8%N
  | Ninit Nis'9 => 9%N
  | Ninit Nis'10 => 10%N
  | Ninit Nis'11 => 11%N
  | Ninit Nis'12 => 12%N
  | Ninit Nis'13 => 13%N
  | Ninit Nis'14 => 14%N
  | Ninit Nis'15 => 15%N
  | Ninit Nis'16 => 16%N
  | Ninit Nis'17 => 17%N
  | Ninit Nis'18 => 18%N
  | Ninit Nis'19 => 19%N
  | Ninit Nis'20 => 20%N
  | Ninit Nis'21 => 21%N
  | Ninit Nis'22 => 22%N
  | Ninit Nis'23 => 23%N
  | Ninit Nis'24 => 24%N
  | Ninit Nis'25 => 25%N
  | Ninit Nis'26 => 26%N
  | Ninit Nis'27 => 27%N
  | Ninit Nis'28 => 28%N
  | Ninit Nis'29 => 29%N
  | Ninit Nis'30 => 30%N
  | Ninit Nis'31 => 31%N
  | Ninit Nis'32 => 32%N
  | Ninit Nis'33 => 33%N
  | Ninit Nis'34 => 34%N
  | Ninit Nis'35 => 35%N
  | Ninit Nis'36 => 36%N
  | Ninit Nis'37 => 37%N
  | Ninit Nis'38 => 38%N
  | Ninit Nis'39 => 39%N
  | Ninit Nis'40 => 40%N
  | Ninit Nis'41 => 41%N
  | Ninit Nis'42 => 42%N
  | Ninit Nis'43 => 43%N
  | Ninit Nis'44 => 44%N
  | Ninit Nis'45 => 45%N
  | Ninit Nis'46 => 46%N
  | Ninit Nis'47 => 47%N
  | Ninit Nis'48 => 48%N
  | Ninit Nis'49 => 49%N
  | Ninit Nis'50 => 50%N
  | Ninit Nis'51 => 51%N
  | Ninit Nis'52 => 52%N
  | Ninit Nis'53 => 53%N
  | Ninit Nis'54 => 54%N
  | Ninit Nis'55 => 55%N
  | Ninit Nis'56 => 56%N
  | Ninit Nis'57 => 57%N
  | Ninit Nis'58 => 58%N
  | Ninit Nis'59 => 59%N
  | Ninit Nis'60 => 60%N
  | Ninit Nis'61 => 61%N
  | Ninit Nis'62 => 62%N
  | Ninit Nis'63 => 63%N
  | Ninit Nis'64 => 64%N
  | Ninit Nis'65 => 65%N
  | Ninit Nis'66 => 66%N
  | Ninit Nis'67 => 67%N
  | Ninit Nis'68 => 68%N
  | Ninit Nis'69 => 69%N
  | Ninit Nis'70 => 70%N
  | Ninit Nis'71 => 71%N
  | Ninit Nis'72 => 72%N
  | Ninit Nis'73 => 73%N
  | Ninit Nis'74 => 74%N
  | Ninit Nis'75 => 75%N
  | Ninit Nis'76 => 76%N
  | Ninit Nis'77 => 77%N
  | Ninit Nis'78 => 78%N
  | Ninit Nis'79 => 79%N
  | Ninit Nis'80 => 80%N
  | Ninit Nis'81 => 81%N
  | Ninit Nis'82 => 82%N
  | Ninit Nis'83 => 83%N
  | Ninit Nis'84 => 84%N
  | Ninit Nis'85 => 85%N
  | Ninit Nis'86 => 86%N
  | Ninit Nis'87 => 87%N
  | Ninit Nis'88 => 88%N
  | Ninit Nis'89 => 89%N
  | Ninit Nis'91 => 91%N
  | Ninit Nis'92 => 92%N
  | Ninit Nis'93 => 93%N
  | Ninit Nis'94 => 94%N
  end.
End Aut.

Module MenhirLibParser := MenhirLib.Main.Make Aut.
Theorem safe:
  MenhirLibParser.safe_validator tt = true.
Proof eq_refl true<:MenhirLibParser.safe_validator tt = true.

Theorem complete:
  MenhirLibParser.complete_validator tt = true.
Proof eq_refl true<:MenhirLibParser.complete_validator tt = true.

Definition prog : nat -> MenhirLibParser.Inter.buffer -> MenhirLibParser.Inter.parse_result (Cst.obj * Cst.obj) := MenhirLibParser.parse safe Aut.Init'0.

Theorem prog_correct (log_fuel : nat) (buffer : MenhirLibParser.Inter.buffer):
  match prog log_fuel buffer with
  | MenhirLibParser.Inter.Parsed_pr sem buffer_new =>
      exists word (tree : Gram.parse_tree (NT prog'nt) word),
        buffer = MenhirLibParser.Inter.app_buf word buffer_new /\
        Gram.pt_sem tree = sem
  | _ => True
  end.
Proof. apply MenhirLibParser.parse_correct with (init:=Aut.Init'0). Qed.

Theorem prog_complete (log_fuel : nat) (word : list token) (buffer_end : MenhirLibParser.Inter.buffer) :
  forall tree : Gram.parse_tree (NT prog'nt) word,
  match prog log_fuel (MenhirLibParser.Inter.app_buf word buffer_end) with
  | MenhirLibParser.Inter.Fail_pr => False
  | MenhirLibParser.Inter.Parsed_pr output_res buffer_end_res =>
      output_res = Gram.pt_sem tree /\
      buffer_end_res = buffer_end /\ (Gram.pt_size tree <= PeanoNat.Nat.pow 2 log_fuel)%nat
  | MenhirLibParser.Inter.Timeout_pr => (PeanoNat.Nat.pow 2 log_fuel < Gram.pt_size tree)%nat
  end.
Proof. apply MenhirLibParser.parse_complete with (init:=Aut.Init'0); exact complete. Qed.

Extract Constant loc => "Lexing.position * Lexing.position".