zohaze (Apr 06 2023 at 12:43): zohaze (Apr 06 2023 at 12:43):I have following functions, i am changing the
sequence/order of functions to show result will be same.
Fixpoint finding(l1 l2: list nat) : bool :=
match l1 with
| nil=> false
|k::t'=> if In k l2 then true else finding t' l2
end.
eq1: a::a1::t <>[]
eq2: f2 (a :: a1 :: f1 a t) = b :: b1 :: l' ->
eq3: finding (f3 b (b1 :: l')) (b1 :: l') = true->
goal statement f2 (f1 a1 (f3 a1 (a :: a1 :: t)))) = b :: b1 :: l'
In k l2 is boolean form of In predicate. I want to ask how to start?
Last updated: Oct 04 2023 at 22:01 UTC