zohaze (Mar 04 2024 at 17:11): zohaze (Mar 04 2024 at 17:11):Definition mod_fun (first a: nat)(l: list nat) : nat:=
if beq_nat first 0 then a mod (length l) else (a+1) mod (length l).
I am using mod_fun in main function f' recusively, whose output is list nat. In main function simply
increase the value of a.(always start first=0 , a=0 , increase a till it becomes equal to length l and only first time
first is zero). Output list nat always contains more zeros than any other natural number.(Because f' always start with zero and get zero when a becomes equal to length l). I want to prove this statement,how to do it?
Last updated: Oct 13 2024 at 01:02 UTC