proofs/signatures/th_bv_rewrites.plf


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

;
; Equality swap
;

(declare rr_bv_eq
	 (! n mpz
	 (! t1 (term (BitVec n))
 	 (! t2 (term (BitVec n))
	     (th_holds (iff (= (BitVec n) t2 t1) (= (BitVec n) t1 t2)))))))

;
; Additional rules...
;

;
; Default, if nothing else applied
;

(declare rr_bv_default
	 (! t1 formula
 	 (! t2 formula
	     (th_holds (iff t1 t2))))))