From: Denis Nikiforov <denis.nikif@gmail.com>
Hi
Here is the lemma:
lemma list_all2_rtrancl2_example:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧⇧ xs ys ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧⇧ xs ys"
nitpick
Nitpick outputs the following:
Nitpicking formula...
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
Nitpick found a counterexample:
Free variables:
xs = [0]
ys = [2]
It's easy to show that the counterexample is wrong:
lemma list_all2_rtrancl2_example_0_2:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧⇧ [0] [2] ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧⇧ [0] [2]"
apply (rule_tac ?b="[1]" in converse_rtranclp_into_rtranclp; simp)
apply (rule_tac ?b="[2]" in converse_rtranclp_into_rtranclp; simp)
done
From: Denis Nikiforov <denis.nikif@gmail.com>
Hi
Here is the lemma:
lemma list_all2_rtrancl2_example:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧⇧ xs ys ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧⇧ xs ys"
nitpick
Nitpick outputs the following:
Nitpicking formula...
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
Nitpick found a counterexample:
Free variables:
xs = [0]
ys = [2]
It's easy to show that the counterexample is wrong:
lemma list_all2_rtrancl2_example_0_2:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧⇧ [0] [2] ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧⇧ [0] [2]"
apply (rule_tac ?b="[1]" in converse_rtranclp_into_rtranclp; simp)
apply (rule_tac ?b="[2]" in converse_rtranclp_into_rtranclp; simp)
done
Last updated: Nov 21 2024 at 12:39 UTC