From 80fad625c54296ad8f0e6f51432c7b498bec9f41 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 8 Feb 2024 15:48:24 -0600 Subject: [PATCH] Removing --- tests/rare-example.smt3 | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/tests/rare-example.smt3 b/tests/rare-example.smt3 index 90d66d28..888c16fe 100644 --- a/tests/rare-example.smt3 +++ b/tests/rare-example.smt3 @@ -10,8 +10,22 @@ (= (or xs true ys) true) ) +(program elim_singleton_list_rhs ((T Type) (f (-> T T T)) (t T) (s T :list)) + ((-> T T T) T) T + ( + ((elim_singleton_list_rhs f (f t s)) (alf.ite (alf.is_eq s (alf.emptylist f)) t (f t s))) + ((elim_singleton_list_rhs f t) t) + ) +)(program elim_singleton_list_lhs ((T Type) (f (-> T T T)) (t T :list) (s T)) + ((-> T T T) T) T + ( + ((elim_singleton_list_lhs f (f t s)) (alf.ite (alf.is_eq t (alf.emptylist f)) s (f t s))) + ((elim_singleton_list_lhs f s) s) + ) +) + (declare-axiom bool-or-false ((xs Bool :list) (ys Bool :list)) - (= (or xs false ys) (alf.from_list or (or xs ys))) + (= (or xs false ys) (elim_singleton_list_rhs or (alf.concat or xs ys))) ) (step @p0 (= (or a b true c) true) :rule bool-or-true :args ((or a b) (or c))) @@ -23,7 +37,7 @@ (step @p5 (= (or (or a b) false) (or a b)) :rule bool-or-false :args ((or (or a b)) false)) (declare-axiom bool-and-true ((xs Bool :list) (ys Bool :list)) - (= (and xs true ys) (alf.from_list and (and xs ys))) + (= (and xs true ys) (elim_singleton_list_lhs and (alf.concat and xs ys))) ) (declare-axiom bool-and-false ((xs Bool :list) (ys Bool :list))