---

Step * of Lemma int_part_decomp_wf

∀[q:ℚ]. (int_part_decomp(q) ∈ {p:ℤ × ℚ| (0 ≤ (snd(p))) ∧ snd(p) < 1 ∧ (q = ((fst(p)) + (snd(p))) ∈ ℚ)} )
BY
{ xxx(ProveWfLemma
      THEN GenConclAtAddr [2]
      THEN RepeatFor 2 (D 2)
      THEN DVar `v2'
      THEN MemTypeCD
      THEN All Reduce
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[q:\mBbbQ{}].  (int\_part\_decomp(q)  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  \mBbbQ{}|  (0  \mleq{}  (snd(p)))  \mwedge{}  snd(p)  <  1  \mwedge{}  (q  =  ((fst(p))  +  (snd(p))))\}  )


By

---

Latex:
xxx(ProveWfLemma
        THEN  GenConclAtAddr  [2]
        THEN  RepeatFor  2  (D  2)
        THEN  DVar  `v2'
        THEN  MemTypeCD
        THEN  All  Reduce
        THEN  Auto)xxx

---

Home Index