---

Step * 1 of Lemma term-cases


1. opr : Type
2. term(opr) ≡ coterm-fun(opr;term(opr))
3. f : opr
4. bts : (varname() List × term(opr)) List
5. inr <f, bts>  ∈ term(opr)
6. bts ∈ {a:bound-term(opr)| (a ∈ bts)}  List
7. bts = bts ∈ ({a:bound-term(opr)| (a ∈ bts)}  List)
8. a : bound-term(opr)
9. (a ∈ bts)
⊢ bound-term-size(a) < 1 + Σ(bound-term-size(bt) | bt ∈ bts)
BY
{ (InstLemma `summand-le-lsum` [⌜bound-term(opr)⌝;⌜bts⌝;⌜λ2bt.bound-term-size(bt)⌝;⌜a⌝] ⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))
3.  f  :  opr
4.  bts  :  (varname()  List  \mtimes{}  term(opr))  List
5.  inr  <f,  bts>    \mmember{}  term(opr)
6.  bts  \mmember{}  \{a:bound-term(opr)|  (a  \mmember{}  bts)\}    List
7.  bts  =  bts
8.  a  :  bound-term(opr)
9.  (a  \mmember{}  bts)
\mvdash{}  bound-term-size(a)  <  1  +  \mSigma{}(bound-term-size(bt)  |  bt  \mmember{}  bts)


By

---

Latex:
(InstLemma  `summand-le-lsum`  [\mkleeneopen{}bound-term(opr)\mkleeneclose{};\mkleeneopen{}bts\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}bt.bound-term-size(bt)\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  \mcdot{}  THEN  Auto)

---

Home Index