Step
*
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(). ((¬(v = nullvar() ∈ varname())) ∧ (t = varterm(v) ∈ term(opr)))
⊢ isvarterm(t) = isvarterm(t')
BY
{ (Subst' isvarterm(t) ~ tt 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. ∃v:varname(). ((¬(v = nullvar() ∈ varname())) ∧ (t = varterm(v) ∈ term(opr)))
⊢ tt = isvarterm(t')
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)))
\mvdash{}  isvarterm(t)  =  isvarterm(t')
By
Latex:
(Subst'  isvarterm(t)  \msim{}  tt  0  THENA  (ExRepD  THEN  Auto  THEN  RWO  "-1"  0  THEN  Auto))
Home
Index