Examples of Manip Strategies

EXAMPLE 1

[-1]  (x!1 + 4) * (x!1 - 3) >= 0
  |-------
[1]   x!1 <= -4
[2]   x!1 >= 3

Rule?  (MULT-CASES -1) 

This completes the proof of t23.1.

EXAMPLE 2

[-1]  px!1 >= 1
  |-------
{1}   (px!1 * px!1) >= 1

Rule?  (mult-ineq -1 -1) 

{-1}  px!1 * px!1 >= 1 * 1
[-2]  px!1 >= 1
  |-------
[1]   (px!1 * px!1) >= 1

Rule? (assert)
Q.E.D.

EXAMPLE 3

{-1}  pa!1 < pb!1
  |-------
{1}   (pa!1 - 1) / pa!1 < (pb!1 - 1) / pb!1

Rule?  (CROSS-MULT 1) 
[-1]  pa!1 < pb!1
  |-------
{1}   pa!1 * pb!1 - pb!1 < pa!1 * pb!1 - pa!1

Rule? (assert)
Q.E.D.

EXAMPLE 4

{-1}  x!1 - 1 < 0
  |-------
{1}   x!1 < 0
{2}   x!1 * x!1 <= 1

Rule?  (MOVE-TERMS -1 L 2)  (ASSERT)

{-1}  (x!1 < 1)
  |-------
[1]   x!1 < 0
[2]   x!1 * x!1 <= 1

Rule?  (MULT-INEQ -1 -1) 

{-1}  x!1 * x!1 < 1 * 1
[-2]  (x!1 < 1)
  |-------
[1]   x!1 < 0
[2]   x!1 * x!1 <= 1

Rule? (ASSERT)
Q.E.D.

EXAMPLE 5

[-1]  sqrt(8 * nnx!1) - sqrt(2 * nnx!1) = a!1
  |-------
[1]   nnx!1 = sq(a!1) / 2

Rule?  (TRANSFORM-BOTH -1 "sq(%1)") 

{-1}  sq(sqrt(8 * nnx!1) - sqrt(2 * nnx!1)) = sq(a!1)
[-2]  sqrt(8 * nnx!1) - sqrt(2 * nnx!1) = a!1
  |-------
[1]   nnx!1 = sq(a!1) / 2

EXAMPLE 6

{-1}  b!1 > a!1
{-2}  (1 + floor((b!1 - a!1) / pd!1)) = 0
  |-------

Rule?  (INVOKE (CASE "%1 > 0") (! -2 (-> "floor") 1)) 

{-1}  (b!1 - a!1) / pd!1 > 0
[-2]  b!1 > a!1
[-3]  (1 + floor((b!1 - a!1) / pd!1)) = 0
  |-------

Rule? (ASSERT)

This completes the proof of t61_TCC1.1.

t61_TCC1.2 :  

[-1]  b!1 > a!1
[-2]  (1 + floor((b!1 - a!1) / pd!1)) = 0
  |-------
{1}   (b!1 - a!1) / pd!1 > 0

Rule?  (MULT-BY 1 "pd!1") 

[-1]  b!1 > a!1
{-2}  (1 + floor((b!1 - a!1) / pd!1)) = 0
  |-------
{1}   (b!1 - a!1) > 0 * pd!1

Rule? (ASSERT)

This completes the proof of t61_TCC1.2.

Q.E.D.

EXAMPLE 7

[-1]  (abs(x!1) + 5) * (abs(x!1) - 2) = 0
  |-------
[1]   x!1 = 2
[2]   x!1 = -2

Rule?  (MULT-CASES -1) 

{-1}  (abs(x!1) - 2) = 0
  |-------
[1]   x!1 = 2
[2]   x!1 = -2

Rule? (grind)
This completes the proof of t3.1.

EXAMPLE 8

[-1]  30 + 9 * y!1 = 4 - 2 * n!1 * y!1
  |-------
[1]   y!1 = -26 / (9 + 2 * n!1)

Rule?  (mult-by 1 (! 1 R 2)) 

[-1]  30 + 9 * y!1 = 4 - 2 * n!1 * y!1
  |-------
{1}   (y!1 * (9 + 2 * n!1) = -26)

Rule? (assert)
This completes the proof of t33.1.1.1.

EXAMPLE 9

{-1}  2 * x!1 - 3 * y!1 = 10
{-2}  3 * x!1 + n!1 * y!1 = 2
  |-------
{1}   y!1 = -26 / (9 + 2 * n!1)

Rule?  (mult-by -1 "3") 

{-1}  (2 * x!1 - 3 * y!1) * 3 = 10 * 3
[-2]  3 * x!1 + n!1 * y!1 = 2
  |-------
[1]   y!1 = -26 / (9 + 2 * n!1)

Rule?  (mult-by -2 "2") 
{-1}  (3 * x!1 + n!1 * y!1) * 2 = 2 * 2
[-2]  (2 * x!1 - 3 * y!1) * 3 = 10 * 3
  |-------
[1]   y!1 = -26 / (9 + 2 * n!1)

Rule?  (MULT-BY 1 (! 1 R 2)) 

