---

Step * 2 1 1 1 of Lemma replace-vars_wf


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. s : (varname() × term(opr)) List
9. y2 ∈ {bt:varname() List × term(opr)| (bt ∈ y2)}  List
10. b1 : varname() List
11. b2 : term(opr)
12. (<b1, b2> ∈ y2)
13. 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ y2))
14. 1 ≤ n
15. ∀[a:term(opr)]. ((term-size(a) ≤ (n - 1)) ⇒ (∀[s:(varname() × term(opr)) List]. (replace-vars(s;a) ∈ term(opr))))
⊢ replace-vars(s;b2) ∈ term(opr)
BY
{ BackThruSomeHyp }

1
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. s : (varname() × term(opr)) List
9. y2 ∈ {bt:varname() List × term(opr)| (bt ∈ y2)}  List
10. b1 : varname() List
11. b2 : term(opr)
12. (<b1, b2> ∈ y2)
13. 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ y2))
14. 1 ≤ n
15. ∀[a:term(opr)]. ((term-size(a) ≤ (n - 1)) ⇒ (∀[s:(varname() × term(opr)) List]. (replace-vars(s;a) ∈ term(opr))))
⊢ term-size(b2) ≤ (n - 1)

---

Latex:

---

Latex:

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.  s  :  (varname()  \mtimes{}  term(opr))  List
9.  y2  \mmember{}  \{bt:varname()  List  \mtimes{}  term(opr)|  (bt  \mmember{}  y2)\}    List
10.  b1  :  varname()  List
11.  b2  :  term(opr)
12.  (<b1,  b2>  \mmember{}  y2)
13.  1  \mleq{}  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  y2))
14.  1  \mleq{}  n
15.  \mforall{}[a:term(opr)]
            ((term-size(a)  \mleq{}  (n  -  1))
            {}\mRightarrow{}  (\mforall{}[s:(varname()  \mtimes{}  term(opr))  List].  (replace-vars(s;a)  \mmember{}  term(opr))))
\mvdash{}  replace-vars(s;b2)  \mmember{}  term(opr)


By

---

Latex:
BackThruSomeHyp

---

Home Index