From 63727d887722101dacbc08593c3959c1448da73d Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 21 Aug 2024 13:15:54 +0200 Subject: [PATCH] lemma corrections --- test/kontrol/lido-lemmas.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k index 864862f3..ec70db3f 100644 --- a/test/kontrol/lido-lemmas.k +++ b/test/kontrol/lido-lemmas.k @@ -46,8 +46,8 @@ module LIDO-LEMMAS rule A *Int B => B *Int A [simplification(30), symbolic(A), concrete(B)] // /Int - rule 0 /Int B => 0 requires B =/=Int 0 [simplification, preserves-definedness] - rule A /Int B ==Int 0 => A ==Int 0 requires B =/=Int 0 [simplification, preserves-definedness] + rule 0 /Int B => 0 requires B =/=Int 0 [simplification, preserves-definedness] + rule A /Int B ==Int 0 => A ( A /Int C ) *Int B requires A modInt C ==Int 0 [simplification, concrete(A, C), preserves-definedness]