Library langs.L1.well_boundness
Well-bound L1 terms as in paper Figure 10.
Section WellBoundness.
Context `{G: Graph (@AT T)}.
Inductive wb_exp : exp → Prop :=
| wb_cnum :
∀ s t z,
wb_exp (E s t (CNum z))
| wb_plus: ∀
s t s1 t1 e1 s2 t2 e2
(WB1: wb_exp (E s1 t1 e1))
(WB2: wb_exp (E s2 t2 e2)),
s = s2 →
s = s1 →
wb_exp (E s t (Plus (E s1 t1 e1) (E s2 t2 e2)))
| wb_var :
∀
s t r,
wb_exp (E s t (Var r))
| wb_fn :
∀
s t d s1 t0 t1 e1
(WB1: wb_exp (E s1 t1 e1))
(PS: linksofScopeP s1 [(P, [s])])
(DS: declsofScopeP s1 [d]),
wb_exp (E s t (Fn d t0 (E s1 t1 e1)))
| wb_app :
∀
s t s1 t1 e1 s2 t2 e2
(WB1: wb_exp (E s1 t1 e1))
(WB2: wb_exp (E s2 t2 e2)),
s = s1 →
s = s2 →
wb_exp (E s t (App (E s1 t1 e1) (E s2 t2 e2)))
.
Inductive wb_prog : prog → Prop :=
| wb_prog_ :
∀
s0 s t e
(WBE: wb_exp (E s t e))
(DS: declsofScopeP s0 [])
(LS : linksofScopeP s0 []),
s = s0 →
wb_prog (Prog (E s t e))
.
End WellBoundness.