(defstep skolem-inst-strat ()
  (then (auto-rewrite-defs :always? t)
		(repeat* (then (assert)(skolem!)(inst?)(bddsimp)))
		(grind))
   "Trying repeated skolemization and instantioation" "")

(defstep unptcc3 ()
  (then (flatten)
		(expand* "SIGSIZE" "EXPSIZE")
		(assert)
        (reveal 1 2 3 4 5 6 7 8 9)
		(use "unpack_TCC3")
		(expand "unpack_top_impl")
		(assert))
  "Strategie for TCCs" "")

(defstep unptcc4 ()
  (then (flatten)
		(expand* "SIGSIZE" "EXPSIZE")
		(assert)
        (reveal 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20)
		(use "unpack_TCC4")
		(expand "unpack_top_impl")
		(assert))
  "Strategie for TCCs" "")

(defstep do-with-tcc (str1 str2)
  (try (quote str1)
	   (try (then (quote str2) (fail)) (fail) (assert)) 
	   (postpone)) 
  "Case with unptcc3 afterwards" "")

(defstep sigexp ()
 (then 
 (branch (case "SIGSIZE[32]=24")
		((then (replace -1 * :actuals? T)
        	  (delete -1) 
			  (assert)) (expand* "SIGSIZE" "EXPSIZE")))
(branch (case "EXPSIZE[32]=8")
		((then (replace -1 * :actuals? T)
        	  (delete -1) 
			  (assert))(expand* "SIGSIZE" "EXPSIZE")))
(branch (case "SIGSIZE[64]=53")
		((then (replace -1 * :actuals? T)
        	  (delete -1) 
			  (assert)) (expand* "SIGSIZE" "EXPSIZE")))
(branch (case "EXPSIZE[64]=11")
		((then (replace -1 * :actuals? T)
        	  (delete -1) 
			  (assert)) (expand* "SIGSIZE" "EXPSIZE")) ))
   "SIGS" "")


(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 exp2-const ()
 (then 
  (repeat (rewrite "exp2_def"))
  (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_11")
  (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_1024")
  (rewrite "exp2_1536")
  (rewrite "exp2_512")
  (rewrite "exp2_128")
  (rewrite "exp2_192")
  (rewrite "exp2_320")
  (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-hide (step)
 (spread
  (case-replace step)
  ((hide -1))
 )
 "do (case-replace <step> :hide? t)"
 "case-replacing ~a"
)

(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 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-grind (step)
 (spread!
  (case-replace step)
  ((hide -1)
   (then
    (hide-all-but 1)
    (grind)
   )
  )
 )
 "do (case-replace <step> :hide? t) and (grind) the case"
 "case-replacing ~a"
)

(defstep first (command first)
 (spread!
  (quote command)
  ((quote first) (skip))
 )
 ""
 "Using ~a and resolving this with ~a"
)

(defstep second (command second)
 (spread!
  (quote command)
  ((skip) (quote second))
 )
 ""
 "Using ~a and resolving the other case with ~a"
)



(defstep log2-strat-ns ()
  (then (rewrite "log2_ineq3")
		(rewrite "log2_mul2expt")
		(rewrite "log2_mul2expt")
		(rewrite "log2_mul2expt")
		(rewrite "log2_mul2expt")
		(rewrite "log2_exp2")
		(assert)) "" "")

(defstep bv-const ()
 (then
  (repeat (rewrite "b2n_fill_caret"))
  (rewrite "b2n_F")
  (rewrite "b2n_T")
  (rewrite "b2sign_F")
  (rewrite "b2sign_T")
  (repeat (rewrite "bv2nat_fill_F"))
  (repeat (rewrite "bv2nat_fill_T"))
  (repeat (rewrite "bv2int_fill_F"))
  (repeat (rewrite "bv2int_fill_T"))
  (assert)
 )
 ""
 "Replacing various instances of bv2int(fill()), b2n() and b2sign()"
)

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