---

Step * 1 of Lemma wf-term_wf


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)
BY
{ (Fold `mkterm` 9
   THEN Reduce 9
   THEN (Enough to prove term-size(snd(<n3, n4>)) ≤ Σ(term-size(snd(bt)) | bt ∈ y2)
          Because (Reduce -1 THEN Auto))
   THEN (InstLemma `summand-le-lsum` [⌜varname() List × term(opr)⌝;⌜y2⌝;⌜λ2bt.term-size(snd(bt))⌝]⋅ THENA Auto)
   THEN BHyp -1
   THEN Auto) }

1
.....wf..... 
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. (1 + Σ(term-size(snd(bt)) | bt ∈ 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) ∈ 𝔹))
23. ∀x:{x:varname() List × term(opr)| (x ∈ y2)} . (term-size(snd(x)) ≤ Σ(term-size(snd(x)) | x ∈ y2))
⊢ <n3, n4> ∈ {x:varname() List × term(opr)| (x ∈ y2)} 

---

Latex:

---

Latex:

1.  opr  :  Type
2.  sort  :  term(opr)  {}\mrightarrow{}  \mBbbN{}
3.  arity  :  opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)
4.  n  :  \mBbbN{}
5.  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))
6.  y1  :  opr
7.  y2  :  (varname()  List  \mtimes{}  term(opr))  List
8.  inr  <y1,  y2>    \mmember{}  term(opr)
9.  term-size(inr  <y1,  y2>  )  \mleq{}  n
10.  \muparrow{}(||arity  y1||  =\msubz{}  ||y2||)
11.  ||arity  y1||  =  ||y2||
12.  \mforall{}x:\mBbbN{}  \mtimes{}  \mBbbN{}  \mtimes{}  varname()  List  \mtimes{}  term(opr).  ((x  \mmember{}  zip(arity  y1;y2))  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
13.  n1  :  \mBbbN{}  \mtimes{}  \mBbbN{}
14.  n3  :  varname()  List
15.  n4  :  term(opr)
16.  (<n1,  n3,  n4>  \mmember{}  zip(arity  y1;y2))
17.  \muparrow{}(fst(n1)  =\msubz{}  ||n3||)
18.  (fst(n1))  =  ||n3||
19.  \muparrow{}(sort  n4  =\msubz{}  snd(n1))
20.  (sort  n4)  =  (snd(n1))
21.  1  \mleq{}  term-size(inr  <y1,  y2>  )
22.  \mforall{}[a:term(opr)].  ((term-size(a)  \mleq{}  (n  -  1))  {}\mRightarrow{}  (wf-term(arity;sort;a)  \mmember{}  \mBbbB{}))
\mvdash{}  term-size(n4)  \mleq{}  (n  -  1)


By

---

Latex:
(Fold  `mkterm`  9
  THEN  Reduce  9
  THEN  (Enough  to  prove  term-size(snd(<n3,  n4>))  \mleq{}  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  y2)
                Because  (Reduce  -1  THEN  Auto))
  THEN  (InstLemma  `summand-le-lsum`  [\mkleeneopen{}varname()  List  \mtimes{}  term(opr)\mkleeneclose{};\mkleeneopen{}y2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}bt.term-size(snd(bt))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  BHyp  -1
  THEN  Auto)

---

Home Index