---

Step * of Lemma term-opr_functionality

No Annotations
∀[opr:Type]. ∀[t,t':term(opr)].
  (term-opr(t) = term-opr(t') ∈ opr) supposing (alpha-eq-terms(opr;t;t') and (¬↑isvarterm(t)))
BY
{ (Auto THEN (InstLemma `term-cases` [⌜opr⌝;⌜t⌝]⋅ THENA Auto) THEN D -1) }

1
1. opr : Type
2. t : term(opr)
3. t' : term(opr)
4. ¬↑isvarterm(t)
5. alpha-eq-terms(opr;t;t')
6. ∃v:varname(). ((¬(v = nullvar() ∈ varname())) ∧ (t = varterm(v) ∈ term(opr)))
⊢ term-opr(t) = term-opr(t') ∈ opr

2
1. opr : Type
2. t : term(opr)
3. t' : term(opr)
4. ¬↑isvarterm(t)
5. alpha-eq-terms(opr;t;t')
6. ∃f:opr. ∃bts:{bt:bound-term(opr)| bound-term-size(bt) < term-size(t)}  List. (t = mkterm(f;bts) ∈ term(opr))
⊢ term-opr(t) = term-opr(t') ∈ opr

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[t,t':term(opr)].
    (term-opr(t)  =  term-opr(t'))  supposing  (alpha-eq-terms(opr;t;t')  and  (\mneg{}\muparrow{}isvarterm(t)))


By

---

Latex:
(Auto  THEN  (InstLemma  `term-cases`  [\mkleeneopen{}opr\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index