---

Step * 2 of Lemma replace-vars_wf


1. opr : Type
2. n : ℕ
3. ∀n:ℕn. ∀[a:term(opr)]. ((term-size(a) ≤ n) ⇒ (∀[s:(varname() × term(opr)) List]. (replace-vars(s;a) ∈ term(opr))))
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. s : (varname() × term(opr)) List
⊢ replace-vars(s;inr <y1, y2> ) ∈ term(opr)
BY
{ (Unfold `replace-vars` 0
   THEN Reduce 0
   THEN (GenConcl ⌜eager-map(λbt.let vs,b = bt in <vs, replace-vars(s;b)>;y2) = L ∈ (bound-term(opr) List)⌝⋅
   THENM Auto
   )) }

1
.....wf..... 
1. opr : Type
2. n : ℕ
3. ∀n:ℕn. ∀[a:term(opr)]. ((term-size(a) ≤ n) ⇒ (∀[s:(varname() × term(opr)) List]. (replace-vars(s;a) ∈ term(opr))))
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. s : (varname() × term(opr)) List
⊢ eager-map(λbt.let vs,b = bt 
                in <vs, replace-vars(s;b)>;y2) ∈ bound-term(opr) List

---

Latex:

---

Latex:

1.  opr  :  Type
2.  n  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}n
          \mforall{}[a:term(opr)]
              ((term-size(a)  \mleq{}  n)  {}\mRightarrow{}  (\mforall{}[s:(varname()  \mtimes{}  term(opr))  List].  (replace-vars(s;a)  \mmember{}  term(opr))))
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.  s  :  (varname()  \mtimes{}  term(opr))  List
\mvdash{}  replace-vars(s;inr  <y1,  y2>  )  \mmember{}  term(opr)


By

---

Latex:
(Unfold  `replace-vars`  0
  THEN  Reduce  0
  THEN  (GenConcl  \mkleeneopen{}eager-map(\mlambda{}bt.let  vs,b  =  bt  in  <vs,  replace-vars(s;b)>y2)  =  L\mkleeneclose{}\mcdot{}  THENM  Auto))

---

Home Index