---

Step * 2 1 2 1 1 of Lemma alpha-rename-aux_wf

.....assertion..... 
1. opr : Type
2. n : ℕ
3. term(opr) ≡ coterm-fun(opr;term(opr))
4. y1 : opr
5. y2 : (varname() List × term(opr)) List
6. inr <y1, y2>  ∈ term(opr)
7. term-size(inr <y1, y2> ) ≤ n
8. bnds : varname() List
9. f : {v:varname()| (v ∈ bnds @ all-vars(inr <y1, y2> ))}  ⟶ varname()
10. ∀x:{v:varname()| (v ∈ bnds @ all-vars(inr <y1, y2> ))} . (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varnam\000Ce()))
11. y2 ∈ {bt:varname() List × term(opr)| (bt ∈ y2)}  List
12. b1 : varname() List
13. b2 : term(opr)
14. (<b1, b2> ∈ y2)
15. 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ y2))
16. 1 ≤ n
17. ∀[a:term(opr)]
      ((term-size(a) ≤ (n - 1))
      ⇒ (∀[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()))))
⊢ {v:varname()| (v ∈ rev(b1) + bnds @ all-vars(b2))}  ⊆r {v:varname()| (v ∈ bnds @ all-vars(inr <y1, y2> ))} 
BY
{ ((D 0 THENA Auto) THEN D -1 THEN (MemTypeCD THENW Auto) THEN Try (Trivial)) }

1
.....set predicate..... 
1. opr : Type
2. n : ℕ
3. term(opr) ≡ coterm-fun(opr;term(opr))
4. y1 : opr
5. y2 : (varname() List × term(opr)) List
6. inr <y1, y2>  ∈ term(opr)
7. term-size(inr <y1, y2> ) ≤ n
8. bnds : varname() List
9. f : {v:varname()| (v ∈ bnds @ all-vars(inr <y1, y2> ))}  ⟶ varname()
10. ∀x:{v:varname()| (v ∈ bnds @ all-vars(inr <y1, y2> ))} . (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varnam\000Ce()))
11. y2 ∈ {bt:varname() List × term(opr)| (bt ∈ y2)}  List
12. b1 : varname() List
13. b2 : term(opr)
14. (<b1, b2> ∈ y2)
15. 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ y2))
16. 1 ≤ n
17. ∀[a:term(opr)]
      ((term-size(a) ≤ (n - 1))
      ⇒ (∀[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()))))
18. x : varname()
19. (x ∈ rev(b1) + bnds @ all-vars(b2))
⊢ (x ∈ bnds @ all-vars(inr <y1, y2> ))

---

Latex:

---

Latex:
.....assertion..... 
1.  opr  :  Type
2.  n  :  \mBbbN{}
3.  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))
4.  y1  :  opr
5.  y2  :  (varname()  List  \mtimes{}  term(opr))  List
6.  inr  <y1,  y2>    \mmember{}  term(opr)
7.  term-size(inr  <y1,  y2>  )  \mleq{}  n
8.  bnds  :  varname()  List
9.  f  :  \{v:varname()|  (v  \mmember{}  bnds  @  all-vars(inr  <y1,  y2>  ))\}    {}\mrightarrow{}  varname()
10.  \mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(inr  <y1,  y2>  ))\}  .  (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar())\000C)
11.  y2  \mmember{}  \{bt:varname()  List  \mtimes{}  term(opr)|  (bt  \mmember{}  y2)\}    List
12.  b1  :  varname()  List
13.  b2  :  term(opr)
14.  (<b1,  b2>  \mmember{}  y2)
15.  1  \mleq{}  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  y2))
16.  1  \mleq{}  n
17.  \mforall{}[a:term(opr)]
            ((term-size(a)  \mleq{}  (n  -  1))
            {}\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()))))
\mvdash{}  \{v:varname()|  (v  \mmember{}  rev(b1)  +  bnds  @  all-vars(b2))\}    \msubseteq{}r  \{v:varname()| 
                                                                                                                      (v  \mmember{}  bnds  @  all-vars(inr  <y1,  y2>  ))\} 


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  (MemTypeCD  THENW  Auto)  THEN  Try  (Trivial))

---

Home Index