zohaze (Nov 08 2021 at 18:12): zohaze (Nov 08 2021 at 18:12):I have defined recursive function f. In this function pattern matching occurs on two parameters (a:nat & b<?c:bool relation) and have a>>c . Q1)No of time recursive function is being call is equal to smaller value of pattern matching(c) or output elements of function are equal to c? Q2)To prove output is equal to c what constraint I should have ? Q3) First perform induction on a then destruct c or (b<? c) for simplification?
Last updated: Oct 05 2023 at 02:01 UTC