---

Step * 1 1 2 1 of Lemma isvarterm_functionality


1. opr : Type
2. t : term(opr)
3. t' : term(opr)
4. alpha-eq-terms(opr;t;t')
5. v : varname()
6. ¬(v = nullvar() ∈ varname())
7. t = varterm(v) ∈ term(opr)
8. f : opr
9. bts : {bt:bound-term(opr)| bound-term-size(bt) < term-size(t')}  List
10. t' = mkterm(f;bts) ∈ term(opr)
⊢ False
BY
{ ((Assert alpha-eq-terms(opr;varterm(v);mkterm(f;bts)) BY
          Auto)
   THEN RW (TagC (mk_tag_term 4)) (-1)
   THEN Reduce -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  t  :  term(opr)
3.  t'  :  term(opr)
4.  alpha-eq-terms(opr;t;t')
5.  v  :  varname()
6.  \mneg{}(v  =  nullvar())
7.  t  =  varterm(v)
8.  f  :  opr
9.  bts  :  \{bt:bound-term(opr)|  bound-term-size(bt)  <  term-size(t')\}    List
10.  t'  =  mkterm(f;bts)
\mvdash{}  False


By

---

Latex:
((Assert  alpha-eq-terms(opr;varterm(v);mkterm(f;bts))  BY
                Auto)
  THEN  RW  (TagC  (mk\_tag\_term  4))  (-1)
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index