---

Step * 1 1 of Lemma radd-list-cons


1. L : ℝ List
2. ||L|| + 1 ≠ 0
3. x : ℝ
4. ||L|| = 0 ∈ ℤ
⊢ bdd-diff(reg-seq-list-add([x / L]);λn.((x n) + (r0 n) + 0))
BY
{ (DVar `L'
   THEN All Reduce
   THEN Auto'
   THEN BLemma `bdd-diff_weakening`
   THEN Auto
   THEN (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto)
   THEN Reduce 0
   THEN EqCD⋅
   THEN Auto
   THEN RepUR ``int-to-real`` 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  L  :  \mBbbR{}  List
2.  ||L||  +  1  \mneq{}  0
3.  x  :  \mBbbR{}
4.  ||L||  =  0
\mvdash{}  bdd-diff(reg-seq-list-add([x  /  L]);\mlambda{}n.((x  n)  +  (r0  n)  +  0))


By

---

Latex:
(DVar  `L'
  THEN  All  Reduce
  THEN  Auto'
  THEN  BLemma  `bdd-diff\_weakening`
  THEN  Auto
  THEN  (RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD\mcdot{}
  THEN  Auto
  THEN  RepUR  ``int-to-real``  0
  THEN  Auto)\mcdot{}

---

Home Index