From: Andrew Reynolds Date: Sun, 13 Mar 2022 01:31:56 +0000 (-0600) Subject: Minor sync from proof-new (#8293) X-Git-Tag: cvc5-1.0.0~265 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca89676e63717ebd5ab5b22dc9b8740af9021558;p=cvc5.git Minor sync from proof-new (#8293) --- diff --git a/proofs/lfsc/signatures/boolean_rules.plf b/proofs/lfsc/signatures/boolean_rules.plf index af16af1f9..05a6347ec 100644 --- a/proofs/lfsc/signatures/boolean_rules.plf +++ b/proofs/lfsc/signatures/boolean_rules.plf @@ -49,4 +49,4 @@ ; Process scope, which is used to translate PfRule::SCOPE. It runs the side ; condition sc_process_scope on f to generate an equivalent formula g. -(declare process_scope (! f term (! g term (! c term (! p1 (holds f) (! r (^ (sc_process_scope f c) g) (holds g)))))) +(declare process_scope (! f term (! g term (! c term (! p1 (holds f) (! r (^ (sc_process_scope f c) g) (holds g)))))))