1 files changed, 56 insertions, 56 deletions
diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf
index 02cadaeab..ae585e455 100755
--- a/proofs/signatures/ex_bv.plf
+++ b/proofs/signatures/ex_bv.plf
@@ -1,57 +1,57 @@
-; a = b ^ a = 00000 ^ b = 11111 is UNSAT
-
-(check
-(% a var_bv
-(% b var_bv
-(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))
-(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))
-(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
-(: (holds cln)
-
-(decl_bv_atom_var 5 a (\ ba1
-(decl_bv_atom_var 5 b (\ ba2
-(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
-(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4
-
-(decl_atom (bblast a 4) (\ v1 (\ a1
-(decl_atom (bblast b 4) (\ v2 (\ a2
-
-; bitblasting terms
-(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1
-(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2
-(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3
-(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4
-
-; bitblasting formulas
-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1
-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2
-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3
-
-; CNFication
-; a.4 V ~b.4
-(satlem _ _
-(asf _ _ _ a1 (\ l1
-(ast _ _ _ a2 (\ l2
-(clausify_false
-  (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1)   ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation
-))))) (\ C2
-
-; ~a.4
-(satlem _ _
-(ast _ _ _ a1 (\ l1
-(clausify_false
-  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))
-))) (\ C3
-
-; b.4 
-(satlem _ _
-(asf _ _ _ a2 (\ l2
-(clausify_false
-  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)
-))) (\ C6
-
-
-(satlem_simplify _ _ _ 
-(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
-
+; a = b ^ a = 00000 ^ b = 11111 is UNSAT
+
+(check
+(% a var_bv
+(% b var_bv
+(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))
+(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))
+(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
+(: (holds cln)
+
+(decl_bv_atom_var 5 a (\ ba1
+(decl_bv_atom_var 5 b (\ ba2
+(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
+(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4
+
+(decl_atom (bblast a 4) (\ v1 (\ a1
+(decl_atom (bblast b 4) (\ v2 (\ a2
+
+; bitblasting terms
+(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1
+(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4
+
+; bitblasting formulas
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3
+
+; CNFication
+; a.4 V ~b.4
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(clausify_false
+  (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1)   ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation
+))))) (\ C2
+
+; ~a.4
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(clausify_false
+  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))
+))) (\ C3
+
+; b.4 
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)
+))) (\ C6
+
+
+(satlem_simplify _ _ _ 
+(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
+
 )))))))))))))))))))))))))))))))))))))))))))
 \ No newline at end of file