---

Step * of Lemma replace-vars_wf

No Annotations
∀[opr:Type]. ∀[t:term(opr)]. ∀[s:(varname() × term(opr)) List].  (replace-vars(s;t) ∈ term(opr))
BY
{ (Intro
   THEN (Enough to prove ∀n:ℕ
                           ∀[a:term(opr)]
                             ((term-size(a) ≤ n)
                             ⇒ (∀[s:(varname() × term(opr)) List]. (replace-vars(s;a) ∈ term(opr))))
          Because ((D 0 THENA Auto) THEN (D -2 With ⌜term-size(t)⌝  THENA Auto) THEN InstHyp [⌜t⌝] (-1)⋅ THEN Auto))
   THEN CompleteInductionOnNat
   THEN (D 0 THENA Auto)
   THEN (InstLemma `term-ext` [⌜opr⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜a = t ∈ coterm-fun(opr;term(opr))⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN (Assert t ∈ term(opr) BY
               Auto)
   THEN RepeatFor 2 (D -2)
   THEN Intros
   THEN Unhide) }

1
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. x : varname()
6. ¬(x = nullvar() ∈ varname())
7. inl x ∈ term(opr)
8. term-size(inl x) ≤ n
9. s : (varname() × term(opr)) List
⊢ replace-vars(s;inl x) ∈ term(opr)

2
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[t:term(opr)].  \mforall{}[s:(varname()  \mtimes{}  term(opr))  List].    (replace-vars(s;t)  \mmember{}  term(opr))


By

---

Latex:
(Intro
  THEN  (Enough  to  prove  \mforall{}n:\mBbbN{}
                                                  \mforall{}[a:term(opr)]
                                                      ((term-size(a)  \mleq{}  n)
                                                      {}\mRightarrow{}  (\mforall{}[s:(varname()  \mtimes{}  term(opr))  List].  (replace-vars(s;a)  \mmember{}  term(opr))))
                Because  ((D  0  THENA  Auto)
                                  THEN  (D  -2  With  \mkleeneopen{}term-size(t)\mkleeneclose{}    THENA  Auto)
                                  THEN  InstHyp  [\mkleeneopen{}t\mkleeneclose{}]  (-1)\mcdot{}
                                  THEN  Auto))
  THEN  CompleteInductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `term-ext`  [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}a  =  t\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  (Assert  t  \mmember{}  term(opr)  BY
                          Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Intros
  THEN  Unhide)

---

Home Index