---

Step * 2 of Lemma isvarterm_functionality


1. opr : Type
2. t : term(opr)
3. t' : term(opr)
4. alpha-eq-terms(opr;t;t')
5. ∃f:opr. ∃bts:{bt:bound-term(opr)| bound-term-size(bt) < term-size(t)}  List. (t = mkterm(f;bts) ∈ term(opr))
⊢ isvarterm(t) = isvarterm(t')
BY
{ (Subst' isvarterm(t) ~ ff 0 THENA (ExRepD THEN Auto THEN RWO "-1" 0 THEN Auto)) }

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

---

Latex:

---

Latex:

1.  opr  :  Type
2.  t  :  term(opr)
3.  t'  :  term(opr)
4.  alpha-eq-terms(opr;t;t')
5.  \mexists{}f:opr.  \mexists{}bts:\{bt:bound-term(opr)|  bound-term-size(bt)  <  term-size(t)\}    List.  (t  =  mkterm(f;bts))
\mvdash{}  isvarterm(t)  =  isvarterm(t')


By

---

Latex:
(Subst'  isvarterm(t)  \msim{}  ff  0  THENA  (ExRepD  THEN  Auto  THEN  RWO  "-1"  0  THEN  Auto))

---

Home Index