; to_clause_1 : forall a b : Prop, ((a -> b) -> (a -> ~b -> False)).
; to_clause_2 : forall a b : Prop, ((a -> b) -> (~b -> a -> False)).
; to_clause_1_sn : forall a b : Prop, ((a -> ~b) -> (a -> b -> False)).
; to_clause_2_sn : forall a b : Prop, ((a -> ~b) -> (b -> a -> False)).
; absurd_n : forall a : Prop, (~a -> False) -> a.
; absurd_p : forall a : Prop, (a -> False) -> ~a.
; and_get : forall a b : Prop, a /\ b -> a.
; and_skip : forall a b : Prop, a /\ b -> b.
; nor_get : forall a b : Prop, ~(a \/ b) -> ~a.
; nor_skip : forall a b : Prop, ~(a \/ b) -> ~b.
; neg_unit_res : forall a b : Prop, a -> ~(a /\ b) -> ~b.
; excl_mid_pn : forall a : Prop, a -> ~a -> False.
; excl_mid_np : forall a : Prop, ~a -> a -> False.
; unit_res_pn : forall a b : Prop, a -> (~ a \/ b) -> b.
; unit_res_np : forall a b : Prop, ~a -> (a \/ b) -> b.
; compose : forall a b c : Prop, (b -> c) -> (a -> b) -> (a -> c).
;
;(* NNF *)
; neg_iff_def : forall a b : Prop, ~(a <-> b) -> ~((~ a \/ b) /\ (~ b \/ a)).
; pos_implies_def : forall a b : Prop, (a -> b) -> (~ a \/ b).
; neg_implies_def : forall a b : Prop, ~(a -> b) -> ~(~ a \/ b).
; neg_and_comp : forall a a' b b' : Prop, (~a -> a') -> (~b -> b') -> (~(a /\ b) -> a' \/ b').
; pos_or_comp : forall a a' b b' : Prop, (a -> a') -> (b -> b') -> (a \/ b -> a' \/ b').
; or_comm : forall a b c d : Prop, ((b \/ c) -> d) -> (a \/ b) \/ c -> a \/ d.
; nnpp : forall a : Prop, (~ (~ a)) -> a.

(rule
  (initial SK F)
  (known (skol %NIL SK F)))

; If (skol Q P A) rewrites to B then for any model M, M |= A there exists M', such that M' |= B,
; and vice versa.

; id : forall a : Prop, a -> a.
(rule 
  (skol Q id A) 
  A)

; pos_iff_def : forall a b : Prop, (a <-> b) -> ((~ a \/ b) /\ (~ b \/ a)).
(rule
  (skol Q pos_iff_def (iff A B))  
  (and (or (not A) B) (or (not B) A)))

; pos_and_comp : forall a a' b b' : Prop, (a -> a') -> (b -> b') -> (a /\ b -> a' /\ b').
(rule
  (skol Q (pos_and_comp X Y) (and A B))
  (and (skol Q X A) (skol Q Y B)))

; neg_or_comp : forall a a' b b' : Prop, (~a -> a') -> (~b -> b') -> (~(a \/ b) -> a' /\ b').
(rule
  (skol Q (neg_or_comp X Y) (not (or A B)))
  (and (skol Q X (not A)) (skol Q Y (not B))))

; and_comm : forall a b c d : Prop, ((b /\ c) -> d) -> (a /\ b) /\ c -> a /\ d.
(rule
  (skol Q (and_comm X) (and (and A B) C))
  (and A (skol Q X (and B C))))

; compose : forall a b c : Prop, (b -> c) -> (a -> b) -> (a -> c).
(rule
  (skol Q (compose X Y) A)
  (skol Q X (skol Q Y A)))

(rule
  (skol Q (skolemize F) (exists P))
  (%BETA P (%SKOL F Q)))

(rule
  (skol Q (skip_forall R) (forall P))
  (forall (\ x (skol (%CONS x Q) R (%BETA P x)))))

;---------------------------------

(rule
  (resolution (known (or L A)) (known (or (not L) B)))
  (known (or A B)))

(rule
  (inst T (forall P))
  (known (implies (forall P) (%BETA P T))))

(rule
  (rewrite X (known A))
  (known (rewr X A)))

(rule
  (rewrite_impl X A)
  (known (implies A (rewr X A))))

(rule
  (rewr and_symm (and A B))
  (and B A))

(rule
  (rewr andl (and A B))
  A)

(rule
  (rewr andr (and A B))
  B)

(rule
  (rewr impl_def (implies A B))
  (or (not A) B))

; ---------------------

(let b0 (rewr andl (and a b)))
(assert_eq b0 a)

(let b1a (skol nil (skip_forall id) (forall (\ x (iff (f x) (g y))))))
(assert_eq b1a (forall (\ A (iff (f A) (g y)))))

(let b1 (skol nil (skip_forall pos_iff_def) (forall (\ x (iff (f x) (g y))))))
(assert_eq b1 (forall (\ A (and (or (not (f A)) (g y)) (or (not (g y)) (f A))))))

(let b2 (skol nil (skip_forall (skip_forall pos_iff_def)) (forall (\ y (forall (\ x (iff (f x) (g y))))))))
(assert_eq b2 (forall (\ A (forall (\ B (and (or (not (f B)) (g A)) (or (not (g A)) (f B))))))))

(let b3 (foo b2))
(assert_eq b3 (foo (forall (\ A (forall (\ B (and (or (not (f B)) (g A)) (or (not (g A)) (f B)))))))))



(let cf1 (%CONSTANT_FOLD (+ 40 2)))
(assert_eq cf1 42)

(let cf2 (%CONSTANT_FOLD (- 47 5)))
(assert_eq cf2 42)

(let cf3 (%CONSTANT_FOLD (+ (%CONSTANT_FOLD (- 47 7)) 2)))
(assert_eq cf3 42)

(let cf4 (%CONSTANT_FOLD (~ (%CONSTANT_FOLD (- 47 7)))))
(assert_eq cf4 -40)

(let cf5 (%CONSTANT_FOLD (- 0 x)))
(assert_eq cf5 (~ x))

(let cf6 (%CONSTANT_FOLD (- x 0)))
(assert_eq cf6 x)

(let cf7 (%CONSTANT_FOLD (+ x 0)))
(assert_eq cf7 x)

(let cf8 (%CONSTANT_FOLD (+ 0 x)))
(assert_eq cf8 x)

quit