Abduction: fix the bug about the size comparison.

data61 · Aug 28, 2023 · 15453f6 · 15453f6
1 parent c3ef4a5
commit 15453f6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Abduction/Proof_By_Abduction.ML b/Abduction/Proof_By_Abduction.ML
@@ -121,7 +121,7 @@ fun expand_ornode_if_original_goral_is_unproved
                   val size_of_simped_cnjctr = Term.size_of_term (rm_Trueprop simped_cnjctr_term): int;
                   val size_of_orig_cnjctr   = Term.size_of_term (rm_Trueprop cnjctr_term): int;
                 in
-                  if size_of_simped_cnjctr > size_of_orig_cnjctr (*orelse simped_cnjctr_term = @{term True}*)
+                  if size_of_simped_cnjctr >= size_of_orig_cnjctr (*orelse simped_cnjctr_term = @{term True}*)
                      (*orelse rm_Trueprop simped_cnjctr_term = rm_Trueprop lemma_term*)
                   then [cnjctr]
                   else [simp, (simped_cnjctr_name, simped_cnjctr_term)](*TODO: not efficient.*)