---

Step * 1 of Lemma alpha-rename-aux_wf


1. opr : Type
2. n : ℕ
3. ∀n:ℕn
     ∀[a:term(opr)]
       ((term-size(a) ≤ n)
       ⇒ (∀[bnds:varname() List]
             ∀f:{v:varname()| (v ∈ bnds @ all-vars(a))}  ⟶ varname()
               alpha-rename-aux(f;bnds;a) ∈ term(opr) 
               supposing ∀x:{v:varname()| (v ∈ bnds @ all-vars(a))} 
                           (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
4. term(opr) ≡ coterm-fun(opr;term(opr))
5. x : varname()
6. ¬(x = nullvar() ∈ varname())
7. inl x ∈ term(opr)
8. term-size(inl x) ≤ n
9. bnds : varname() List
10. f : {v:varname()| (v ∈ bnds @ all-vars(inl x))}  ⟶ varname()
11. ∀x:{v:varname()| (v ∈ bnds @ all-vars(inl x))} . (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))
⊢ alpha-rename-aux(f;bnds;inl x) ∈ term(opr)
BY
{ (Unfold `all-vars` -2 THEN Reduce -2 THEN Unfold `alpha-rename-aux` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  n  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}n
          \mforall{}[a:term(opr)]
              ((term-size(a)  \mleq{}  n)
              {}\mRightarrow{}  (\mforall{}[bnds:varname()  List]
                          \mforall{}f:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(a))\}    {}\mrightarrow{}  varname()
                              alpha-rename-aux(f;bnds;a)  \mmember{}  term(opr) 
                              supposing  \mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(a))\} 
                                                      (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))))
4.  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))
5.  x  :  varname()
6.  \mneg{}(x  =  nullvar())
7.  inl  x  \mmember{}  term(opr)
8.  term-size(inl  x)  \mleq{}  n
9.  bnds  :  varname()  List
10.  f  :  \{v:varname()|  (v  \mmember{}  bnds  @  all-vars(inl  x))\}    {}\mrightarrow{}  varname()
11.  \mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(inl  x))\}  .  (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))
\mvdash{}  alpha-rename-aux(f;bnds;inl  x)  \mmember{}  term(opr)


By

---

Latex:
(Unfold  `all-vars`  -2  THEN  Reduce  -2  THEN  Unfold  `alpha-rename-aux`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index