---

Step * 1 1 2 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(). ((¬(v = nullvar() ∈ varname())) ∧ (t = varterm(v) ∈ term(opr)))
6. ∃f:opr. ∃bts:{bt:bound-term(opr)| bound-term-size(bt) < term-size(t')}  List. (t' = mkterm(f;bts) ∈ term(opr))
⊢ tt = isvarterm(t')
BY
{ ((Assert ⌜False⌝⋅ THEN Auto) THEN ExRepD) }

1
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

---

Latex:

---

Latex:

1.  opr  :  Type
2.  t  :  term(opr)
3.  t'  :  term(opr)
4.  alpha-eq-terms(opr;t;t')
5.  \mexists{}v:varname().  ((\mneg{}(v  =  nullvar()))  \mwedge{}  (t  =  varterm(v)))
6.  \mexists{}f:opr.  \mexists{}bts:\{bt:bound-term(opr)|  bound-term-size(bt)  <  term-size(t')\}    List.  (t'  =  mkterm(f;bts)\000C)
\mvdash{}  tt  =  isvarterm(t')


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  ExRepD)

---

Home Index