#1: " ----------[ D e r i v e ]---------- " User #2: " ---------- Initialization ---------- " User #3: " ----------- Inequalities ----------- " User #4: " => True " User pi #e #5: #e > pi User #6: true Simp(#5) #7: " => [True, False] " User / 4 4 \ #8: \x - x + 1 > 0, x - x + 1 > 1/ User / 4 4 \ #9: \x - x + 1 > 0, x - x + 1 > 1/ Simp(#8) #10: BOOL(x) := IF(x, true, false, "unknown") User / 4 4 \ #11: \BOOL(x - x + 1 > 0), BOOL(x - x + 1 > 1)/ User #12: ["unknown", "unknown"] Simp(#11) #13: " x > y > 0 and k, n > 0 => k x^n > k y^n " User #14: " => True " User #15: "ABS(x) :epsilon Real [0, 1)" User #16: BOOL(-1 < x AND x < 1) User #17: "unknown" Simp(#16) #18: x := User #19: "assume(x > y)" User #20: y :epsilon Real (0, inf) User #21: y Simp(#20) 2 2 #22: 2*x > 2*y User 2 2 #23: 2*x > 2*y Simp(#22) #24: k :epsilon Real (0, inf) User #25: k Simp(#24) 2 2 #26: k*x > k*y User 2 2 #27: k*x > k*y Simp(#26) #28: n :epsilon Real (0, inf) User #29: n Simp(#28) n n #30: k*x > k*y User n n #31: k*x > k*y Simp(#30) #32: x := User #33: y := User #34: k := User #35: n := User #36: " x > 1 and y >= x - 1 => y > 0 " User #37: x :epsilon (1, inf) User #38: x Simp(#37) #39: "assume(y >= x - 1)" User #40: y > 0 User #41: y > 0 Simp(#40) #42: x := User #43: y := User #44: " x >= y, y >= z, z >= x => x = y = z " User #45: "assume(x >= y, y >= z, z >= x)" User #46: [x = y, x = z, y = z] User #47: [x = y, x = z, y = z] Simp(#46) #48: x := User #49: y := User #50: z := User #51: " x < -1 or x > 3 " User #52: SOLVE(|x - 1| > 2, x) User #53: [x < -1, x > 3] Simp(#52) #54: " x < 1 or 2 < x < 3 or 4 < x < 5 " User #55: SOLVE((x - 1)*(x - 2)*(x - 3)*(x - 4)*(x - 5) < 0, x) User #56: [x < 1, 2 < x < 3, 4 < x < 5] Simp(#55) #57: " x < 3 or x >= 5 " User / 6 \ #58: SOLVE|------- <= 3, x| User \ x - 3 / #59: [x < 3, x > 5] Simp(#58) #60: " => 0 <= x < 4 " User #61: SOLVE(SQRT(x) < 2, x) User #62: [0 < x < 4] Simp(#61) #63: " => x is real " User #64: SOLVE(SIN(x) < 2, x) User #65: [x = @1] Simp(#64) #66: " => x != pi/2 + n 2 pi " User #67: SOLVE(SIN(x) < 1, x) User #68: [SIN(x) < 1] Simp(#67) User #69: " The next two examples come from Abdubrahim Muhammad Farhat, _Stability " User #70: " Analysis of Finite Difference Schemes_, Ph.D. dissertation, University of " User #71: " New Mexico, Albuquerque, New Mexico, December 1993 => 0 <= A <= 1/2 " #72: SOLVE(|2*a*(COS(t) - 1) + 1| <= 1, a) User #73: [-1 <= 2*a*COS(t) - 2*a + 1 <= 1] Simp(#72) #74: c :epsilon [-1, 1] User #75: c Simp(#74) #76: SOLVE(|2*a*(c - 1) + 1| <= 1, a) User #77: [-1 <= 2*a*(c - 1) + 1 <= 1] Simp(#76) User #78: " => 125 A^4 + 24 A^2 - 48 < 0 or |A| < 2/5 sqrt([8 sqrt(6) - 3]/5) " 2 2 2 #79: SOLVE(a *(COS(t) - 4) *SIN(t) < 9, a) User Simp(#79) / 3 3 \ #80: |----------------------- < a < -----------------------| \ |SIN(t)|*(COS(t) - 4) |SIN(t)|*(4 - COS(t)) / #81: s :epsilon [-1, 1] User #82: s Simp(#81) 2 2 2 #83: SOLVE(a *(c - 4) *s < 9, a) User / 3 3 \ #84: |------------- < a < -------------| Simp(#83) \ (c - 4)*|s| (4 - c)*|s| / #85: c := User #86: s := User #87: " => |x| < y " User #88: SOLVE([x + y > 0, x - y < 0], [x, y]) User #89: [] Simp(#88) #90: " ---------- Quit ---------- " User