[-1]  (3 * x!1 + n!1 * y!1) * 2 = 2 * 2
[-2]  (2 * x!1 - 3 * y!1) * 3 = 10 * 3
  |-------
{1}   (y!1 * (9 + 2 * n!1) = -26)

Rule? (assert)
Q.E.D.

EXAMPLE 10

  |-------
[1]   (b!1 * ii!1 - a!1 * ii!1) / (N!1 - 1) + a!1 <= b!1

Rule?  (MOVE-TERMS 1 L 2) 

  |-------
{1}   ((b!1 * ii!1 - a!1 * ii!1) / (N!1 - 1) <= b!1 - a!1)

Rule?  (MULT-BY * "N!1-1") 

  |-------
{1}   (b!1 * ii!1 - a!1 * ii!1) <= (b!1 - a!1) * (N!1 - 1)

Rule?  (FACTOR 1 L) 

  |-------
{1}   ii!1 * (b!1 - a!1) <= (b!1 - a!1) * (N!1 - 1)

Rule? (TYPEPRED "ii!1")

{-1}  ii!1 < N!1
  |-------
[1]   ii!1 * (b!1 - a!1) <= (b!1 - a!1) * (N!1 - 1)

Rule?  (DIV-BY 1 "(b!1-a!1)")  (ASSERT)

This completes the proof of eq_partition_TCC2.1.2.1.

EXAMPLE 11

{-1}  a!1 >= 0
{-2}  b!1 >= 0
{-3}  c!1 >= 0
  |-------
{1}   a!1 + (a!1 + b!1 + c!1) / (x!1 * x!1 + 1) >= 0

Rule?  (HAS-SIGN (! 1 L 2) 0+) 
this yields  2 subgoals: 
t11.1 :  

{-1}  (a!1 + b!1 + c!1) / (x!1 * x!1 + 1) >= 0
[-2]  a!1 >= 0
[-3]  b!1 >= 0
[-4]  c!1 >= 0
  |-------
[1]   a!1 + (a!1 + b!1 + c!1) / (x!1 * x!1 + 1) >= 0

Rule? (ASSERT)
This completes the proof of t11.1.

t11.2 :  

[-1]  a!1 >= 0
[-2]  b!1 >= 0
[-3]  c!1 >= 0
  |-------
{1}   (a!1 + b!1 + c!1) / (x!1 * x!1 + 1) >= 0
[2]   a!1 + (a!1 + b!1 + c!1) / (x!1 * x!1 + 1) >= 0

Rule?  (CROSS-MULT 1) 

This completes the proof of t11.2.

EXAMPLE 12

[-1]  x!1 > 1
[-2]  P!1(sqrt(sq(x!1) - 1) / sqrt(x!1 - 1))
  |-------
[1]   P!1(sqrt(x!1 + 1))

Rule?  (invoke (case-replace "%1 = sqrt(x!1+1)") (? -2 "P!1(%1)")) 

[-1]  x!1 > 1
[-2]  P!1(sqrt(sq(x!1) - 1) / sqrt(x!1 - 1))
  |-------
{1}   sqrt(sq(x!1) - 1) / sqrt(x!1 - 1) = sqrt(x!1 + 1)
[2]   P!1(sqrt(x!1 + 1))

EXAMPLE 13

{-1}  px!1 * px!1 > pa!1 * pa!1
  |-------
{1}   px!1 > pa!1

Rule?  (mult-ineq 1 1) 

{-1}  px!1 * px!1 <= pa!1 * pa!1
[-2]  px!1 * px!1 > pa!1 * pa!1
  |-------
[1]   px!1 > pa!1

Rule? (assert)
Q.E.D.

EXAMPLE 14

[-1]  x!1 > y!1 * pa!1
{-2}  y!1 * pa!1 > pa!1 * pb!1 * z!1
[-3]  z!1 > 0
  |-------
[1]   x!1 > 0

Rule?  (HAS-SIGN (! -2 R) +) 

{-1}  pa!1 * pb!1 * z!1 > 0
[-2]  x!1 > y!1 * pa!1
[-3]  y!1 * pa!1 > pa!1 * pb!1 * z!1
[-4]  z!1 > 0
  |-------
[1]   x!1 > 0

EXAMPLE 15

t57 :  

{-1}  a!1 > 1
{-2}  b!1 > 1
{-3}  a!1 > b!1
  |-------
{1}   1 + (a!1 - 1) / floor((a!1 - 1) / (b!1 - 1)) >= b!1

Rule?  (claim "%1 > 0" nil (! 1 (-> "floor"))) 

this yields  3 subgoals: 
t57.1 :  

{-1}  floor((a!1 - 1) / (b!1 - 1)) > 0
[-2]  a!1 > 1
[-3]  b!1 > 1
[-4]  a!1 > b!1
  |-------
[1]   1 + (a!1 - 1) / floor((a!1 - 1) / (b!1 - 1)) >= b!1

Rule?  (MOVE-TERMS 1 L 1) 

this yields  3 subgoals: 
t57.1.1 :  

