Want to count two natural numbers(k1 and k2)that exist in the list. On the basis of this count I want to to find greater element.(count k1 l < count k2 l).
I have (a::l0) list nat. There is function f, whose input is (c::l0) and output is l1. During recursive call number of elements
in l1 are going to increase.( m ,c,c0 & k are nat).
H: (m > 0 ->
count_occ Nat.eq_dec (firstn m 11) 0 <= count_occ Nat.eq_dec (firstn m 11) (S k) ->
count_occ Nat.eq_dec (firstn (S m) l1 0 <= count_occ Nat.eq_dec (firstn (S m) l1 (S k)))).
When (c::c0::l0) is given to function f, then
Goal: count_occ Nat.eq_dec (firstn (S m) l1 0 <= count_occ Nat.eq_dec (firstn (S m) l1 (S k).
To prove above i should focuss on role of c0 in f? How to proceed? I have already asked but might be not properly asked.
Last updated: Feb 01 2023 at 13:03 UTC