---

Step * 1 of Lemma radd-list-rabs

.....wf..... 
λL.(|radd-list(L)| ≤ radd-list(map(λx.|x|;L))) ∈ (ℝ List) ⟶ ℙ
BY
{ TACTIC:(RepeatFor 3 (TACTIC:MemCD') THEN Try (Complete (Auto)) THEN SubsumeC ⌜ℝ List⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
\mlambda{}L.(|radd-list(L)|  \mleq{}  radd-list(map(\mlambda{}x.|x|;L)))  \mmember{}  (\mBbbR{}  List)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
TACTIC:(RepeatFor  3  (TACTIC:MemCD')  THEN  Try  (Complete  (Auto))  THEN  SubsumeC  \mkleeneopen{}\mBbbR{}  List\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index