Step
*
1
1
1
1
2
1
1
1
of Lemma
real-path-comp-exists
.....aux..... 
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃m:ℕ+
       ((|t - (r1/r(2))| ≤ (r1/r(m)))
       
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃x:ℝ
       (((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
       ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]}  ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      (((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
      ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]} 
19. k : ℕ+
⊢ ∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) 
⇒ (N ≤ m) 
⇒ (|(h t (n + 1)) - h t (m + 1)| ≤ (r1/r(k)))))]
BY
{ ((InstHyp [⌜t⌝;⌜k⌝] (-6)⋅ THENA Auto)
   THEN D -1
   THEN D 0 With ⌜m⌝ 
   THEN Auto
   THEN RenameVar `j' (-3)
   THEN (InstHyp [⌜t⌝;⌜j + 1⌝] 17⋅ THENA Auto)
   THEN (InstHyp [⌜t⌝;⌜n + 1⌝] 17⋅ THENA Auto)
   THEN SplitOrHyps
   THEN ExRepD
   THEN RWO "-3 -1" 0
   THEN Auto) }
1
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃m:ℕ+
       ((|t - (r1/r(2))| ≤ (r1/r(m)))
       
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃x:ℝ
       (((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
       ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]}  ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      (((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
      ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]} 
19. k : ℕ+
20. m : ℕ+
21. (|t - (r1/r(2))| ≤ (r1/r(m))) 
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k)))
22. n : ℕ
23. j : ℕ
24. m ≤ n
25. m ≤ j
26. t < ((r1/r(2)) + (r1/r(j + 1)))
27. (h t (j + 1)) = f(r(2) * rmin(t;(r1/r(2))))
28. t < ((r1/r(2)) + (r1/r(n + 1)))
29. (h t (n + 1)) = f(r(2) * rmin(t;(r1/r(2))))
⊢ |f(r(2) * rmin(t;(r1/r(2)))) - f(r(2) * rmin(t;(r1/r(2))))| ≤ (r1/r(k))
2
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃m:ℕ+
       ((|t - (r1/r(2))| ≤ (r1/r(m)))
       
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃x:ℝ
       (((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
       ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]}  ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      (((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
      ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]} 
19. k : ℕ+
20. m : ℕ+
21. (|t - (r1/r(2))| ≤ (r1/r(m))) 
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k)))
22. n : ℕ
23. j : ℕ
24. m ≤ n
25. m ≤ j
26. ((r1/r(2)) - (r1/r(j + 1))) < t
27. (h t (j + 1)) = g((r(2) * rmax(t;(r1/r(2)))) - r1)
28. t < ((r1/r(2)) + (r1/r(n + 1)))
29. (h t (n + 1)) = f(r(2) * rmin(t;(r1/r(2))))
⊢ |f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k))
3
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃m:ℕ+
       ((|t - (r1/r(2))| ≤ (r1/r(m)))
       
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃x:ℝ
       (((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
       ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]}  ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      (((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
      ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]} 
19. k : ℕ+
20. m : ℕ+
21. (|t - (r1/r(2))| ≤ (r1/r(m))) 
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k)))
22. n : ℕ
23. j : ℕ
24. m ≤ n
25. m ≤ j
26. t < ((r1/r(2)) + (r1/r(j + 1)))
27. (h t (j + 1)) = f(r(2) * rmin(t;(r1/r(2))))
28. ((r1/r(2)) - (r1/r(n + 1))) < t
29. (h t (n + 1)) = g((r(2) * rmax(t;(r1/r(2)))) - r1)
⊢ |g((r(2) * rmax(t;(r1/r(2)))) - r1) - f(r(2) * rmin(t;(r1/r(2))))| ≤ (r1/r(k))
4
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) 
⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃m:ℕ+
       ((|t - (r1/r(2))| ≤ (r1/r(m)))
       
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      ∃x:ℝ
       (((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
       ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]}  ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
      (((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
      ∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]} 
19. k : ℕ+
20. m : ℕ+
21. (|t - (r1/r(2))| ≤ (r1/r(m))) 
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k)))
22. n : ℕ
23. j : ℕ
24. m ≤ n
25. m ≤ j
26. ((r1/r(2)) - (r1/r(j + 1))) < t
27. (h t (j + 1)) = g((r(2) * rmax(t;(r1/r(2)))) - r1)
28. ((r1/r(2)) - (r1/r(n + 1))) < t
29. (h t (n + 1)) = g((r(2) * rmax(t;(r1/r(2)))) - r1)
⊢ |g((r(2) * rmax(t;(r1/r(2)))) - r1) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k))
Latex:
Latex:
.....aux..... 
1.  f  :  [r0,  r1]  {}\mrightarrow{}\mBbbR{}
2.  g  :  [r0,  r1]  {}\mrightarrow{}\mBbbR{}
3.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y)))
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y)))
5.  f(r1)  =  g(r0)
6.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (rmin(t;(r1/r(2)))  =  t)
7.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (r(2)  *  t  \mmember{}  [r0,  r1])
8.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (f(r(2)  *  rmin(t;(r1/r(2))))  =  f(r(2)  *  t))
9.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  (rmax(t;(r1/r(2)))  =  t)
10.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  ((r(2)  *  t)  -  r1  \mmember{}  [r0,  r1])
11.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  (g((r(2)  *  rmax(t;(r1/r(2))))  -  r1)  =  g((r(2)  *  t)  -  r1))
12.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .  (f(r(2)  *  rmin(t;(r1/r(2))))  \mmember{}  \mBbbR{})
13.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .  (g((r(2)  *  rmax(t;(r1/r(2))))  -  r1)  \mmember{}  \mBbbR{})
14.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
            \mexists{}m:\mBbbN{}\msupplus{}
              ((|t  -  (r1/r(2))|  \mleq{}  (r1/r(m)))
              {}\mRightarrow{}  (|f(r(2)  *  rmin(t;(r1/r(2))))  -  g((r(2)  *  rmax(t;(r1/r(2))))  -  r1)|  \mleq{}  (r1/r(n))))
15.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
            \mexists{}x:\mBbbR{}
              (((t  <  ((r1/r(2))  +  (r1/r(n))))  \mwedge{}  (x  =  f(r(2)  *  rmin(t;(r1/r(2))))))
              \mvee{}  ((((r1/r(2))  -  (r1/r(n)))  <  t)  \mwedge{}  (x  =  g((r(2)  *  rmax(t;(r1/r(2))))  -  r1))))
16.  h  :  t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}    {}\mrightarrow{}  n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbR{}
17.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
            (((t  <  ((r1/r(2))  +  (r1/r(n))))  \mwedge{}  ((h  t  n)  =  f(r(2)  *  rmin(t;(r1/r(2))))))
            \mvee{}  ((((r1/r(2))  -  (r1/r(n)))  <  t)  \mwedge{}  ((h  t  n)  =  g((r(2)  *  rmax(t;(r1/r(2))))  -  r1))))
18.  t  :  \{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\} 
19.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}N:\mBbbN{}  [(\mforall{}n,m:\mBbbN{}.    ((N  \mleq{}  n)  {}\mRightarrow{}  (N  \mleq{}  m)  {}\mRightarrow{}  (|(h  t  (n  +  1))  -  h  t  (m  +  1)|  \mleq{}  (r1/r(k)))))]
By
Latex:
((InstHyp  [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  D  0  With  \mkleeneopen{}m\mkleeneclose{} 
  THEN  Auto
  THEN  RenameVar  `j'  (-3)
  THEN  (InstHyp  [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}j  +  1\mkleeneclose{}]  17\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{}]  17\mcdot{}  THENA  Auto)
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  RWO  "-3  -1"  0
  THEN  Auto)
Home
Index