---

Step * 2 of Lemma alpha-aux_wf


1. opr : Type
2. n : ℕ
3. term(opr) ≡ coterm-fun(opr;term(opr))
4. y1 : opr
5. u : varname() List × term(opr)
6. v : (varname() List × term(opr)) List
7. inr <y1, [u / v]>  ∈ term(opr)
8. (1 + Σ(term-size(snd(bt)) | bt ∈ [u / v])) ≤ n
9. y3 : opr
10. u1 : varname() List × term(opr)
11. v1 : (varname() List × term(opr)) List
12. inr <y3, [u1 / v1]>  ∈ term(opr)
13. vs : varname() List
14. ws : varname() List
15. 0 ≤ Σ(term-size(snd(bt)) | bt ∈ [u / v])
16. ∀[a:term(opr)]
      ((term-size(a) ≤ (n - 1)) ⇒ (∀[b:term(opr)]. ∀[vs,ws:varname() List].  (alpha-aux(opr;vs;ws;a;b) ∈ ℙ)))
17. let as,x = u 
    in let bs,y = u1 
       in alpha-aux(opr;rev(as) + vs;rev(bs) + ws;x;y)
⊢ term-size(mkterm(y1;v)) ≤ (n - 1)
BY
{ ((Enough to prove term-size(mkterm(y1;v)) ≤ Σ(term-size(snd(bt)) | bt ∈ [u / v])
     Because Auto)
   THEN Reduce 0
   THEN (Assert 1 ≤ term-size(snd(u)) BY
               Auto)
   THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  n  :  \mBbbN{}
3.  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))
4.  y1  :  opr
5.  u  :  varname()  List  \mtimes{}  term(opr)
6.  v  :  (varname()  List  \mtimes{}  term(opr))  List
7.  inr  <y1,  [u  /  v]>    \mmember{}  term(opr)
8.  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  [u  /  v]))  \mleq{}  n
9.  y3  :  opr
10.  u1  :  varname()  List  \mtimes{}  term(opr)
11.  v1  :  (varname()  List  \mtimes{}  term(opr))  List
12.  inr  <y3,  [u1  /  v1]>    \mmember{}  term(opr)
13.  vs  :  varname()  List
14.  ws  :  varname()  List
15.  0  \mleq{}  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  [u  /  v])
16.  \mforall{}[a:term(opr)]
            ((term-size(a)  \mleq{}  (n  -  1))
            {}\mRightarrow{}  (\mforall{}[b:term(opr)].  \mforall{}[vs,ws:varname()  List].    (alpha-aux(opr;vs;ws;a;b)  \mmember{}  \mBbbP{})))
17.  let  as,x  =  u 
        in  let  bs,y  =  u1 
              in  alpha-aux(opr;rev(as)  +  vs;rev(bs)  +  ws;x;y)
\mvdash{}  term-size(mkterm(y1;v))  \mleq{}  (n  -  1)


By

---

Latex:
((Enough  to  prove  term-size(mkterm(y1;v))  \mleq{}  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  [u  /  v])
      Because  Auto)
  THEN  Reduce  0
  THEN  (Assert  1  \mleq{}  term-size(snd(u))  BY
                          Auto)
  THEN  Auto)

---

Home Index