关于伊莎贝尔的引理证明的一些问题
我已经定义了一个引理，例如“ a ==＆gt; b ==＆gt; c”，并尝试使用nitpick，并且给出了反例，我看到了a = false，b = false和c = false的结果。
我只想知道，当A和B持有A时，如何给引理，然后C持有。
lemma "LTS_is_reachable (Δ (reg2nfa r1 v)) [] x y ⟹
y ∈ ℱ (reg2nfa r1 v) ⟹
LTS_is_reachable (Δ (reg2nfa r1 v)) [] y x"
nitpick
Nitpicking formula...
Nitpick found a potentially spurious counterexample for card 'a = 1:
Free variables:
r1 = LChr a⇩1?
v = {a⇩1}
x = [a⇩1]
y = []
lemma "LTS_is_reachable (Δ (reg2nfa (LChr a1) {a1})) [] [a1] [] == False"
by auto
lemma "[] \<in> ℱ (reg2nfa (LChr a1) {a1}) == False"
by auto
lemma "LTS_is_reachable (Δ (reg2nfa (LChr a⇩1) {a⇩1})) [] [] [a⇩1] == False"
by auto
I have defined a lemma like "A ==> B ==>C" and try to use the nitpick, and it give the counterexample, I see the result of A = False , B = False, and C = False.
I just wanna know that how to give a lemma when A and B holds, then C holds.
lemma "LTS_is_reachable (Δ (reg2nfa r1 v)) [] x y ⟹
y ∈ ℱ (reg2nfa r1 v) ⟹
LTS_is_reachable (Δ (reg2nfa r1 v)) [] y x"
nitpick
Nitpicking formula...
Nitpick found a potentially spurious counterexample for card 'a = 1:
Free variables:
r1 = LChr a⇩1?
v = {a⇩1}
x = [a⇩1]
y = []
lemma "LTS_is_reachable (Δ (reg2nfa (LChr a1) {a1})) [] [a1] [] == False"
by auto
lemma "[] \<in> ℱ (reg2nfa (LChr a1) {a1}) == False"
by auto
lemma "LTS_is_reachable (Δ (reg2nfa (LChr a⇩1) {a⇩1})) [] [] [a⇩1] == False"
by auto
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
当Nitpick表示其结果“可能是虚假的”时，这可能是错误的。就在这里。
When nitpick says its result is "potentially spurious", that means it might be wrong. And so it is here.