From ca89676e63717ebd5ab5b22dc9b8740af9021558 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 12 Mar 2022 19:31:56 -0600 Subject: [PATCH] Minor sync from proof-new (#8293) --- proofs/lfsc/signatures/boolean_rules.plf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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))))))) -- 2.30.2