:forall
((mastate 7) (rf 4 2) (imem 4 7))
((getppc (2) ((mastate 7))
	 (bits mastate 0 1))
 (getewdest (2) ((mastate 7))
	    (bits mastate 2 3))
 (getewresult (2) ((mastate 7))
	      (bits mastate 4 5))
 (getewregwrite (1) ((mastate 7))
		(bits mastate 6 6))
 (src1 (2) ((inst 7))
       (bits inst 5 6))
 (src2 (2) ((inst 7))
       (bits inst 3 4))
 (dest (2) ((inst 7))
       (bits inst 1 2))
 (getregwrite (1) ((inst 7))
	      (bits inst 0 0))
 (nextspc (2) ((pc 2))
	  (bits (+ pc 1u) 0 1))
 (nextsrf (4 2) ((inst 7) (regwrite 1) (rf 4 2) (result 2))
	  (if regwrite
	      (set rf (dest inst) result)
	    rf))
 (step-isa ((2) (4 2) (4 7))
	   ((pc 2) (rf 4 2) (imem 4 7))
	   (local ((inst (get imem pc))
		   (regwrite (getregwrite inst))
		   (arg1 (get rf (src1 inst)))
		   (arg2 (get rf (src2 inst)))
		   (result (bits (+ arg1 arg2) 0 1)))
		  (mv (nextspc pc)
		      (nextsrf inst regwrite rf result)
		      imem)))
 (nextppc (2) ((pc 2)) (bits (+ pc 1u) 0 1))
 (nextprf (4 2) ((rf 4 2) (ewregwrite 1) (ewresult 2) (ewdest 2))
	  (if ewregwrite
	      (set rf ewdest ewresult)
	    rf))
 (step-ma ((7) (4 2) (4 7))
	  ((mastate 7) (rf 4 2) (imem 4 7))
	  (local ((ppc (getppc mastate)) (ewdest (getewdest mastate))
		  (ewregwrite (getewregwrite mastate))
		  (ewresult (getewresult mastate)) (inst (get imem ppc))
		  (arg1_tmp (get rf (src1 inst)))
		  (arg2_tmp (get rf (src2 inst)))
		  (arg1 (if (and ewregwrite (= ewdest (src1 inst)))
			    ewresult
			  arg1_tmp))
		  (arg2 (if (and ewregwrite (= ewdest (src2 inst)))
			    ewresult
			  arg2_tmp))
		  (result (bits (+ arg1 arg2) 0 1)))
		 (mv (cat (getregwrite inst)
			  result
			  (dest inst)
			  (nextppc ppc))
		     (nextprf rf ewregwrite ewresult ewdest)
		     imem)))
 (flush-ma ((7) (4 2) (4 7))
	   ((mastate 7) (rf 4 2) (imem 4 7))
	   (local
	    ((ppc (getppc mastate))
	     (ewdest (getewdest mastate))
	     (ewregwrite (getewregwrite mastate))
	     (ewresult (getewresult mastate))
	     (inst (get imem ppc))
	     (arg1_tmp (get rf (src1 inst)))
	     (arg2_tmp (get rf (src2 inst)))
	     (arg1
	      (if (and ewregwrite (= ewdest (src1 inst)))
		  ewresult
		arg1_tmp))
	     (arg2
	      (if (and ewregwrite (= ewdest (src2 inst)))
		  ewresult
		arg2_tmp))
	     (result (bits (+ arg1 arg2) 0 1)))
	    (mv (cat 1b0 result (dest inst) ppc)
		(nextprf rf ewregwrite ewresult ewdest)
		imem))))
(local (((w1 s-rf s-imem) (flush-ma mastate rf imem)) (s-pc (getppc w1))
	((u-pc u-rf u-imem) (step-isa s-pc s-rf s-imem))
	((v v-rf v-imem) (step-ma mastate rf imem))
	((v1 v1-rf v1-imem) (flush-ma v v-rf v-imem)))
       (and (= (getppc v1) u-pc) (= v1-rf u-rf)))