---

Step * of Lemma awf_sum_wf

∀[n:ℕ]. ∀[s:awf(ℤ)].  (awf_sum(n;s) ∈ ℤ)
BY
{ (InductionOnNat
   THEN Auto
   THEN RecUnfold `awf_sum` 0
   THEN ((InstLemma `awf-subtype` [⌜ℤ⌝;⌜s⌝]⋅ THENA Auto) THEN GenConclAtAddr [2;1] THEN D -2 THEN Reduce 0 THEN Auto)
   ⋅) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[s:awf(\mBbbZ{})].    (awf\_sum(n;s)  \mmember{}  \mBbbZ{})


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  RecUnfold  `awf\_sum`  0
  THEN  ((InstLemma  `awf-subtype`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  GenConclAtAddr  [2;1]
              THEN  D  -2
              THEN  Reduce  0
              THEN  Auto)\mcdot{})

---

Home Index