Syntax fixes for LFSC signature (#8172)

diff --git a/proofs/lfsc/signatures/arith_rules.plf b/proofs/lfsc/signatures/arith_rules.plf
index 8c134181e4e5805595e0cf3d9d3e2fcbacd305c0..095d3d0bd4bc58c21d539b766addb8615d7d5d06 100644 (file)
--- a/proofs/lfsc/signatures/arith_rules.plf
+++ b/proofs/lfsc/signatures/arith_rules.plf
@@ -94,7 +94,7 @@
 
 ; Returns ok if c2 is the least integer greater than c1. We compute this
 ; via conditions 0 <= c1-c2 ^ (c1-c2)-1 <= 0.
-(program sc_check_int_tight_lb ((t mpq) (c term)) Ok
+(program sc_check_int_tight_lb ((t term) (c term)) Ok
   (mpq_between_zero_one (mp_add (mpz_to_mpq (sc_arith_get_mpz c))
                                 (mp_neg (match t ((int ct) (mpz_to_mpq ct)) ((real ct) ct))))))
 

diff --git a/proofs/lfsc/signatures/cnf_rules.plf b/proofs/lfsc/signatures/cnf_rules.plf
index c593a0a95180c9c48760831190a063e701ad3554..90744e20413ee161dee2ffb4d0c4e71e87b2a4da 100644 (file)
--- a/proofs/lfsc/signatures/cnf_rules.plf
+++ b/proofs/lfsc/signatures/cnf_rules.plf
@@ -20,9 +20,9 @@
 (declare cnf_xor_neg1 (! f1 term (! f2 term (holds (or (xor f1 f2) (or (not f1) (or f2 false)))))))
 (declare cnf_xor_neg2 (! f1 term (! f2 term (holds (or (xor f1 f2) (or f1 (or (not f2) false)))))))
 
-(declare cnf_ite_pos1 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or (not c) (or f1 false)))))))
-(declare cnf_ite_pos2 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or c (or f2 false)))))))
-(declare cnf_ite_pos3 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or f1 (or f2 false)))))))
-(declare cnf_ite_neg1 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not c) (or (not f1) false)))))))
-(declare cnf_ite_neg2 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or c (or (not f2) false)))))))
-(declare cnf_ite_neg3 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not f1) (or (not f2) false)))))))
+(declare cnf_ite_pos1 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or (not c) (or f1 false))))))))
+(declare cnf_ite_pos2 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or c (or f2 false))))))))
+(declare cnf_ite_pos3 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or f1 (or f2 false))))))))
+(declare cnf_ite_neg1 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not c) (or (not f1) false))))))))
+(declare cnf_ite_neg2 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or c (or (not f2) false))))))))
+(declare cnf_ite_neg3 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not f1) (or (not f2) false))))))))

diff --git a/proofs/lfsc/signatures/quantifiers_rules.plf b/proofs/lfsc/signatures/quantifiers_rules.plf
index 7bdd6539cdc9cf6411e1e80e54d8fdac9218624d..6c30ca52355f23be5cd04826015618543b063ea0 100644 (file)
--- a/proofs/lfsc/signatures/quantifiers_rules.plf
+++ b/proofs/lfsc/signatures/quantifiers_rules.plf
@@ -43,7 +43,7 @@
                       (! body term
                       (! p (holds bodyi)
                       (! r (^ (sc_substitute body v s) bodyi)
-                        (holds (exists v u body)))))))))
+                        (holds (exists v u body))))))))))
 
 (declare skolem_intro (! u term
                       (! t term