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_20250903.
Unset Elimination Schemes.
Inductive token : Type :=
| ZERO : (loc)%type -> token
| VAR : (loc*string)%type -> token
| TYPE : (loc)%type -> token
| SUCC : (loc)%type -> token
| SND : (loc)%type -> token
| SIGMA : (loc)%type -> token
| RPAREN : (loc)%type -> token
| RETURN : (loc)%type -> token
| REFL : (loc)%type -> token
| REC : (loc)%type -> token
| RCURLY : (loc)%type -> token
| RANGLE : (loc)%type -> token
| PI : (loc)%type -> token
| NAT : (loc)%type -> token
| LPAREN : (loc)%type -> token
| LET : (loc)%type -> token
| LCURLY : (loc)%type -> token
| LANGLE : (loc)%type -> token
| LAMBDA : (loc)%type -> token
| INT : (loc*nat)%type -> token
| IN : (loc)%type -> token
| FST : (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
| FST't
| IN't
| INT't
| LAMBDA't
| LANGLE't
| LCURLY't
| LET't
| LPAREN't
| NAT't
| PI't
| RANGLE't
| RCURLY't
| REC't
| REFL't
| RETURN't
| RPAREN't
| SIGMA't
| SND'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
| FST't => 13%positive
| IN't => 14%positive
| INT't => 15%positive
| LAMBDA't => 16%positive
| LANGLE't => 17%positive
| LCURLY't => 18%positive
| LET't => 19%positive
| LPAREN't => 20%positive
| NAT't => 21%positive
| PI't => 22%positive
| RANGLE't => 23%positive
| RCURLY't => 24%positive
| REC't => 25%positive
| REFL't => 26%positive
| RETURN't => 27%positive
| RPAREN't => 28%positive
| SIGMA't => 29%positive
| SND't => 30%positive
| SUCC't => 31%positive
| TYPE't => 32%positive
| VAR't => 33%positive
| ZERO't => 34%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 => FST't
| 14%positive => IN't
| 15%positive => INT't
| 16%positive => LAMBDA't
| 17%positive => LANGLE't
| 18%positive => LCURLY't
| 19%positive => LET't
| 20%positive => LPAREN't
| 21%positive => NAT't
| 22%positive => PI't
| 23%positive => RANGLE't
| 24%positive => RCURLY't
| 25%positive => REC't
| 26%positive => REFL't
| 27%positive => RETURN't
| 28%positive => RPAREN't
| 29%positive => SIGMA't
| 30%positive => SND't
| 31%positive => SUCC't
| 32%positive => TYPE't
| 33%positive => VAR't
| 34%positive => ZERO't
| _ => ARROW't
end)%Z;
inj_bound := 34%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
| SND't => (loc)%type
| SIGMA't => (loc)%type
| RPAREN't => (loc)%type
| RETURN't => (loc)%type
| REFL't => (loc)%type
| REC't => (loc)%type
| RCURLY't => (loc)%type
| RANGLE't => (loc)%type
| PI't => (loc)%type
| NAT't => (loc)%type
| LPAREN't => (loc)%type
| LET't => (loc)%type
| LCURLY't => (loc)%type
| LANGLE't => (loc)%type
| LAMBDA't => (loc)%type
| INT't => (loc*nat)%type
| IN't => (loc)%type
| FST'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
| SND _ => SND't
| SIGMA _ => SIGMA't
| RPAREN _ => RPAREN't
| RETURN _ => RETURN't
| REFL _ => REFL't
| REC _ => REC't
| RCURLY _ => RCURLY't
| RANGLE _ => RANGLE't
| PI _ => PI't
| NAT _ => NAT't
| LPAREN _ => LPAREN't
| LET _ => LET't
| LCURLY _ => LCURLY't
| LANGLE _ => LANGLE't
| LAMBDA _ => LAMBDA't
| INT _ => INT't
| IN _ => IN't
| FST _ => FST'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
| SND x => x
| SIGMA x => x
| RPAREN x => x
| RETURN x => x
| REFL x => x
| REC x => x
| RCURLY x => x
| RANGLE x => x
| PI x => x
| NAT x => x
| LPAREN x => x
| LET x => x
| LCURLY x => x
| LANGLE x => x
| LAMBDA x => x
| INT x => x
| IN x => x
| FST 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'8
| Prod'obj'7
| 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'2
| Prod'fnbinder'1
| Prod'fnbinder'0
| Prod'eq_obj'1
| Prod'eq_obj'0
| Prod'atomic_obj'6
| 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'8 => 7%positive
| Prod'obj'7 => 8%positive
| Prod'obj'6 => 9%positive
| Prod'obj'5 => 10%positive
| Prod'obj'4 => 11%positive
| Prod'obj'3 => 12%positive
| Prod'obj'2 => 13%positive
| Prod'obj'1 => 14%positive
| Prod'obj'0 => 15%positive
| Prod'let_defns'1 => 16%positive
| Prod'let_defns'0 => 17%positive
| Prod'let_defn'0 => 18%positive
| Prod'fnbinder'2 => 19%positive
| Prod'fnbinder'1 => 20%positive
| Prod'fnbinder'0 => 21%positive
| Prod'eq_obj'1 => 22%positive
| Prod'eq_obj'0 => 23%positive
| Prod'atomic_obj'6 => 24%positive
| Prod'atomic_obj'5 => 25%positive
| Prod'atomic_obj'4 => 26%positive
| Prod'atomic_obj'3 => 27%positive
| Prod'atomic_obj'2 => 28%positive
| Prod'atomic_obj'1 => 29%positive
| Prod'atomic_obj'0 => 30%positive
| Prod'app_obj'1 => 31%positive
| Prod'app_obj'0 => 32%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'8
| 8%positive => Prod'obj'7
| 9%positive => Prod'obj'6
| 10%positive => Prod'obj'5
| 11%positive => Prod'obj'4
| 12%positive => Prod'obj'3
| 13%positive => Prod'obj'2
| 14%positive => Prod'obj'1
| 15%positive => Prod'obj'0
| 16%positive => Prod'let_defns'1
| 17%positive => Prod'let_defns'0
| 18%positive => Prod'let_defn'0
| 19%positive => Prod'fnbinder'2
| 20%positive => Prod'fnbinder'1
| 21%positive => Prod'fnbinder'0
| 22%positive => Prod'eq_obj'1
| 23%positive => Prod'eq_obj'0
| 24%positive => Prod'atomic_obj'6
| 25%positive => Prod'atomic_obj'5
| 26%positive => Prod'atomic_obj'4
| 27%positive => Prod'atomic_obj'3
| 28%positive => Prod'atomic_obj'2
| 29%positive => Prod'atomic_obj'1
| 30%positive => Prod'atomic_obj'0
| 31%positive => Prod'app_obj'1
| 32%positive => Prod'app_obj'0
| _ => Prod'prog'0
end)%Z;
inj_bound := 32%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 RANGLE't; NT obj'nt; T DOT't; T VAR't; T COLON't; NT obj'nt; T COMMA't; NT obj'nt; T COLON't; NT obj'nt; T LANGLE't]%list)
(fun _11 snd_ty _9 x _7 snd_tm _5 fst_ty _3 fst_tm _1 =>
( Cst.pair fst_tm fst_ty snd_tm (snd x) snd_ty )
)
| Prod'atomic_obj'6 => 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 RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt]%list)
(fun rhs _5 ty _3 _2 lhs =>
( Cst.prop_eq lhs ty 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'fnbinder'2 => box
(fnbinder'nt, [T SIGMA't]%list)
(fun _1 =>
( Cst.sigma )
)
| 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 RCURLY't; NT obj'nt; T LCURLY'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 ty _7 _6 lhs _4 _3 escr _1 =>
( Cst.eqrec escr (snd mx) (snd my) (snd mz) em (snd rx) er lhs ty rhs )
)
| Prod'obj'4 => box
(obj'nt, [NT atomic_obj'nt; NT atomic_obj'nt; T REFL't]%list)
(fun e ty _1 =>
( Cst.refl ty 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 atomic_obj'nt; T FST't]%list)
(fun atomic_obj _1 =>
( Cst.fst atomic_obj )
)
| Prod'obj'7 => box
(obj'nt, [NT atomic_obj'nt; T SND't]%list)
(fun atomic_obj _1 =>
( Cst.snd atomic_obj )
)
| Prod'obj'8 => 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 ty _2 exp =>
(exp, ty)
)
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; SND't; SIGMA't; REFL't; REC't; PI't; NAT't; LPAREN't; LET't; LANGLE't; LAMBDA't; INT't; FST'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; SND't; SIGMA't; REFL't; REC't; PI't; NAT't; LPAREN't; LET't; LANGLE't; LAMBDA't; INT't; FST't]%list
| let_defns'nt => [LPAREN't]%list
| let_defn'nt => [LPAREN't]%list
| fnbinder'nt => [SIGMA't; PI't; LAMBDA't]%list
| eq_obj'nt => [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; LANGLE't; INT't]%list
| atomic_obj'nt => [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; LANGLE't; INT't]%list
| app_obj'nt => [ZERO't; VAR't; TYPE't; NAT't; LPAREN't; LANGLE't; INT't]%list
end.
Inductive noninitstate' : Set :=
| Nis'110
| Nis'109
| Nis'108
| Nis'107
| Nis'105
| Nis'104
| Nis'103
| Nis'102
| Nis'101
| Nis'100
| Nis'99
| Nis'98
| Nis'97
| Nis'96
| Nis'95
| Nis'94
| Nis'93
| Nis'92
| Nis'91
| Nis'90
| 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'110 => 1%positive
| Nis'109 => 2%positive
| Nis'108 => 3%positive
| Nis'107 => 4%positive
| Nis'105 => 5%positive
| Nis'104 => 6%positive
| Nis'103 => 7%positive
| Nis'102 => 8%positive
| Nis'101 => 9%positive
| Nis'100 => 10%positive
| Nis'99 => 11%positive
| Nis'98 => 12%positive
| Nis'97 => 13%positive
| Nis'96 => 14%positive
| Nis'95 => 15%positive
| Nis'94 => 16%positive
| Nis'93 => 17%positive
| Nis'92 => 18%positive
| Nis'91 => 19%positive
| Nis'90 => 20%positive
| Nis'89 => 21%positive
| Nis'88 => 22%positive
| Nis'87 => 23%positive
| Nis'86 => 24%positive
| Nis'85 => 25%positive
| Nis'84 => 26%positive
| Nis'83 => 27%positive
| Nis'82 => 28%positive
| Nis'81 => 29%positive
| Nis'80 => 30%positive
| Nis'79 => 31%positive
| Nis'78 => 32%positive
| Nis'77 => 33%positive
| Nis'76 => 34%positive
| Nis'75 => 35%positive
| Nis'74 => 36%positive
| Nis'73 => 37%positive
| Nis'72 => 38%positive
| Nis'71 => 39%positive
| Nis'70 => 40%positive
| Nis'69 => 41%positive
| Nis'68 => 42%positive
| Nis'67 => 43%positive
| Nis'66 => 44%positive
| Nis'65 => 45%positive
| Nis'64 => 46%positive
| Nis'63 => 47%positive
| Nis'62 => 48%positive
| Nis'61 => 49%positive
| Nis'60 => 50%positive
| Nis'59 => 51%positive
| Nis'58 => 52%positive
| Nis'57 => 53%positive
| Nis'56 => 54%positive
| Nis'55 => 55%positive
| Nis'54 => 56%positive
| Nis'53 => 57%positive
| Nis'52 => 58%positive
| Nis'51 => 59%positive
| Nis'50 => 60%positive
| Nis'49 => 61%positive
| Nis'48 => 62%positive
| Nis'47 => 63%positive
| Nis'46 => 64%positive
| Nis'45 => 65%positive
| Nis'44 => 66%positive
| Nis'43 => 67%positive
| Nis'42 => 68%positive
| Nis'41 => 69%positive
| Nis'40 => 70%positive
| Nis'39 => 71%positive
| Nis'38 => 72%positive
| Nis'37 => 73%positive
| Nis'36 => 74%positive
| Nis'35 => 75%positive
| Nis'34 => 76%positive
| Nis'33 => 77%positive
| Nis'32 => 78%positive
| Nis'31 => 79%positive
| Nis'30 => 80%positive
| Nis'29 => 81%positive
| Nis'28 => 82%positive
| Nis'27 => 83%positive
| Nis'26 => 84%positive
| Nis'25 => 85%positive
| Nis'24 => 86%positive
| Nis'23 => 87%positive
| Nis'22 => 88%positive
| Nis'21 => 89%positive
| Nis'20 => 90%positive
| Nis'19 => 91%positive
| Nis'18 => 92%positive
| Nis'17 => 93%positive
| Nis'16 => 94%positive
| Nis'15 => 95%positive
| Nis'14 => 96%positive
| Nis'13 => 97%positive
| Nis'12 => 98%positive
| Nis'11 => 99%positive
| Nis'10 => 100%positive
| Nis'9 => 101%positive
| Nis'8 => 102%positive
| Nis'7 => 103%positive
| Nis'6 => 104%positive
| Nis'5 => 105%positive
| Nis'4 => 106%positive
| Nis'3 => 107%positive
| Nis'2 => 108%positive
| Nis'1 => 109%positive
end;
surj := (fun n => match n return _ with
| 1%positive => Nis'110
| 2%positive => Nis'109
| 3%positive => Nis'108
| 4%positive => Nis'107
| 5%positive => Nis'105
| 6%positive => Nis'104
| 7%positive => Nis'103
| 8%positive => Nis'102
| 9%positive => Nis'101
| 10%positive => Nis'100
| 11%positive => Nis'99
| 12%positive => Nis'98
| 13%positive => Nis'97
| 14%positive => Nis'96
| 15%positive => Nis'95
| 16%positive => Nis'94
| 17%positive => Nis'93
| 18%positive => Nis'92
| 19%positive => Nis'91
| 20%positive => Nis'90
| 21%positive => Nis'89
| 22%positive => Nis'88
| 23%positive => Nis'87
| 24%positive => Nis'86
| 25%positive => Nis'85
| 26%positive => Nis'84
| 27%positive => Nis'83
| 28%positive => Nis'82
| 29%positive => Nis'81
| 30%positive => Nis'80
| 31%positive => Nis'79
| 32%positive => Nis'78
| 33%positive => Nis'77
| 34%positive => Nis'76
| 35%positive => Nis'75
| 36%positive => Nis'74
| 37%positive => Nis'73
| 38%positive => Nis'72
| 39%positive => Nis'71
| 40%positive => Nis'70
| 41%positive => Nis'69
| 42%positive => Nis'68
| 43%positive => Nis'67
| 44%positive => Nis'66
| 45%positive => Nis'65
| 46%positive => Nis'64
| 47%positive => Nis'63
| 48%positive => Nis'62
| 49%positive => Nis'61
| 50%positive => Nis'60
| 51%positive => Nis'59
| 52%positive => Nis'58
| 53%positive => Nis'57
| 54%positive => Nis'56
| 55%positive => Nis'55
| 56%positive => Nis'54
| 57%positive => Nis'53
| 58%positive => Nis'52
| 59%positive => Nis'51
| 60%positive => Nis'50
| 61%positive => Nis'49
| 62%positive => Nis'48
| 63%positive => Nis'47
| 64%positive => Nis'46
| 65%positive => Nis'45
| 66%positive => Nis'44
| 67%positive => Nis'43
| 68%positive => Nis'42
| 69%positive => Nis'41
| 70%positive => Nis'40
| 71%positive => Nis'39
| 72%positive => Nis'38
| 73%positive => Nis'37
| 74%positive => Nis'36
| 75%positive => Nis'35
| 76%positive => Nis'34
| 77%positive => Nis'33
| 78%positive => Nis'32
| 79%positive => Nis'31
| 80%positive => Nis'30
| 81%positive => Nis'29
| 82%positive => Nis'28
| 83%positive => Nis'27
| 84%positive => Nis'26
| 85%positive => Nis'25
| 86%positive => Nis'24
| 87%positive => Nis'23
| 88%positive => Nis'22
| 89%positive => Nis'21
| 90%positive => Nis'20
| 91%positive => Nis'19
| 92%positive => Nis'18
| 93%positive => Nis'17
| 94%positive => Nis'16
| 95%positive => Nis'15
| 96%positive => Nis'14
| 97%positive => Nis'13
| 98%positive => Nis'12
| 99%positive => Nis'11
| 100%positive => Nis'10
| 101%positive => Nis'9
| 102%positive => Nis'8
| 103%positive => Nis'7
| 104%positive => Nis'6
| 105%positive => Nis'5
| 106%positive => Nis'4
| 107%positive => Nis'3
| 108%positive => Nis'2
| 109%positive => Nis'1
| _ => Nis'110
end)%Z;
inj_bound := 109%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 SND't
| Nis'10 => T LANGLE't
| Nis'11 => T SIGMA't
| Nis'12 => T REFL't
| Nis'13 => T INT't
| Nis'14 => NT atomic_obj'nt
| Nis'15 => NT atomic_obj'nt
| Nis'16 => T REC't
| Nis'17 => T PI't
| Nis'18 => T LET't
| Nis'19 => T LPAREN't
| Nis'20 => T LPAREN't
| Nis'21 => T VAR't
| Nis'22 => T COLON't
| Nis'23 => T LAMBDA't
| Nis'24 => T FST't
| Nis'25 => NT atomic_obj'nt
| Nis'26 => NT obj'nt
| Nis'27 => T RPAREN't
| Nis'28 => NT fnbinder'nt
| Nis'29 => NT params'nt
| Nis'30 => T ARROW't
| Nis'31 => NT obj'nt
| Nis'32 => NT eq_obj'nt
| Nis'33 => NT atomic_obj'nt
| Nis'34 => NT app_obj'nt
| Nis'35 => T EQ't
| Nis'36 => T LCURLY't
| Nis'37 => NT obj'nt
| Nis'38 => T RCURLY't
| Nis'39 => NT app_obj'nt
| Nis'40 => NT atomic_obj'nt
| Nis'41 => NT param'nt
| Nis'42 => NT param'nt
| Nis'43 => NT param'nt
| Nis'44 => T DEF't
| Nis'45 => NT obj'nt
| Nis'46 => T RPAREN't
| Nis'47 => NT let_defns'nt
| Nis'48 => T IN't
| Nis'49 => NT obj'nt
| Nis'50 => NT let_defn'nt
| Nis'51 => NT let_defn'nt
| Nis'52 => NT obj'nt
| Nis'53 => T AS't
| Nis'54 => T NAT't
| Nis'55 => T LPAREN't
| Nis'56 => NT app_obj'nt
| Nis'57 => T EQ't
| Nis'58 => T LCURLY't
| Nis'59 => NT obj'nt
| Nis'60 => T RCURLY't
| Nis'61 => NT app_obj'nt
| Nis'62 => T RPAREN't
| Nis'63 => T RETURN't
| Nis'64 => T VAR't
| Nis'65 => T VAR't
| Nis'66 => T VAR't
| Nis'67 => T DOT't
| Nis'68 => NT obj'nt
| Nis'69 => T BAR't
| Nis'70 => T REFL't
| Nis'71 => T VAR't
| Nis'72 => T DARROW't
| Nis'73 => NT obj'nt
| Nis'74 => T END't
| Nis'75 => NT optional_as_nat'nt
| Nis'76 => T RETURN't
| Nis'77 => T VAR't
| Nis'78 => T DOT't
| Nis'79 => NT obj'nt
| Nis'80 => T BAR't
| Nis'81 => T ZERO't
| Nis'82 => T DARROW't
| Nis'83 => NT obj'nt
| Nis'84 => T BAR't
| Nis'85 => T SUCC't
| Nis'86 => T VAR't
| Nis'87 => T COMMA't
| Nis'88 => T VAR't
| Nis'89 => T DARROW't
| Nis'90 => NT obj'nt
| Nis'91 => T END't
| Nis'92 => NT obj'nt
| Nis'93 => T COLON't
| Nis'94 => NT obj'nt
| Nis'95 => T COMMA't
| Nis'96 => NT obj'nt
| Nis'97 => T COLON't
| Nis'98 => T VAR't
| Nis'99 => T DOT't
| Nis'100 => NT obj'nt
| Nis'101 => T RANGLE't
| Nis'102 => NT atomic_obj'nt
| Nis'103 => NT obj'nt
| Nis'104 => T RPAREN't
| Nis'105 => NT atomic_obj'nt
| Nis'107 => NT obj'nt
| Nis'108 => T COLON't
| Nis'109 => NT obj'nt
| Nis'110 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (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 _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (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 _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'10 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'11 => Default_reduce_act Prod'fnbinder'2
| Ninit Nis'12 => 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 _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'13 => Default_reduce_act Prod'atomic_obj'3
| Ninit Nis'14 => 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 _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'15 => Default_reduce_act Prod'obj'4
| Ninit Nis'16 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'17 => Default_reduce_act Prod'fnbinder'0
| Ninit Nis'18 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| LPAREN'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
| LPAREN't => Shift_act Nis'20 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'20 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| VAR't => Shift_act Nis'21 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'21 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| COLON't => Shift_act Nis'22 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'22 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'23 => Default_reduce_act Prod'fnbinder'1
| Ninit Nis'24 => 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 _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'25 => Default_reduce_act Prod'obj'6
| Ninit Nis'26 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| RPAREN't => Shift_act Nis'27 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'27 => Default_reduce_act Prod'param'0
| Ninit Nis'28 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| LPAREN't => Shift_act Nis'20 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'29 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| LPAREN't => Shift_act Nis'20 (eq_refl _)
| ARROW't => Shift_act Nis'30 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'30 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'31 => Default_reduce_act Prod'obj'0
| Ninit Nis'32 => Default_reduce_act Prod'obj'1
| Ninit Nis'33 => Default_reduce_act Prod'app_obj'1
| 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'1
| SND't => Reduce_act Prod'eq_obj'1
| SIGMA'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
| RCURLY'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
| LCURLY't => Reduce_act Prod'eq_obj'1
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Reduce_act Prod'eq_obj'1
| INT't => Shift_act Nis'13 (eq_refl _)
| IN't => Reduce_act Prod'eq_obj'1
| FST't => Reduce_act Prod'eq_obj'1
| EQ't => Shift_act Nis'35 (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'35 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| LCURLY't => Shift_act Nis'36 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'36 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'37 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| RCURLY't => Shift_act Nis'38 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'38 => 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 _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (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 => Reduce_act Prod'eq_obj'0
| SND't => Reduce_act Prod'eq_obj'0
| SIGMA'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
| RCURLY'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
| LCURLY't => Reduce_act Prod'eq_obj'0
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Reduce_act Prod'eq_obj'0
| INT't => Shift_act Nis'13 (eq_refl _)
| IN't => Reduce_act Prod'eq_obj'0
| FST'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'40 => Default_reduce_act Prod'app_obj'0
| Ninit Nis'41 => Default_reduce_act Prod'params'0
| Ninit Nis'42 => Default_reduce_act Prod'params'1
| Ninit Nis'43 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| DEF't => Shift_act Nis'44 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'44 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'45 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| RPAREN't => Shift_act Nis'46 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'46 => Default_reduce_act Prod'let_defn'0
| Ninit Nis'47 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| LPAREN't => Shift_act Nis'19 (eq_refl _)
| IN'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
| 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'49 => Default_reduce_act Prod'obj'8
| Ninit Nis'50 => Default_reduce_act Prod'let_defns'0
| Ninit Nis'51 => Default_reduce_act Prod'let_defns'1
| Ninit Nis'52 => 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'53 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'53 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| NAT't => Shift_act Nis'54 (eq_refl _)
| LPAREN't => Shift_act Nis'55 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'54 => Default_reduce_act Prod'optional_as_nat'0
| 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 _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (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 _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| EQ't => Shift_act Nis'57 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'57 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| LCURLY'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
| 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'59 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| RCURLY'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
| 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 _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'61 => 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'62 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'62 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| RETURN't => Shift_act Nis'63 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'63 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| VAR'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
| VAR'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
| DOT'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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'68 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| BAR't => Shift_act Nis'69 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'69 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| REFL't => Shift_act Nis'70 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'70 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| VAR'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
| DARROW'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
| 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'73 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| END't => Shift_act Nis'74 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'74 => Default_reduce_act Prod'obj'3
| Ninit Nis'75 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| RETURN'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
| VAR'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
| DOT't => Shift_act Nis'78 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'78 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'79 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| BAR'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
| ZERO'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
| DARROW'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
| 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'83 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| BAR'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
| SUCC't => Shift_act Nis'85 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'85 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| VAR't => Shift_act Nis'86 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'86 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| COMMA't => Shift_act Nis'87 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'87 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| VAR't => Shift_act Nis'88 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'88 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| DARROW't => Shift_act Nis'89 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'89 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'90 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| END't => Shift_act Nis'91 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'91 => Default_reduce_act Prod'obj'2
| Ninit Nis'92 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| COLON't => Shift_act Nis'93 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'93 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'94 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| COMMA't => Shift_act Nis'95 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'95 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'96 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| COLON't => Shift_act Nis'97 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'97 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| VAR't => Shift_act Nis'98 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'98 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| DOT't => Shift_act Nis'99 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'99 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'100 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| RANGLE't => Shift_act Nis'101 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'101 => Default_reduce_act Prod'atomic_obj'5
| Ninit Nis'102 => Default_reduce_act Prod'obj'7
| Ninit Nis'103 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| RPAREN't => Shift_act Nis'104 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'104 => Default_reduce_act Prod'atomic_obj'6
| Ninit Nis'105 => Default_reduce_act Prod'obj'5
| Ninit Nis'107 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| COLON't => Shift_act Nis'108 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'108 => 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 _)
| SND't => Shift_act Nis'9 (eq_refl _)
| SIGMA't => Shift_act Nis'11 (eq_refl _)
| REFL't => Shift_act Nis'12 (eq_refl _)
| REC't => Shift_act Nis'16 (eq_refl _)
| PI't => Shift_act Nis'17 (eq_refl _)
| NAT't => Shift_act Nis'7 (eq_refl _)
| LPAREN't => Shift_act Nis'8 (eq_refl _)
| LET't => Shift_act Nis'18 (eq_refl _)
| LANGLE't => Shift_act Nis'10 (eq_refl _)
| LAMBDA't => Shift_act Nis'23 (eq_refl _)
| INT't => Shift_act Nis'13 (eq_refl _)
| FST't => Shift_act Nis'24 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'109 => Lookahead_act (fun terminal:terminal =>
match terminal return lookahead_action terminal with
| EOF't => Shift_act Nis'110 (eq_refl _)
| _ => Fail_act
end)
| Ninit Nis'110 => 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'107 (eq_refl _))
| Init Init'0, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Init Init'0, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Init Init'0, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Init Init'0, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'6, atomic_obj'nt => Some (exist _ Nis'105 (eq_refl _))
| Ninit Nis'8, obj'nt => Some (exist _ Nis'103 (eq_refl _))
| Ninit Nis'8, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'8, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'8, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'8, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'9, atomic_obj'nt => Some (exist _ Nis'102 (eq_refl _))
| Ninit Nis'10, obj'nt => Some (exist _ Nis'92 (eq_refl _))
| Ninit Nis'10, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'10, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'10, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'10, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'12, atomic_obj'nt => Some (exist _ Nis'14 (eq_refl _))
| Ninit Nis'14, atomic_obj'nt => Some (exist _ Nis'15 (eq_refl _))
| Ninit Nis'16, obj'nt => Some (exist _ Nis'52 (eq_refl _))
| Ninit Nis'16, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'16, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'16, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'16, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'18, let_defns'nt => Some (exist _ Nis'47 (eq_refl _))
| Ninit Nis'18, let_defn'nt => Some (exist _ Nis'51 (eq_refl _))
| Ninit Nis'19, param'nt => Some (exist _ Nis'43 (eq_refl _))
| Ninit Nis'22, obj'nt => Some (exist _ Nis'26 (eq_refl _))
| Ninit Nis'22, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'22, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'22, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'22, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'24, atomic_obj'nt => Some (exist _ Nis'25 (eq_refl _))
| Ninit Nis'28, params'nt => Some (exist _ Nis'29 (eq_refl _))
| Ninit Nis'28, param'nt => Some (exist _ Nis'42 (eq_refl _))
| Ninit Nis'29, param'nt => Some (exist _ Nis'41 (eq_refl _))
| Ninit Nis'30, obj'nt => Some (exist _ Nis'31 (eq_refl _))
| Ninit Nis'30, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'30, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'30, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'30, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'34, atomic_obj'nt => Some (exist _ Nis'40 (eq_refl _))
| Ninit Nis'36, obj'nt => Some (exist _ Nis'37 (eq_refl _))
| Ninit Nis'36, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'36, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'36, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'36, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'38, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'38, app_obj'nt => Some (exist _ Nis'39 (eq_refl _))
| Ninit Nis'39, atomic_obj'nt => Some (exist _ Nis'40 (eq_refl _))
| Ninit Nis'44, obj'nt => Some (exist _ Nis'45 (eq_refl _))
| Ninit Nis'44, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'44, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'44, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'44, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'47, let_defn'nt => Some (exist _ Nis'50 (eq_refl _))
| Ninit Nis'48, obj'nt => Some (exist _ Nis'49 (eq_refl _))
| Ninit Nis'48, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'48, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'48, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'48, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'52, optional_as_nat'nt => Some (exist _ Nis'75 (eq_refl _))
| Ninit Nis'55, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'55, app_obj'nt => Some (exist _ Nis'56 (eq_refl _))
| Ninit Nis'56, atomic_obj'nt => Some (exist _ Nis'40 (eq_refl _))
| Ninit Nis'58, obj'nt => Some (exist _ Nis'59 (eq_refl _))
| Ninit Nis'58, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'58, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'58, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'58, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'60, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'60, app_obj'nt => Some (exist _ Nis'61 (eq_refl _))
| Ninit Nis'61, atomic_obj'nt => Some (exist _ Nis'40 (eq_refl _))
| Ninit Nis'67, obj'nt => Some (exist _ Nis'68 (eq_refl _))
| Ninit Nis'67, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'67, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'67, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'67, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'72, obj'nt => Some (exist _ Nis'73 (eq_refl _))
| Ninit Nis'72, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'72, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'72, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'72, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'78, obj'nt => Some (exist _ Nis'79 (eq_refl _))
| Ninit Nis'78, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'78, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'78, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'78, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'82, obj'nt => Some (exist _ Nis'83 (eq_refl _))
| Ninit Nis'82, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'82, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'82, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'82, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'89, obj'nt => Some (exist _ Nis'90 (eq_refl _))
| Ninit Nis'89, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'89, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'89, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'89, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'93, obj'nt => Some (exist _ Nis'94 (eq_refl _))
| Ninit Nis'93, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'93, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'93, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'93, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'95, obj'nt => Some (exist _ Nis'96 (eq_refl _))
| Ninit Nis'95, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'95, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'95, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'95, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'99, obj'nt => Some (exist _ Nis'100 (eq_refl _))
| Ninit Nis'99, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'99, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'99, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'99, app_obj'nt => Some (exist _ Nis'34 (eq_refl _))
| Ninit Nis'108, obj'nt => Some (exist _ Nis'109 (eq_refl _))
| Ninit Nis'108, fnbinder'nt => Some (exist _ Nis'28 (eq_refl _))
| Ninit Nis'108, eq_obj'nt => Some (exist _ Nis'32 (eq_refl _))
| Ninit Nis'108, atomic_obj'nt => Some (exist _ Nis'33 (eq_refl _))
| Ninit Nis'108, app_obj'nt => Some (exist _ Nis'34 (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 => []%list
| Nis'12 => []%list
| Nis'13 => []%list
| Nis'14 => [T REFL't]%list
| Nis'15 => [NT atomic_obj'nt; T REFL't]%list
| Nis'16 => []%list
| Nis'17 => []%list
| Nis'18 => []%list
| Nis'19 => []%list
| Nis'20 => []%list
| Nis'21 => [T LPAREN't]%list
| Nis'22 => [T VAR't; T LPAREN't]%list
| Nis'23 => []%list
| Nis'24 => []%list
| Nis'25 => [T FST't]%list
| Nis'26 => [T COLON't; T VAR't; T LPAREN't]%list
| Nis'27 => [NT obj'nt; T COLON't; T VAR't; T LPAREN't]%list
| Nis'28 => []%list
| Nis'29 => [NT fnbinder'nt]%list
| Nis'30 => [NT params'nt; NT fnbinder'nt]%list
| Nis'31 => [T ARROW't; NT params'nt; NT fnbinder'nt]%list
| Nis'32 => []%list
| Nis'33 => []%list
| Nis'34 => []%list
| Nis'35 => [NT app_obj'nt]%list
| Nis'36 => [T EQ't; NT app_obj'nt]%list
| Nis'37 => [T LCURLY't; T EQ't; NT app_obj'nt]%list
| Nis'38 => [NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt]%list
| Nis'39 => [T RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt]%list
| Nis'40 => [NT app_obj'nt]%list
| Nis'41 => [NT params'nt]%list
| Nis'42 => []%list
| Nis'43 => [T LPAREN't]%list
| Nis'44 => [NT param'nt; T LPAREN't]%list
| Nis'45 => [T DEF't; NT param'nt; T LPAREN't]%list
| Nis'46 => [NT obj'nt; T DEF't; NT param'nt; T LPAREN't]%list
| Nis'47 => [T LET't]%list
| Nis'48 => [NT let_defns'nt; T LET't]%list
| Nis'49 => [T IN't; NT let_defns'nt; T LET't]%list
| Nis'50 => [NT let_defns'nt]%list
| Nis'51 => []%list
| Nis'52 => [T REC't]%list
| Nis'53 => [NT obj'nt; T REC't]%list
| Nis'54 => [T AS't]%list
| Nis'55 => [T AS't; NT obj'nt; T REC't]%list
| Nis'56 => [T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'57 => [NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'58 => [T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'59 => [T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'60 => [NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'61 => [T RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'62 => [NT app_obj'nt; T RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'63 => [T RPAREN't; NT app_obj'nt; T RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'64 => [T RETURN't; T RPAREN't; NT app_obj'nt; T RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'65 => [T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'66 => [T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RCURLY't; NT obj'nt; T LCURLY'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 VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'68 => [T DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RCURLY't; NT obj'nt; T LCURLY'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 DOT't; T VAR't; T VAR't; T VAR't; T RETURN't; T RPAREN't; NT app_obj'nt; T RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'70 => [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 RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'71 => [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 RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'72 => [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 RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'73 => [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 RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'74 => [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 RCURLY't; NT obj'nt; T LCURLY't; T EQ't; NT app_obj'nt; T LPAREN't; T AS't; NT obj'nt; T REC't]%list
| Nis'75 => [NT obj'nt; T REC't]%list
| Nis'76 => [NT optional_as_nat'nt; NT obj'nt; T REC't]%list
| Nis'77 => [T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
| Nis'78 => [T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
| Nis'79 => [T DOT't; T VAR't; T RETURN't; NT optional_as_nat'nt; NT obj'nt; T REC't]%list
| Nis'80 => [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 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 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 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 => [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 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 => [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 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'88 => [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'89 => [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'90 => [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'91 => [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'92 => [T LANGLE't]%list
| Nis'93 => [NT obj'nt; T LANGLE't]%list
| Nis'94 => [T COLON't; NT obj'nt; T LANGLE't]%list
| Nis'95 => [NT obj'nt; T COLON't; NT obj'nt; T LANGLE't]%list
| Nis'96 => [T COMMA't; NT obj'nt; T COLON't; NT obj'nt; T LANGLE't]%list
| Nis'97 => [NT obj'nt; T COMMA't; NT obj'nt; T COLON't; NT obj'nt; T LANGLE't]%list
| Nis'98 => [T COLON't; NT obj'nt; T COMMA't; NT obj'nt; T COLON't; NT obj'nt; T LANGLE't]%list
| Nis'99 => [T VAR't; T COLON't; NT obj'nt; T COMMA't; NT obj'nt; T COLON't; NT obj'nt; T LANGLE't]%list
| Nis'100 => [T DOT't; T VAR't; T COLON't; NT obj'nt; T COMMA't; NT obj'nt; T COLON't; NT obj'nt; T LANGLE't]%list
| Nis'101 => [NT obj'nt; T DOT't; T VAR't; T COLON't; NT obj'nt; T COMMA't; NT obj'nt; T COLON't; NT obj'nt; T LANGLE't]%list
| Nis'102 => [T SND't]%list
| Nis'103 => [T LPAREN't]%list
| Nis'104 => [NT obj'nt; T LPAREN't]%list
| Nis'105 => [T SUCC't]%list
| Nis'107 => []%list
| Nis'108 => [NT obj'nt]%list
| Nis'109 => [T COLON't; NT obj'nt]%list
| Nis'110 => [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'10 | Ninit Nis'12 | Ninit Nis'14 | Ninit Nis'16 | Ninit Nis'22 | Ninit Nis'24 | Ninit Nis'30 | Ninit Nis'34 | Ninit Nis'36 | Ninit Nis'38 | Ninit Nis'39 | Ninit Nis'44 | Ninit Nis'48 | Ninit Nis'55 | Ninit Nis'56 | Ninit Nis'58 | Ninit Nis'60 | Ninit Nis'61 | Ninit Nis'67 | Ninit Nis'72 | Ninit Nis'78 | Ninit Nis'82 | Ninit Nis'89 | Ninit Nis'93 | Ninit Nis'95 | Ninit Nis'99 | Ninit Nis'108 => 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'10 | Ninit Nis'16 | Ninit Nis'22 | Ninit Nis'30 | Ninit Nis'36 | Ninit Nis'44 | Ninit Nis'48 | Ninit Nis'58 | Ninit Nis'67 | Ninit Nis'72 | Ninit Nis'78 | Ninit Nis'82 | Ninit Nis'89 | Ninit Nis'93 | Ninit Nis'95 | Ninit Nis'99 | Ninit Nis'108 => true
| _ => false
end.
Extract Inlined Constant state_set_4 => "assert false".
Definition state_set_5 (s:state) : bool :=
match s with
| Ninit Nis'12 => true
| _ => false
end.
Extract Inlined Constant state_set_5 => "assert false".
Definition state_set_6 (s:state) : bool :=
match s with
| Ninit Nis'14 => true
| _ => false
end.
Extract Inlined Constant state_set_6 => "assert false".
Definition state_set_7 (s:state) : bool :=
match s with
| Ninit Nis'18 | Ninit Nis'47 => true
| _ => false
end.
Extract Inlined Constant state_set_7 => "assert false".
Definition state_set_8 (s:state) : bool :=
match s with
| Ninit Nis'19 | Ninit Nis'28 | Ninit Nis'29 => true
| _ => false
end.
Extract Inlined Constant state_set_8 => "assert false".
Definition state_set_9 (s:state) : bool :=
match s with
| Ninit Nis'20 => true
| _ => false
end.
Extract Inlined Constant state_set_9 => "assert false".
Definition state_set_10 (s:state) : bool :=
match s with
| Ninit Nis'21 => true
| _ => false
end.
Extract Inlined Constant state_set_10 => "assert false".
Definition state_set_11 (s:state) : bool :=
match s with
| Ninit Nis'24 => true
| _ => false
end.
Extract Inlined Constant state_set_11 => "assert false".
Definition state_set_12 (s:state) : bool :=
match s with
| Ninit Nis'22 => true
| _ => false
end.
Extract Inlined Constant state_set_12 => "assert false".
Definition state_set_13 (s:state) : bool :=
match s with
| Ninit Nis'26 => true
| _ => false
end.
Extract Inlined Constant state_set_13 => "assert false".
Definition state_set_14 (s:state) : bool :=
match s with
| Ninit Nis'28 => true
| _ => false
end.
Extract Inlined Constant state_set_14 => "assert false".
Definition state_set_15 (s:state) : bool :=
match s with
| Ninit Nis'29 => true
| _ => false
end.
Extract Inlined Constant state_set_15 => "assert false".
Definition state_set_16 (s:state) : bool :=
match s with
| Ninit Nis'30 => true
| _ => false
end.
Extract Inlined Constant state_set_16 => "assert false".
Definition state_set_17 (s:state) : bool :=
match s with
| Init Init'0 | Ninit Nis'8 | Ninit Nis'10 | Ninit Nis'16 | Ninit Nis'22 | Ninit Nis'30 | Ninit Nis'36 | Ninit Nis'38 | Ninit Nis'44 | Ninit Nis'48 | Ninit Nis'55 | Ninit Nis'58 | Ninit Nis'60 | Ninit Nis'67 | Ninit Nis'72 | Ninit Nis'78 | Ninit Nis'82 | Ninit Nis'89 | Ninit Nis'93 | Ninit Nis'95 | Ninit Nis'99 | Ninit Nis'108 => true
| _ => false
end.
Extract Inlined Constant state_set_17 => "assert false".
Definition state_set_18 (s:state) : bool :=
match s with
| Ninit Nis'34 => true
| _ => false
end.
Extract Inlined Constant state_set_18 => "assert false".
Definition state_set_19 (s:state) : bool :=
match s with
| Ninit Nis'35 => true
| _ => false
end.
Extract Inlined Constant state_set_19 => "assert false".
Definition state_set_20 (s:state) : bool :=
match s with
| Ninit Nis'36 => true
| _ => false
end.
Extract Inlined Constant state_set_20 => "assert false".
Definition state_set_21 (s:state) : bool :=
match s with
| Ninit Nis'37 => true
| _ => false
end.
Extract Inlined Constant state_set_21 => "assert false".
Definition state_set_22 (s:state) : bool :=
match s with
| Ninit Nis'38 => true
| _ => false
end.
Extract Inlined Constant state_set_22 => "assert false".
Definition state_set_23 (s:state) : bool :=
match s with
| Ninit Nis'34 | Ninit Nis'39 | Ninit Nis'56 | Ninit Nis'61 => true
| _ => false
end.
Extract Inlined Constant state_set_23 => "assert false".
Definition state_set_24 (s:state) : bool :=
match s with
| Ninit Nis'19 => true
| _ => false
end.
Extract Inlined Constant state_set_24 => "assert false".
Definition state_set_25 (s:state) : bool :=
match s with
| Ninit Nis'43 => true
| _ => false
end.
Extract Inlined Constant state_set_25 => "assert false".
Definition state_set_26 (s:state) : bool :=
match s with
| Ninit Nis'44 => true
| _ => false
end.
Extract Inlined Constant state_set_26 => "assert false".
Definition state_set_27 (s:state) : bool :=
match s with
| Ninit Nis'45 => true
| _ => false
end.
Extract Inlined Constant state_set_27 => "assert false".
Definition state_set_28 (s:state) : bool :=
match s with
| Ninit Nis'18 => true
| _ => false
end.
Extract Inlined Constant state_set_28 => "assert false".
Definition state_set_29 (s:state) : bool :=
match s with
| Ninit Nis'47 => true
| _ => false
end.
Extract Inlined Constant state_set_29 => "assert false".
Definition state_set_30 (s:state) : bool :=
match s with
| Ninit Nis'48 => true
| _ => false
end.
Extract Inlined Constant state_set_30 => "assert false".
Definition state_set_31 (s:state) : bool :=
match s with
| Ninit Nis'16 => true
| _ => false
end.
Extract Inlined Constant state_set_31 => "assert false".
Definition state_set_32 (s:state) : bool :=
match s with
| Ninit Nis'52 => true
| _ => false
end.
Extract Inlined Constant state_set_32 => "assert false".
Definition state_set_33 (s:state) : bool :=
match s with
| Ninit Nis'53 => true
| _ => false
end.
Extract Inlined Constant state_set_33 => "assert false".
Definition state_set_34 (s:state) : bool :=
match s with
| Ninit Nis'55 => true
| _ => false
end.
Extract Inlined Constant state_set_34 => "assert false".
Definition state_set_35 (s:state) : bool :=
match s with
| Ninit Nis'56 => true
| _ => false
end.
Extract Inlined Constant state_set_35 => "assert false".
Definition state_set_36 (s:state) : bool :=
match s with
| Ninit Nis'57 => true
| _ => false
end.
Extract Inlined Constant state_set_36 => "assert false".
Definition state_set_37 (s:state) : bool :=
match s with
| Ninit Nis'58 => true
| _ => false
end.
Extract Inlined Constant state_set_37 => "assert false".
Definition state_set_38 (s:state) : bool :=
match s with
| Ninit Nis'59 => true
| _ => false
end.
Extract Inlined Constant state_set_38 => "assert false".
Definition state_set_39 (s:state) : bool :=
match s with
| Ninit Nis'60 => true
| _ => false
end.
Extract Inlined Constant state_set_39 => "assert false".
Definition state_set_40 (s:state) : bool :=
match s with
| Ninit Nis'61 => true
| _ => false
end.
Extract Inlined Constant state_set_40 => "assert false".
Definition state_set_41 (s:state) : bool :=
match s with
| Ninit Nis'62 => true
| _ => false
end.
Extract Inlined Constant state_set_41 => "assert false".
Definition state_set_42 (s:state) : bool :=
match s with
| Ninit Nis'63 => true
| _ => false
end.
Extract Inlined Constant state_set_42 => "assert false".
Definition state_set_43 (s:state) : bool :=
match s with
| Ninit Nis'64 => true
| _ => false
end.
Extract Inlined Constant state_set_43 => "assert false".
Definition state_set_44 (s:state) : bool :=
match s with
| Ninit Nis'65 => true
| _ => false
end.
Extract Inlined Constant state_set_44 => "assert false".
Definition state_set_45 (s:state) : bool :=
match s with
| Ninit Nis'66 => true
| _ => false
end.
Extract Inlined Constant state_set_45 => "assert false".
Definition state_set_46 (s:state) : bool :=
match s with
| Ninit Nis'67 => true
| _ => false
end.
Extract Inlined Constant state_set_46 => "assert false".
Definition state_set_47 (s:state) : bool :=
match s with
| Ninit Nis'68 => true
| _ => false
end.
Extract Inlined Constant state_set_47 => "assert false".
Definition state_set_48 (s:state) : bool :=
match s with
| Ninit Nis'69 => true
| _ => false
end.
Extract Inlined Constant state_set_48 => "assert false".
Definition state_set_49 (s:state) : bool :=
match s with
| Ninit Nis'70 => true
| _ => false
end.
Extract Inlined Constant state_set_49 => "assert false".
Definition state_set_50 (s:state) : bool :=
match s with
| Ninit Nis'71 => true
| _ => false
end.
Extract Inlined Constant state_set_50 => "assert false".
Definition state_set_51 (s:state) : bool :=
match s with
| Ninit Nis'72 => true
| _ => false
end.
Extract Inlined Constant state_set_51 => "assert false".
Definition state_set_52 (s:state) : bool :=
match s with
| Ninit Nis'73 => true
| _ => false
end.
Extract Inlined Constant state_set_52 => "assert false".
Definition state_set_53 (s:state) : bool :=
match s with
| Ninit Nis'75 => true
| _ => false
end.
Extract Inlined Constant state_set_53 => "assert false".
Definition state_set_54 (s:state) : bool :=
match s with
| Ninit Nis'76 => true
| _ => false
end.
Extract Inlined Constant state_set_54 => "assert false".
Definition state_set_55 (s:state) : bool :=
match s with
| Ninit Nis'77 => true
| _ => false
end.
Extract Inlined Constant state_set_55 => "assert false".
Definition state_set_56 (s:state) : bool :=
match s with
| Ninit Nis'78 => true
| _ => false
end.
Extract Inlined Constant state_set_56 => "assert false".
Definition state_set_57 (s:state) : bool :=
match s with
| Ninit Nis'79 => true
| _ => false
end.
Extract Inlined Constant state_set_57 => "assert false".
Definition state_set_58 (s:state) : bool :=
match s with
| Ninit Nis'80 => true
| _ => false
end.
Extract Inlined Constant state_set_58 => "assert false".
Definition state_set_59 (s:state) : bool :=
match s with
| Ninit Nis'81 => true
| _ => false
end.
Extract Inlined Constant state_set_59 => "assert false".
Definition state_set_60 (s:state) : bool :=
match s with
| Ninit Nis'82 => true
| _ => false
end.
Extract Inlined Constant state_set_60 => "assert false".
Definition state_set_61 (s:state) : bool :=
match s with
| Ninit Nis'83 => true
| _ => false
end.
Extract Inlined Constant state_set_61 => "assert false".
Definition state_set_62 (s:state) : bool :=
match s with
| Ninit Nis'84 => true
| _ => false
end.
Extract Inlined Constant state_set_62 => "assert false".
Definition state_set_63 (s:state) : bool :=
match s with
| Ninit Nis'85 => true
| _ => false
end.
Extract Inlined Constant state_set_63 => "assert false".
Definition state_set_64 (s:state) : bool :=
match s with
| Ninit Nis'86 => true
| _ => false
end.
Extract Inlined Constant state_set_64 => "assert false".
Definition state_set_65 (s:state) : bool :=
match s with
| Ninit Nis'87 => true
| _ => false
end.
Extract Inlined Constant state_set_65 => "assert false".
Definition state_set_66 (s:state) : bool :=
match s with
| Ninit Nis'88 => true
| _ => false
end.
Extract Inlined Constant state_set_66 => "assert false".
Definition state_set_67 (s:state) : bool :=
match s with
| Ninit Nis'89 => true
| _ => false
end.
Extract Inlined Constant state_set_67 => "assert false".
Definition state_set_68 (s:state) : bool :=
match s with
| Ninit Nis'90 => true
| _ => false
end.
Extract Inlined Constant state_set_68 => "assert false".
Definition state_set_69 (s:state) : bool :=
match s with
| Ninit Nis'10 => true
| _ => false
end.
Extract Inlined Constant state_set_69 => "assert false".
Definition state_set_70 (s:state) : bool :=
match s with
| Ninit Nis'92 => true
| _ => false
end.
Extract Inlined Constant state_set_70 => "assert false".
Definition state_set_71 (s:state) : bool :=
match s with
| Ninit Nis'93 => true
| _ => false
end.
Extract Inlined Constant state_set_71 => "assert false".
Definition state_set_72 (s:state) : bool :=
match s with
| Ninit Nis'94 => true
| _ => false
end.
Extract Inlined Constant state_set_72 => "assert false".
Definition state_set_73 (s:state) : bool :=
match s with
| Ninit Nis'95 => true
| _ => false
end.
Extract Inlined Constant state_set_73 => "assert false".
Definition state_set_74 (s:state) : bool :=
match s with
| Ninit Nis'96 => true
| _ => false
end.
Extract Inlined Constant state_set_74 => "assert false".
Definition state_set_75 (s:state) : bool :=
match s with
| Ninit Nis'97 => true
| _ => false
end.
Extract Inlined Constant state_set_75 => "assert false".
Definition state_set_76 (s:state) : bool :=
match s with
| Ninit Nis'98 => true
| _ => false
end.
Extract Inlined Constant state_set_76 => "assert false".
Definition state_set_77 (s:state) : bool :=
match s with
| Ninit Nis'99 => true
| _ => false
end.
Extract Inlined Constant state_set_77 => "assert false".
Definition state_set_78 (s:state) : bool :=
match s with
| Ninit Nis'100 => true
| _ => false
end.
Extract Inlined Constant state_set_78 => "assert false".
Definition state_set_79 (s:state) : bool :=
match s with
| Ninit Nis'9 => true
| _ => false
end.
Extract Inlined Constant state_set_79 => "assert false".
Definition state_set_80 (s:state) : bool :=
match s with
| Ninit Nis'8 => true
| _ => false
end.
Extract Inlined Constant state_set_80 => "assert false".
Definition state_set_81 (s:state) : bool :=
match s with
| Ninit Nis'103 => true
| _ => false
end.
Extract Inlined Constant state_set_81 => "assert false".
Definition state_set_82 (s:state) : bool :=
match s with
| Ninit Nis'6 => true
| _ => false
end.
Extract Inlined Constant state_set_82 => "assert false".
Definition state_set_83 (s:state) : bool :=
match s with
| Init Init'0 => true
| _ => false
end.
Extract Inlined Constant state_set_83 => "assert false".
Definition state_set_84 (s:state) : bool :=
match s with
| Ninit Nis'107 => true
| _ => false
end.
Extract Inlined Constant state_set_84 => "assert false".
Definition state_set_85 (s:state) : bool :=
match s with
| Ninit Nis'108 => true
| _ => false
end.
Extract Inlined Constant state_set_85 => "assert false".
Definition state_set_86 (s:state) : bool :=
match s with
| Ninit Nis'109 => true
| _ => false
end.
Extract Inlined Constant state_set_86 => "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_4]%list
| Nis'12 => [state_set_4]%list
| Nis'13 => [state_set_1]%list
| Nis'14 => [state_set_5; state_set_4]%list
| Nis'15 => [state_set_6; state_set_5; state_set_4]%list
| Nis'16 => [state_set_4]%list
| Nis'17 => [state_set_4]%list
| Nis'18 => [state_set_4]%list
| Nis'19 => [state_set_7]%list
| Nis'20 => [state_set_8]%list
| Nis'21 => [state_set_9; state_set_8]%list
| Nis'22 => [state_set_10; state_set_9; state_set_8]%list
| Nis'23 => [state_set_4]%list
| Nis'24 => [state_set_4]%list
| Nis'25 => [state_set_11; state_set_4]%list
| Nis'26 => [state_set_12; state_set_10; state_set_9; state_set_8]%list
| Nis'27 => [state_set_13; state_set_12; state_set_10; state_set_9; state_set_8]%list
| Nis'28 => [state_set_4]%list
| Nis'29 => [state_set_14; state_set_4]%list
| Nis'30 => [state_set_15; state_set_14; state_set_4]%list
| Nis'31 => [state_set_16; state_set_15; state_set_14; state_set_4]%list
| Nis'32 => [state_set_4]%list
| Nis'33 => [state_set_17]%list
| Nis'34 => [state_set_4]%list
| Nis'35 => [state_set_18; state_set_4]%list
| Nis'36 => [state_set_19; state_set_18; state_set_4]%list
| Nis'37 => [state_set_20; state_set_19; state_set_18; state_set_4]%list
| Nis'38 => [state_set_21; state_set_20; state_set_19; state_set_18; state_set_4]%list
| Nis'39 => [state_set_22; state_set_21; state_set_20; state_set_19; state_set_18; state_set_4]%list
| Nis'40 => [state_set_23; state_set_17]%list
| Nis'41 => [state_set_15; state_set_14]%list
| Nis'42 => [state_set_14]%list
| Nis'43 => [state_set_24; state_set_7]%list
| Nis'44 => [state_set_25; state_set_24; state_set_7]%list
| Nis'45 => [state_set_26; state_set_25; state_set_24; state_set_7]%list
| Nis'46 => [state_set_27; state_set_26; state_set_25; state_set_24; state_set_7]%list
| Nis'47 => [state_set_28; state_set_4]%list
| Nis'48 => [state_set_29; state_set_28; state_set_4]%list
| Nis'49 => [state_set_30; state_set_29; state_set_28; state_set_4]%list
| Nis'50 => [state_set_29; state_set_28]%list
| Nis'51 => [state_set_28]%list
| Nis'52 => [state_set_31; state_set_4]%list
| Nis'53 => [state_set_32; state_set_31; state_set_4]%list
| Nis'54 => [state_set_33; state_set_32]%list
| Nis'55 => [state_set_33; state_set_32; state_set_31; state_set_4]%list
| Nis'56 => [state_set_34; state_set_33; state_set_32; state_set_31; state_set_4]%list
| Nis'57 => [state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_4]%list
| Nis'58 => [state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_4]%list
| Nis'59 => [state_set_37; state_set_36; state_set_35; state_set_34; state_set_33; state_set_32; state_set_31; state_set_4]%list
| Nis'60 => [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_4]%list
| Nis'61 => [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_4]%list
| Nis'62 => [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_4]%list
| Nis'63 => [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_4]%list
| Nis'64 => [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_4]%list
| Nis'65 => [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_4]%list
| Nis'66 => [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_4]%list
| Nis'67 => [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_4]%list
| Nis'68 => [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_4]%list
| Nis'69 => [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_4]%list
| Nis'70 => [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_4]%list
| Nis'71 => [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_4]%list
| Nis'72 => [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_4]%list
| Nis'73 => [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_4]%list
| Nis'74 => [state_set_52; 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_4]%list
| Nis'75 => [state_set_32; state_set_31; state_set_4]%list
| Nis'76 => [state_set_53; state_set_32; state_set_31; state_set_4]%list
| Nis'77 => [state_set_54; state_set_53; state_set_32; state_set_31; state_set_4]%list
| Nis'78 => [state_set_55; state_set_54; state_set_53; state_set_32; state_set_31; state_set_4]%list
| Nis'79 => [state_set_56; state_set_55; state_set_54; state_set_53; state_set_32; state_set_31; state_set_4]%list
| Nis'80 => [state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_32; state_set_31; state_set_4]%list
| Nis'81 => [state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_32; state_set_31; state_set_4]%list
| Nis'82 => [state_set_59; state_set_58; state_set_57; state_set_56; state_set_55; state_set_54; state_set_53; state_set_32; state_set_31; state_set_4]%list
| Nis'83 => [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_32; state_set_31; state_set_4]%list
| Nis'84 => [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_32; state_set_31; state_set_4]%list
| Nis'85 => [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_32; state_set_31; state_set_4]%list
| Nis'86 => [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_32; state_set_31; state_set_4]%list
| Nis'87 => [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_32; state_set_31; state_set_4]%list
| Nis'88 => [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_32; state_set_31; state_set_4]%list
| Nis'89 => [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_32; state_set_31; state_set_4]%list
| Nis'90 => [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_32; state_set_31; state_set_4]%list
| Nis'91 => [state_set_68; 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_32; state_set_31; state_set_4]%list
| Nis'92 => [state_set_69; state_set_1]%list
| Nis'93 => [state_set_70; state_set_69; state_set_1]%list
| Nis'94 => [state_set_71; state_set_70; state_set_69; state_set_1]%list
| Nis'95 => [state_set_72; state_set_71; state_set_70; state_set_69; state_set_1]%list
| Nis'96 => [state_set_73; state_set_72; state_set_71; state_set_70; state_set_69; state_set_1]%list
| Nis'97 => [state_set_74; state_set_73; state_set_72; state_set_71; state_set_70; state_set_69; state_set_1]%list
| Nis'98 => [state_set_75; state_set_74; state_set_73; state_set_72; state_set_71; state_set_70; state_set_69; state_set_1]%list
| Nis'99 => [state_set_76; state_set_75; state_set_74; state_set_73; state_set_72; state_set_71; state_set_70; state_set_69; state_set_1]%list
| Nis'100 => [state_set_77; state_set_76; state_set_75; state_set_74; state_set_73; state_set_72; state_set_71; state_set_70; state_set_69; state_set_1]%list
| Nis'101 => [state_set_78; state_set_77; state_set_76; state_set_75; state_set_74; state_set_73; state_set_72; state_set_71; state_set_70; state_set_69; state_set_1]%list
| Nis'102 => [state_set_79; state_set_4]%list
| Nis'103 => [state_set_80; state_set_1]%list
| Nis'104 => [state_set_81; state_set_80; state_set_1]%list
| Nis'105 => [state_set_82; state_set_4]%list
| Nis'107 => [state_set_83]%list
| Nis'108 => [state_set_84; state_set_83]%list
| Nis'109 => [state_set_85; state_set_84; state_set_83]%list
| Nis'110 => [state_set_86; state_set_85; state_set_84; state_set_83]%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; LANGLE'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; SND't; SIGMA't; RPAREN't; RETURN't; REFL't; REC't; RCURLY't; RANGLE't; PI't; NAT't; LPAREN't; LET't; LCURLY't; LANGLE't; LAMBDA't; INT't; IN't; FST'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; RCURLY't; RANGLE't; NAT't; LPAREN't; LANGLE't; INT't; EQ't; EOF't; END't; COMMA'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; RCURLY't; RANGLE't; EOF't; END't; COMMA'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; LANGLE'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; LANGLE'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; LANGLE'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; RCURLY't; NAT't; LPAREN't; LANGLE't; INT't; EQ't]%list.
Extract Inlined Constant lookahead_set_16 => "assert false".
Definition lookahead_set_17 : list terminal :=
[RCURLY'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; RCURLY't; RANGLE't; NAT't; LPAREN't; LANGLE't; INT't; EOF't; END't; COMMA'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; LANGLE'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; LANGLE'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; LANGLE'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; LANGLE'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; LANGLE't; INT't; EQ't; COMMA't]%list.
Extract Inlined Constant lookahead_set_26 => "assert false".
Definition lookahead_set_27 : list terminal :=
[COMMA't]%list.
Extract Inlined Constant lookahead_set_27 => "assert false".
Definition lookahead_set_28 : list terminal :=
[ZERO't; VAR't; TYPE't; RANGLE't; NAT't; LPAREN't; LANGLE't; INT't; EQ't]%list.
Extract Inlined Constant lookahead_set_28 => "assert false".
Definition lookahead_set_29 : list terminal :=
[RANGLE't]%list.
Extract Inlined Constant lookahead_set_29 => "assert false".
Definition lookahead_set_30 : list terminal :=
[ZERO't; VAR't; TYPE't; NAT't; LPAREN't; LANGLE't; INT't; EQ't; EOF't]%list.
Extract Inlined Constant lookahead_set_30 => "assert false".
Definition lookahead_set_31 : list terminal :=
[EOF't]%list.
Extract Inlined Constant lookahead_set_31 => "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'atomic_obj'6; 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'fnbinder'2; 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'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
{| prod_item := Prod'obj'8; 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'atomic_obj'6; 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'6; dot_pos_item := 0; lookaheads_item := lookahead_set_7 |};
{| prod_item := Prod'atomic_obj'6; 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'fnbinder'2; 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'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
{| prod_item := Prod'obj'8; 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_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'atomic_obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
{| prod_item := Prod'obj'7; 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'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'atomic_obj'5; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |};
{| prod_item := Prod'atomic_obj'6; 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'fnbinder'2; 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'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |} ]%list.
Extract Inlined Constant items_of_state_10 => "assert false".
Definition items_of_state_11 : list item :=
[ {| prod_item := Prod'fnbinder'2; dot_pos_item := 1; lookaheads_item := lookahead_set_3 |} ]%list.
Extract Inlined Constant items_of_state_11 => "assert false".
Definition items_of_state_12 : 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'atomic_obj'6; 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_12 => "assert false".
Definition items_of_state_13 : list item :=
[ {| prod_item := Prod'atomic_obj'3; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_13 => "assert false".
Definition items_of_state_14 : 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'atomic_obj'6; 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_14 => "assert false".
Definition items_of_state_15 : list item :=
[ {| prod_item := Prod'obj'4; dot_pos_item := 3; 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'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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_11 |} ]%list.
Extract Inlined Constant items_of_state_16 => "assert false".
Definition items_of_state_17 : list item :=
[ {| prod_item := Prod'fnbinder'0; dot_pos_item := 1; lookaheads_item := lookahead_set_3 |} ]%list.
Extract Inlined Constant items_of_state_17 => "assert false".
Definition items_of_state_18 : 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'8; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_18 => "assert false".
Definition items_of_state_19 : 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_19 => "assert false".
Definition items_of_state_20 : list item :=
[ {| prod_item := Prod'param'0; dot_pos_item := 1; lookaheads_item := lookahead_set_14 |} ]%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 := 2; 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'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'6; 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'fnbinder'2; 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'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
{| prod_item := Prod'obj'8; 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_22 => "assert false".
Definition items_of_state_23 : list item :=
[ {| prod_item := Prod'fnbinder'1; dot_pos_item := 1; lookaheads_item := lookahead_set_3 |} ]%list.
Extract Inlined Constant items_of_state_23 => "assert false".
Definition items_of_state_24 : 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'atomic_obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
{| prod_item := Prod'obj'6; dot_pos_item := 1; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_24 => "assert false".
Definition items_of_state_25 : list item :=
[ {| prod_item := Prod'obj'6; dot_pos_item := 2; 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'param'0; dot_pos_item := 4; lookaheads_item := lookahead_set_14 |} ]%list.
Extract Inlined Constant items_of_state_26 => "assert false".
Definition items_of_state_27 : list item :=
[ {| prod_item := Prod'param'0; dot_pos_item := 5; lookaheads_item := lookahead_set_14 |} ]%list.
Extract Inlined Constant items_of_state_27 => "assert false".
Definition items_of_state_28 : 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_28 => "assert false".
Definition items_of_state_29 : 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_29 => "assert false".
Definition items_of_state_30 : 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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; 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'obj'0; dot_pos_item := 4; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_31 => "assert false".
Definition items_of_state_32 : list item :=
[ {| prod_item := Prod'obj'1; dot_pos_item := 1; 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'1; dot_pos_item := 1; lookaheads_item := lookahead_set_5 |} ]%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_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'atomic_obj'6; 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_34 => "assert false".
Definition items_of_state_35 : list item :=
[ {| prod_item := Prod'eq_obj'0; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_35 => "assert false".
Definition items_of_state_36 : 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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |} ]%list.
Extract Inlined Constant items_of_state_36 => "assert false".
Definition items_of_state_37 : list item :=
[ {| prod_item := Prod'eq_obj'0; dot_pos_item := 4; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_37 => "assert false".
Definition items_of_state_38 : 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'atomic_obj'6; 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_38 => "assert false".
Definition items_of_state_39 : 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'atomic_obj'6; 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_39 => "assert false".
Definition items_of_state_40 : list item :=
[ {| prod_item := Prod'app_obj'0; dot_pos_item := 2; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_40 => "assert false".
Definition items_of_state_41 : list item :=
[ {| prod_item := Prod'params'0; dot_pos_item := 2; lookaheads_item := lookahead_set_15 |} ]%list.
Extract Inlined Constant items_of_state_41 => "assert false".
Definition items_of_state_42 : list item :=
[ {| prod_item := Prod'params'1; dot_pos_item := 1; lookaheads_item := lookahead_set_15 |} ]%list.
Extract Inlined Constant items_of_state_42 => "assert false".
Definition items_of_state_43 : list item :=
[ {| prod_item := Prod'let_defn'0; dot_pos_item := 2; lookaheads_item := lookahead_set_12 |} ]%list.
Extract Inlined Constant items_of_state_43 => "assert false".
Definition items_of_state_44 : 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'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_8 |} ]%list.
Extract Inlined Constant items_of_state_44 => "assert false".
Definition items_of_state_45 : list item :=
[ {| prod_item := Prod'let_defn'0; dot_pos_item := 4; 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_defn'0; dot_pos_item := 5; 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'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'8; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_47 => "assert false".
Definition items_of_state_48 : 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'atomic_obj'6; 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'fnbinder'2; 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'7; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_6 |};
{| prod_item := Prod'obj'8; dot_pos_item := 3; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_48 => "assert false".
Definition items_of_state_49 : list item :=
[ {| prod_item := Prod'obj'8; dot_pos_item := 4; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_49 => "assert false".
Definition items_of_state_50 : list item :=
[ {| prod_item := Prod'let_defns'0; dot_pos_item := 2; lookaheads_item := lookahead_set_12 |} ]%list.
Extract Inlined Constant items_of_state_50 => "assert false".
Definition items_of_state_51 : list item :=
[ {| prod_item := Prod'let_defns'1; dot_pos_item := 1; lookaheads_item := lookahead_set_12 |} ]%list.
Extract Inlined Constant items_of_state_51 => "assert false".
Definition items_of_state_52 : 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_52 => "assert false".
Definition items_of_state_53 : 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_53 => "assert false".
Definition items_of_state_54 : 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_54 => "assert false".
Definition items_of_state_55 : 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'atomic_obj'6; 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_55 => "assert false".
Definition items_of_state_56 : 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'atomic_obj'6; 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_56 => "assert false".
Definition items_of_state_57 : list item :=
[ {| prod_item := Prod'obj'3; dot_pos_item := 6; 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'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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_17 |} ]%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 := 8; 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'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'atomic_obj'6; 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_60 => "assert false".
Definition items_of_state_61 : 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'atomic_obj'6; 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_61 => "assert false".
Definition items_of_state_62 : list item :=
[ {| prod_item := Prod'obj'3; dot_pos_item := 11; lookaheads_item := lookahead_set_6 |} ]%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 := 12; 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 := 13; 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 := 14; 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 := 15; 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_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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |} ]%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 := 17; 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 := 18; 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'3; dot_pos_item := 19; 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'3; dot_pos_item := 20; 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'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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |} ]%list.
Extract Inlined Constant items_of_state_72 => "assert false".
Definition items_of_state_73 : list item :=
[ {| prod_item := Prod'obj'3; dot_pos_item := 22; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_73 => "assert false".
Definition items_of_state_74 : list item :=
[ {| prod_item := Prod'obj'3; dot_pos_item := 23; 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 := 3; 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 := 4; 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'obj'2; dot_pos_item := 5; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_77 => "assert false".
Definition items_of_state_78 : 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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |} ]%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 := 7; 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 := 8; 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 := 9; 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'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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_23 |} ]%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 := 11; 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'obj'2; dot_pos_item := 12; lookaheads_item := lookahead_set_6 |} ]%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 := 13; 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 := 14; 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'obj'2; dot_pos_item := 15; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_87 => "assert false".
Definition items_of_state_88 : list item :=
[ {| prod_item := Prod'obj'2; dot_pos_item := 16; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_88 => "assert false".
Definition items_of_state_89 : 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'atomic_obj'6; 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'fnbinder'2; 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 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_25 |} ]%list.
Extract Inlined Constant items_of_state_89 => "assert false".
Definition items_of_state_90 : list item :=
[ {| prod_item := Prod'obj'2; dot_pos_item := 18; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_90 => "assert false".
Definition items_of_state_91 : list item :=
[ {| prod_item := Prod'obj'2; dot_pos_item := 19; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_91 => "assert false".
Definition items_of_state_92 : list item :=
[ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 2; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_92 => "assert false".
Definition items_of_state_93 : 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'atomic_obj'5; dot_pos_item := 3; lookaheads_item := lookahead_set_5 |};
{| prod_item := Prod'atomic_obj'6; 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'fnbinder'2; 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'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_27 |} ]%list.
Extract Inlined Constant items_of_state_93 => "assert false".
Definition items_of_state_94 : list item :=
[ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 4; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_94 => "assert false".
Definition items_of_state_95 : 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'atomic_obj'5; dot_pos_item := 5; lookaheads_item := lookahead_set_5 |};
{| prod_item := Prod'atomic_obj'6; 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'fnbinder'2; 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'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_2 |} ]%list.
Extract Inlined Constant items_of_state_95 => "assert false".
Definition items_of_state_96 : list item :=
[ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 6; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_96 => "assert false".
Definition items_of_state_97 : list item :=
[ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 7; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_97 => "assert false".
Definition items_of_state_98 : list item :=
[ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 8; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_98 => "assert false".
Definition items_of_state_99 : list item :=
[ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'atomic_obj'5; dot_pos_item := 9; lookaheads_item := lookahead_set_5 |};
{| prod_item := Prod'atomic_obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_28 |};
{| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| 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'fnbinder'2; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
{| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_29 |} ]%list.
Extract Inlined Constant items_of_state_99 => "assert false".
Definition items_of_state_100 : list item :=
[ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 10; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_100 => "assert false".
Definition items_of_state_101 : list item :=
[ {| prod_item := Prod'atomic_obj'5; dot_pos_item := 11; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_101 => "assert false".
Definition items_of_state_102 : list item :=
[ {| prod_item := Prod'obj'7; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_102 => "assert false".
Definition items_of_state_103 : list item :=
[ {| prod_item := Prod'atomic_obj'6; dot_pos_item := 2; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_103 => "assert false".
Definition items_of_state_104 : list item :=
[ {| prod_item := Prod'atomic_obj'6; dot_pos_item := 3; lookaheads_item := lookahead_set_5 |} ]%list.
Extract Inlined Constant items_of_state_104 => "assert false".
Definition items_of_state_105 : list item :=
[ {| prod_item := Prod'obj'5; dot_pos_item := 2; lookaheads_item := lookahead_set_6 |} ]%list.
Extract Inlined Constant items_of_state_105 => "assert false".
Definition items_of_state_107 : list item :=
[ {| prod_item := Prod'prog'0; dot_pos_item := 1; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_107 => "assert false".
Definition items_of_state_108 : list item :=
[ {| prod_item := Prod'app_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'app_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'atomic_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'atomic_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'atomic_obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'atomic_obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'atomic_obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'atomic_obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'atomic_obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_30 |};
{| prod_item := Prod'eq_obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'eq_obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| 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'fnbinder'2; dot_pos_item := 0; lookaheads_item := lookahead_set_3 |};
{| prod_item := Prod'obj'0; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'obj'1; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'obj'2; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'obj'3; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'obj'4; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'obj'5; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'obj'6; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'obj'7; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'obj'8; dot_pos_item := 0; lookaheads_item := lookahead_set_31 |};
{| prod_item := Prod'prog'0; dot_pos_item := 2; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_108 => "assert false".
Definition items_of_state_109 : list item :=
[ {| prod_item := Prod'prog'0; dot_pos_item := 3; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_109 => "assert false".
Definition items_of_state_110 : list item :=
[ {| prod_item := Prod'prog'0; dot_pos_item := 4; lookaheads_item := lookahead_set_4 |} ]%list.
Extract Inlined Constant items_of_state_110 => "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'90 => items_of_state_90
| 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
| Ninit Nis'95 => items_of_state_95
| Ninit Nis'96 => items_of_state_96
| Ninit Nis'97 => items_of_state_97
| Ninit Nis'98 => items_of_state_98
| Ninit Nis'99 => items_of_state_99
| Ninit Nis'100 => items_of_state_100
| Ninit Nis'101 => items_of_state_101
| Ninit Nis'102 => items_of_state_102
| Ninit Nis'103 => items_of_state_103
| Ninit Nis'104 => items_of_state_104
| Ninit Nis'105 => items_of_state_105
| Ninit Nis'107 => items_of_state_107
| Ninit Nis'108 => items_of_state_108
| Ninit Nis'109 => items_of_state_109
| Ninit Nis'110 => items_of_state_110
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'90 => 90%N
| Ninit Nis'91 => 91%N
| Ninit Nis'92 => 92%N
| Ninit Nis'93 => 93%N
| Ninit Nis'94 => 94%N
| Ninit Nis'95 => 95%N
| Ninit Nis'96 => 96%N
| Ninit Nis'97 => 97%N
| Ninit Nis'98 => 98%N
| Ninit Nis'99 => 99%N
| Ninit Nis'100 => 100%N
| Ninit Nis'101 => 101%N
| Ninit Nis'102 => 102%N
| Ninit Nis'103 => 103%N
| Ninit Nis'104 => 104%N
| Ninit Nis'105 => 105%N
| Ninit Nis'107 => 107%N
| Ninit Nis'108 => 108%N
| Ninit Nis'109 => 109%N
| Ninit Nis'110 => 110%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".