H: chk r1 r2 (k1 :: k2 :: t)=true H1: r1=k1 H2: r2=k2 IH3: k2::t<> -> chk r1 r2 (k2:: t)=true-> In r1(k2:: t)-> In r2(k2:: t)-> f3 r2(k2:: t)=true-> f4 r2(k2:: t)=true.
Co-existence of above 4 hypothesis is false because H1(r1=k1) & In r1(k2:: t).How i could prove it false?
Plz, some one help me in proving H1 & IH3 are contra statement?
we don´t know was
chk are. How can we help you....
We asked several times for snippets in Coq we could download and replay, not trying to guess missing information.
Yes, you have pointed out many times. But i have represented the functions by f1,f2..just to keep code simple. Secondly,
H1: r1=k1 & In r1(k2:: t) [in IH3] are not possible at a time (point of contradiction is clear here). Third whatever f3 & f4 it gives true on the basis of wrong assumption.Therefore it results in true=false. If i am wrong then just give comment on H1: r1=k1 & In r1(k2:: t) [in IH3] or how these f2 f3 play their role ? Thank u.
The fact that
In r1 (k2 :: t) is not possible in
IH3 simply says that
iH3 is of the form
False -> ... So
IH3 is no contradictory, it just means
IH3 is useless : we cannot derive anything from it.
Last updated: Oct 04 2023 at 21:01 UTC