---

Step * of Lemma wf-term_wf

No Annotations
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[t:term(opr)].  (wf-term(arity;sort;t) ∈ 𝔹)
BY
{ (RepeatFor 3 (Intro)
   THEN (Enough to prove ∀n:ℕ. ∀[a:term(opr)]. ((term-size(a) ≤ n) ⇒ (wf-term(arity;sort;a) ∈ 𝔹))
          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
   THEN Unfold `wf-term` 0
   THEN Reduce 0
   THEN Try (((GenConcl ⌜(arity y1) = ns ∈ (ℕ List)⌝⋅ THENA Auto) THEN (CallByValueReduce 0 THENA Auto)))
   THEN Auto
   THEN (Assert 1 ≤ term-size(inr <y1, y2> ) BY
               (Fold `mkterm` 0 THEN Auto))
   THEN (D 5 With ⌜n - 1⌝  THENA Auto)
   THEN BHyp -1
   THEN Auto) }

1
1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
4. n : ℕ
5. term(opr) ≡ coterm-fun(opr;term(opr))
6. y1 : opr
7. y2 : (varname() List × term(opr)) List
8. inr <y1, y2>  ∈ term(opr)
9. term-size(inr <y1, y2> ) ≤ n
10. ↑(||arity y1|| =z ||y2||)
11. ||arity y1|| = ||y2|| ∈ ℤ
12. ∀x:ℕ × ℕ × varname() List × term(opr). ((x ∈ zip(arity y1;y2)) ∈ 𝕌{[1 | i 0]})
13. n1 : ℕ × ℕ
14. n3 : varname() List
15. n4 : term(opr)
16. (<n1, n3, n4> ∈ zip(arity y1;y2))
17. ↑(fst(n1) =z ||n3||)
18. (fst(n1)) = ||n3|| ∈ ℤ
19. ↑(sort n4 =z snd(n1))
20. (sort n4) = (snd(n1)) ∈ ℤ
21. 1 ≤ term-size(inr <y1, y2> )
22. ∀[a:term(opr)]. ((term-size(a) ≤ (n - 1)) ⇒ (wf-term(arity;sort;a) ∈ 𝔹))
⊢ term-size(n4) ≤ (n - 1)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[sort:term(opr)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)].  \mforall{}[t:term(opr)].
    (wf-term(arity;sort;t)  \mmember{}  \mBbbB{})


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (Enough  to  prove  \mforall{}n:\mBbbN{}.  \mforall{}[a:term(opr)].  ((term-size(a)  \mleq{}  n)  {}\mRightarrow{}  (wf-term(arity;sort;a)  \mmember{}  \mBbbB{}))
                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
  THEN  Unfold  `wf-term`  0
  THEN  Reduce  0
  THEN  Try  (((GenConcl  \mkleeneopen{}(arity  y1)  =  ns\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (CallByValueReduce  0  THENA  Auto)))
  THEN  Auto
  THEN  (Assert  1  \mleq{}  term-size(inr  <y1,  y2>  )  BY
                          (Fold  `mkterm`  0  THEN  Auto))
  THEN  (D  5  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)
  THEN  BHyp  -1
  THEN  Auto)

---

Home Index