---

Step * of Lemma Longs-algorithm_wf

∀[h:ℤ ⟶ ℤ]. ∀n:ℕ ⟶ ℕ. ∀a,b,c:ℕ.  (Longs-algorithm(h;n;a;b;c) ∈ ℤ)
BY
{ (RepeatFor 3 (InductionOnNat)
   THEN RecUnfold `Longs-algorithm` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (Repeat (AutoSplit)
         THEN Repeat ((CallByValueReduce 0⋅ THENA Auto))⋅
         THEN MemCD
         THEN Try (Complete (Auto))
         THEN Try ((RecUnfold `Longs-algorithm` 0⋅ THEN Reduce 0 THEN Complete (Auto))⋅))⋅) }

1
.....subterm..... T:t
2:n
1. h : ℤ ⟶ ℤ
2. n : ℕ ⟶ ℕ
3. a : ℤ
4. a ≠ 0
5. 0 < a
6. ∀b,c:ℕ.  (Longs-algorithm(h;n;a - 1;b;c) ∈ ℤ)
7. b : ℤ
8. c : ℤ
9. ¬c < 0
10. 0 < c
11. Longs-algorithm(h;n;a;0;c - 1) ∈ ℤ
⊢ Longs-algorithm(h;n;a - 1;(n (a - 1)) - c;c) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[h:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a,b,c:\mBbbN{}.    (Longs-algorithm(h;n;a;b;c)  \mmember{}  \mBbbZ{})


By

---

Latex:
(RepeatFor  3  (InductionOnNat)
  THEN  RecUnfold  `Longs-algorithm`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (Repeat  (AutoSplit)
              THEN  Repeat  ((CallByValueReduce  0\mcdot{}  THENA  Auto))\mcdot{}
              THEN  MemCD
              THEN  Try  (Complete  (Auto))
              THEN  Try  ((RecUnfold  `Longs-algorithm`  0\mcdot{}  THEN  Reduce  0  THEN  Complete  (Auto))\mcdot{}))\mcdot{})

---

Home Index