---

Step * 2 1 of Lemma alpha-rename-aux_wf

.....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. 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()))
⊢ eager-map(λbt.let vs,a = bt 
                in <map(f;vs), alpha-rename-aux(f;rev(vs) + bnds;a)>;y2) ∈ bound-term(opr) List
BY
{ ((Assert y2 ∈ {bt:varname() List × term(opr)| (bt ∈ y2)}  List BY
          Auto)
   THEN (Enough to prove λbt.let vs,a = bt 
                             in <map(f;vs), alpha-rename-aux(f;rev(vs) + bnds;a)> ∈ {bt:varname() List × term(opr)| 
                                                                                     (bt ∈ y2)}  ⟶ bound-term(opr)
          Because Auto)
   THEN (MemCD THENL [(D -1 THEN D -2 THEN Reduce 0 THEN Unfold `bound-term` 0 THEN MemCD); Auto])) }

1
.....subterm..... T:t
1:n
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()))
12. y2 ∈ {bt:varname() List × term(opr)| (bt ∈ y2)}  List
13. b1 : varname() List
14. b2 : term(opr)
15. (<b1, b2> ∈ y2)
⊢ map(f;b1) ∈ varname() List

2
.....subterm..... T:t
2:n
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()))
12. y2 ∈ {bt:varname() List × term(opr)| (bt ∈ y2)}  List
13. b1 : varname() List
14. b2 : term(opr)
15. (<b1, b2> ∈ y2)
⊢ alpha-rename-aux(f;rev(b1) + bnds;b2) ∈ term(opr)

---

Latex:

---

Latex:
.....wf..... 
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.  y1  :  opr
6.  y2  :  (varname()  List  \mtimes{}  term(opr))  List
7.  inr  <y1,  y2>    \mmember{}  term(opr)
8.  term-size(inr  <y1,  y2>  )  \mleq{}  n
9.  bnds  :  varname()  List
10.  f  :  \{v:varname()|  (v  \mmember{}  bnds  @  all-vars(inr  <y1,  y2>  ))\}    {}\mrightarrow{}  varname()
11.  \mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(inr  <y1,  y2>  ))\}  .  (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar())\000C)
\mvdash{}  eager-map(\mlambda{}bt.let  vs,a  =  bt 
                                in  <map(f;vs),  alpha-rename-aux(f;rev(vs)  +  bnds;a)>y2)  \mmember{}  bound-term(opr)  List


By

---

Latex:
((Assert  y2  \mmember{}  \{bt:varname()  List  \mtimes{}  term(opr)|  (bt  \mmember{}  y2)\}    List  BY
                Auto)
  THEN  (Enough  to  prove  \mlambda{}bt.let  vs,a  =  bt 
                                                      in  <map(f;vs),  alpha-rename-aux(f;rev(vs)  +  bnds;a)>  \mmember{}  \{bt:varname()  List
                                                                                                                                                                      \mtimes{}  term(opr)| 
                                                                                                                                                                      (bt  \mmember{}  y2)\}    {}\mrightarrow{}  bo\000Cund-term(opr)
                Because  Auto)
  THEN  (MemCD  THENL  [(D  -1  THEN  D  -2  THEN  Reduce  0  THEN  Unfold  `bound-term`  0  THEN  MemCD);  Auto]))

---

Home Index