[-1]  floor((a!1 - 1) / (b!1 - 1)) > 0
[-2]  a!1 > 1
[-3]  b!1 > 1
[-4]  a!1 > b!1
  |-------
{1}   ((a!1 - 1) / floor((a!1 - 1) / (b!1 - 1)) >= b!1 - 1)

Rule?  (MULT-BY 1 (! 1 (-> "floor"))) 

{-1}  floor((a!1 - 1) / (b!1 - 1)) > 0
[-2]  a!1 > 1
[-3]  b!1 > 1
[-4]  a!1 > b!1
  |-------
{1}   (a!1 - 1) >= (b!1 - 1) * floor((a!1 - 1) / (b!1 - 1))

Rule?  (DIV-BY 1 "b!1-1") 

[-1]  floor((a!1 - 1) / (b!1 - 1)) > 0
[-2]  a!1 > 1
[-3]  b!1 > 1
[-4]  a!1 > b!1
  |-------
{1}   (a!1 - 1) / (b!1 - 1) >=
       (b!1 - 1) * floor((a!1 - 1) / (b!1 - 1)) / (b!1 - 1)

Rule? (NAME-REPLACE "bp" "b!1-1")

{-1}  floor((a!1 - 1) / bp) > 0
[-2]  a!1 > 1
[-3]  b!1 > 1
[-4]  a!1 > b!1
  |-------
{1}   (a!1 - 1) / bp >= bp * floor((a!1 - 1) / bp) / bp

Rule? (ASSERT)
t57.1.2 (TCC):   

[-1]  floor((a!1 - 1) / (b!1 - 1)) > 0
[-2]  a!1 > 1
[-3]  b!1 > 1
[-4]  a!1 > b!1
  |-------
{1}   floor((a!1 - 1) / (b!1 - 1)) /= 0
[2]   1 + (a!1 - 1) / floor((a!1 - 1) / (b!1 - 1)) >= b!1

Rule? (ASSERT)
This completes the proof of t57.1.2.

t57.1.3 (TCC):   

[-1]  floor((a!1 - 1) / (b!1 - 1)) > 0
[-2]  a!1 > 1
[-3]  b!1 > 1
[-4]  a!1 > b!1
  |-------
{1}   (b!1 - 1) /= 0
[2]   1 + (a!1 - 1) / floor((a!1 - 1) / (b!1 - 1)) >= b!1

Rule? (ASSERT)

This completes the proof of t57.1.3.
This completes the proof of t57.1.

t57.2 :  

[-1]  a!1 > 1
[-2]  b!1 > 1
[-3]  a!1 > b!1
  |-------
{1}   floor((a!1 - 1) / (b!1 - 1)) > 0
[2]   1 + (a!1 - 1) / floor((a!1 - 1) / (b!1 - 1)) >= b!1

Rule? (HIDE 2)

[-1]  a!1 > 1
[-2]  b!1 > 1
[-3]  a!1 > b!1
  |-------
[1]   floor((a!1 - 1) / (b!1 - 1)) > 0

Rule?  (INVOKE (CASE "%1 > 1") (! 1 (-> "floor") 1)) 
this yields  3 subgoals: 
t57.2.1 :  

{-1}  (a!1 - 1) / (b!1 - 1) > 1
[-2]  a!1 > 1
[-3]  b!1 > 1
[-4]  a!1 > b!1
  |-------
[1]   floor((a!1 - 1) / (b!1 - 1)) > 0

Rule? (ASSERT)
Simplifying, rewriting, and recording with decision procedures,

This completes the proof of t57.2.1.

t57.2.2 :  

[-1]  a!1 > 1
[-2]  b!1 > 1
[-3]  a!1 > b!1
  |-------
{1}   (a!1 - 1) / (b!1 - 1) > 1
[2]   floor((a!1 - 1) / (b!1 - 1)) > 0

Rule? (HIDE 2)

[-1]  a!1 > 1
[-2]  b!1 > 1
[-3]  a!1 > b!1
  |-------
[1]   (a!1 - 1) / (b!1 - 1) > 1

Rule?  (MULT-BY 1 "b!1-1") 

[-1]  a!1 > 1
[-2]  b!1 > 1
[-3]  a!1 > b!1
  |-------
{1}   (a!1 - 1) > 1 * (b!1 - 1)

Rule? (ASSERT)

This completes the proof of t57.2.2.

t57.2.3 (TCC):   

[-1]  a!1 > 1
[-2]  b!1 > 1
[-3]  a!1 > b!1
  |-------
{1}   (b!1 - 1) /= 0
[2]   floor((a!1 - 1) / (b!1 - 1)) > 0

Rule? (ASSERT)

This completes the proof of t57.2.3.
This completes the proof of t57.2.

t57.3 (TCC):   

[-1]  a!1 > 1
[-2]  b!1 > 1
[-3]  a!1 > b!1
  |-------
{1}   (b!1 - 1) /= 0
[2]   1 + (a!1 - 1) / floor((a!1 - 1) / (b!1 - 1)) >= b!1

Rule? (ASSERT)
Simplifying, rewriting, and recording with decision procedures,

This completes the proof of t57.3.

Q.E.D.

Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 27 February 2002 (10:27:18)