---

Step * 1 of Lemma case-real_wf

.....assertion..... 
1. P : ℙ
2. a : ℕ+ ⟶ ℤ
3. regular-seq(a)
4. b : ℕ+ ⟶ ℤ
5. regular-seq(b)
6. f : {n:ℕ+| 4 < |(a n) - b n|}  ⟶ ((↓P) ∨ (↓¬P))
7. λn.if 4 <z |(a n) - b n| ∧b (f n) then a n else b n fi  ∈ ℕ+ ⟶ ℤ
⊢ 3-regular-seq(λn.if 4 <z |(a n) - b n| ∧b (f n) then a n else b n fi )
BY
{ (RepeatFor 2 ((D 0 THENW Auto))
   THEN Reduce 0
   THEN (BoolCase ⌜4 <z |(a n) - b n|⌝⋅ THENA Auto)
   THEN (BoolCase ⌜4 <z |(a m) - b m|⌝⋅ THENA Auto)
   THEN Try (((D 5 With ⌜n⌝  THENA Auto) THEN RWO "-1" 0 THEN Auto))
   THEN Try (((GenConclTerm ⌜f n⌝⋅ THENM (D -2 THEN Progress(Reduce 0))) THENA Auto))
   THEN Try (((GenConclTerm ⌜f m⌝⋅ THENM (D -2 THEN Progress(Reduce 0))) THENA Auto))
   THEN Try (((D 3 With ⌜n⌝  THENA Auto) THEN RWO "-1" 0 THEN Auto))
   THEN Try (((D 5 With ⌜n⌝  THENA Auto) THEN RWO "-1" 0 THEN Auto))
   THEN Try (((Assert ⌜False⌝⋅ THENM Trivial)
              THEN D -4
              THEN D -2
              THEN OnMaybeHyp 11 (\h. (Unfold `not` h THEN BHyp h THEN Trivial))))) }

1
1. P : ℙ
2. a : ℕ+ ⟶ ℤ
3. regular-seq(a)
4. b : ℕ+ ⟶ ℤ
5. regular-seq(b)
6. f : {n:ℕ+| 4 < |(a n) - b n|}  ⟶ ((↓P) ∨ (↓¬P))
7. λn.if 4 <z |(a n) - b n| ∧b (f n) then a n else b n fi  ∈ ℕ+ ⟶ ℤ
8. n : ℕ+
9. m : ℕ+
10. ¬4 < |(a m) - b m|
11. 4 < |(a n) - b n|
12. x : ↓P
13. (f n) = (inl x) ∈ ((↓P) ∨ (↓¬P))
⊢ |(m * (a n)) - n * (b m)| ≤ (6 * (n + m))

2
1. P : ℙ
2. a : ℕ+ ⟶ ℤ
3. regular-seq(a)
4. b : ℕ+ ⟶ ℤ
5. regular-seq(b)
6. f : {n:ℕ+| 4 < |(a n) - b n|}  ⟶ ((↓P) ∨ (↓¬P))
7. λn.if 4 <z |(a n) - b n| ∧b (f n) then a n else b n fi  ∈ ℕ+ ⟶ ℤ
8. n : ℕ+
9. ¬4 < |(a n) - b n|
10. m : ℕ+
11. 4 < |(a m) - b m|
12. x : ↓P
13. (f m) = (inl x) ∈ ((↓P) ∨ (↓¬P))
⊢ |(m * (b n)) - n * (a m)| ≤ (6 * (n + m))

---

Latex:

---

Latex:
.....assertion..... 
1.  P  :  \mBbbP{}
2.  a  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  regular-seq(a)
4.  b  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
5.  regular-seq(b)
6.  f  :  \{n:\mBbbN{}\msupplus{}|  4  <  |(a  n)  -  b  n|\}    {}\mrightarrow{}  ((\mdownarrow{}P)  \mvee{}  (\mdownarrow{}\mneg{}P))
7.  \mlambda{}n.if  4  <z  |(a  n)  -  b  n|  \mwedge{}\msubb{}  (f  n)  then  a  n  else  b  n  fi    \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  3-regular-seq(\mlambda{}n.if  4  <z  |(a  n)  -  b  n|  \mwedge{}\msubb{}  (f  n)  then  a  n  else  b  n  fi  )


By

---

Latex:
(RepeatFor  2  ((D  0  THENW  Auto))
  THEN  Reduce  0
  THEN  (BoolCase  \mkleeneopen{}4  <z  |(a  n)  -  b  n|\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}4  <z  |(a  m)  -  b  m|\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (((D  5  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  Try  (((GenConclTerm  \mkleeneopen{}f  n\mkleeneclose{}\mcdot{}  THENM  (D  -2  THEN  Progress(Reduce  0)))  THENA  Auto))
  THEN  Try  (((GenConclTerm  \mkleeneopen{}f  m\mkleeneclose{}\mcdot{}  THENM  (D  -2  THEN  Progress(Reduce  0)))  THENA  Auto))
  THEN  Try  (((D  3  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  Try  (((D  5  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  Try  (((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THENM  Trivial)
                        THEN  D  -4
                        THEN  D  -2
                        THEN  OnMaybeHyp  11  (\mbackslash{}h.  (Unfold  `not`  h  THEN  BHyp  h  THEN  Trivial)))))

---

Home Index