(defstep exp2-strat ()
    (repeat (then (use "expt_plus")
		  (replace -)
		  (delete -1)
		  (assert)

          (use "expt_inverse")
		  (replace -)
		  (delete -1)
		  (assert)

          (use "expt_x1")
		  (replace -)
		  (delete -1)
		  (assert)

          (use "expt_x0")
		  (replace -)
		  (delete -1)
		  (assert)

          (use "expt_div")
		  (replace - :dir RL)
		  (delete -1)
		  (assert)
    ))
  "Prove simple equalities with 2^..."
  "")


(defstep exp2-strat-neu ()
    (repeat (then (rewrite "exp2_def")
				  (rewrite "expt_inverse")
				  (rewrite "expt_plus")
				  (rewrite "expt_div" :dir RL)
				  (rewrite "expt_x1")
				  (rewrite "expt_x0")
				  (assert)))
	"Prove simple ...."
"")
 
(defstep exp2 ()
 (repeat (then 
	  (rewrite "exp2_def")
	  (rewrite "expt_inverse")
	  (rewrite "expt_plus")
	  (rewrite "expt_div" :dir RL)
	  (rewrite "expt_x1")
	  (rewrite "expt_x0")
	  (assert)))
 "exp2-catch-all-strategy, includes exp2_def expt_inverse expt_plus
 expt_div :dir RL expt_x1 expt_x0 and assert"
 "Rewriting with expt lemmas")


(defstep case-replace-hide-all (step)
 (else
  (spread!
   (case-replace step)
   ((hide -1) (hide-all-but 1))
  )
  (spread!
   (case-replace step)
   ((hide-all-but 1))
  )
 )
 "do (case-replace <step> :hide? t) and (hide-all-but 1) on the second subgoal"
 "case-replacing ~a"
)


(defstep exp2-const ()
 (then 
  (repeat (rewrite "exp2_def"))
  (rewrite "exp2_0")
  (rewrite "exp2_1")
  (rewrite "exp2_2")
  (rewrite "exp2_3")
  (rewrite "exp2_4")
  (rewrite "exp2_5")
  (rewrite "exp2_6")
  (rewrite "exp2_7")
  (rewrite "exp2_8")
  (rewrite "exp2_9")
  (rewrite "exp2_10")
  (rewrite "exp2_13")
  (rewrite "exp2_23")
  (rewrite "exp2_28")
  (rewrite "exp2_29")
  (rewrite "exp2_52")
  (rewrite "exp2_53")
  (rewrite "exp2_54")
  (rewrite "exp2_55")
  (rewrite "exp2_56")
  (rewrite "exp2_57")
  (rewrite "exp2_63")
  (rewrite "exp2_64")
  (rewrite "exp2_71")
  (rewrite "exp2_127")
  (rewrite "exp2_128")
  (assert))
  "Resolves 2^i for various values of i"
  "Using exp2 lemmas"
)


(defstep exp2-const-inverse ()
 (then
  (repeat (rewrite "exp2_def"))
  (repeat (rewrite "expt_inverse"))
  (exp2-const)
 )
 "(exp2-const) plus (rewrite \"expt_inverse\")"
 "Using exp2 lemmas"
)

(defstep case-replace-assert (step)
 (spread!
  (case-replace step)
  ((hide -1) (assert))
 )
 "do (case-replace <step> :hide? t) and (assert) the second subgoal"
 "case-replacing ~a"
)

(defstep case-replace-hide (step)
 (spread
  (case-replace step)
  ((hide -1))
 )
 "do (case-replace <step> :hide? t)"
 "case-replacing ~a"
)

(defstep bveq9 (&optional (fnum -1))
  (then (stop-rewrite)
		(expand* "fill" "o" "^")
		(decompose-equality fnum)
		(inst-cp -1 0)
		(inst-cp -1 1)
		(inst-cp -1 2)
		(inst-cp -1 3)
		(inst-cp -1 4)
		(inst-cp -1 5)
		(inst-cp -1 6)
		(inst-cp -1 7)
		(inst -1 8)
		(expand* "h0" "h1" "h2" "h3" "h4" "h5" "h6" "h7" "h8" "h9" "hA" "hB" "hC" "hD" "hE" "hF")
		(ground))
	"" "")

(defstep fa ()
 (repeat (then (assert) (flatten)))
 ""
 "Repeating assert/flatten"
)


(defstep cr (formula &optional (hide? t) (all nil) (actuals? nil))
 (spread
  (case formula)
  ((replace -1 :hide? hide? :actuals? actuals?)
   (if all (hide-all-but 1) (skip))
  )
 )
 "Identical to (case-replace), with further arguments :hide? and :all. The latter will invoke (hide-all
-but 1) on the second subgoal."
 "~%Assuming and applying ~a"
)