diff --git a/arith.modal b/arith.modal index 96d91e5..def6e92 100644 --- a/arith.modal +++ b/arith.modal @@ -331,7 +331,7 @@ <> ((pow (Z (- ?x)) (N (0 ?k)))) ((nat>pos (pow (N ?x) (N (0 ?k))))) <> ((pow (Z (- ?x)) (N (1 ?k)))) ((nat>neg (pow (N ?x) (N (1 ?k))))) --- ( to natural number ) +-- ( to integer ) <> ((int ?*)) ((int1 (?*))) <> ((int1 (- ?t))) ((int2 - (nat1 ?t))) <> ((int1 (?h ?t))) ((int2 + (nat1 (?h ?t)))) @@ -375,4 +375,15 @@ <> ((div (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((mul (Q (?s ?x ?d)) (Q (?t ?e ?y)))) -(str (mul (Q (+ sixteen ten)) (Q (- sixteen ten)))) +<> ((pow (Q (?s ?x ?d)) (N ?k))) ((qpow (pow (Z (?s ?x)) (N ?k)) (pow (N ?d) (N ?k)))) +<> ((qpow (Z (?s ?n)) (N ?d))) ((ratify ?s (N ?n) (N ?d))) + +-- ( to rational number ) +<> ((rat ?*)) ((rat1 (?*))) +<> ((rat1 (- ?t))) ((rat2 - ?t ())) +<> ((rat1 (?h ?t))) ((rat2 + (?h ?t) ())) +<> ((rat2 ?s (/ ?t) ?a)) ((rat3 ?s (nat1 reverse ?a) (nat1 ?t))) +<> ((rat2 ?s (?h ?t) ?a)) ((rat2 ?s ?t (?h ?a))) +<> ((rat3 ?s (N ?n) (N ?d))) ((Q (?s ?n ?d))) + +(str (pow (rat -2/7) (nat 3)))