---

Step * of Lemma alpha-rename-aux_wf

No Annotations
∀[opr:Type]. ∀[t:term(opr)]. ∀[bnds:varname() List].
  ∀f:{v:varname()| (v ∈ bnds @ all-vars(t))}  ⟶ varname()
    alpha-rename-aux(f;bnds;t) ∈ term(opr) 
    supposing ∀x:{v:varname()| (v ∈ bnds @ all-vars(t))} 
                (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))
BY
{ (Intro
   THEN (Enough to prove ∀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()))))
          Because ((D 0 THENA Auto) THEN (D -2 With ⌜term-size(t)⌝  THENA Auto) THEN InstHyp [⌜t⌝] (-1)⋅ THEN Auto))
   THEN CompleteInductionOnNat
   THEN (D 0 THENA Auto)
   THEN (InstLemma `term-ext` [⌜opr⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜a = t ∈ coterm-fun(opr;term(opr))⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN (Assert t ∈ term(opr) BY
               Auto)
   THEN RepeatFor 2 (D -2)
   THEN Intros
   THEN Unhide) }

1
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)

2
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. y1 : opr
6. y2 : (varname() List × term(opr)) List
7. inr <y1, y2>  ∈ term(opr)
8. term-size(inr <y1, y2> ) ≤ n
9. bnds : varname() List
10. f : {v:varname()| (v ∈ bnds @ all-vars(inr <y1, y2> ))}  ⟶ varname()
11. ∀x:{v:varname()| (v ∈ bnds @ all-vars(inr <y1, y2> ))} . (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varnam\000Ce()))
⊢ alpha-rename-aux(f;bnds;inr <y1, y2> ) ∈ term(opr)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[t:term(opr)].  \mforall{}[bnds:varname()  List].
    \mforall{}f:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(t))\}    {}\mrightarrow{}  varname()
        alpha-rename-aux(f;bnds;t)  \mmember{}  term(opr) 
        supposing  \mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(t))\}  .  (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))


By

---

Latex:
(Intro
  THEN  (Enough  to  prove  \mforall{}n:\mBbbN{}
                                                  \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()))))
                Because  ((D  0  THENA  Auto)
                                  THEN  (D  -2  With  \mkleeneopen{}term-size(t)\mkleeneclose{}    THENA  Auto)
                                  THEN  InstHyp  [\mkleeneopen{}t\mkleeneclose{}]  (-1)\mcdot{}
                                  THEN  Auto))
  THEN  CompleteInductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `term-ext`  [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}a  =  t\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  (Assert  t  \mmember{}  term(opr)  BY
                          Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Intros
  THEN  Unhide)

---

Home Index