I want to prove function equality of two functions f1 & f2. Whose input arguments are nat and nat list and output is bool.Matching patteren of these functions is input list.

I should move in the following way

1) [] of f1= [] of f2

2) [a] of f1= [a] of f2

3)(a::t) of f1= (a::t) of f2

How to terminate the third case.In hypothesises i have all the conditions under which f1 give true in the case of two elements

in the input list. I have to relate these conditions with f2 for each and every case?

looks like you should use the induction hypothesis `f1 l = f2 l`

in order to prove that `f1 [a::l] = f2 [a::l]`

Yes. When apply induction then one element appears in the list and hypothesis gives all test conditions true.Then second time

two elements and their hypothesis ....in f1. I want to ask how to terminate . Now list is not empty,true required hypothesis (related to f1) including induction hypothesises. Now i have to use these induction hypothesises to prove f2? Stop induction after two time?

how to use the induction depends of the definition of `f1`

and `f2`

. If you don't give us their definition it is difficult to help you.

Last updated: Oct 04 2023 at 20:01 UTC