Fixpoint total_cycle (num x y: nat) (l: list nat): bool :=
match num with
| O => false
| S num' => (f1 x y) && if (f2 x y) then true else
let l1 := f3 ( y l))) in
match l1 with
| nil => false
| a1::t => if f1 a1 y then
total_cycle num' x a1 t
else false
end
end.
I am simplifing this function by performing induction and checking the functions
(f1 f2 f3 (f1 a1 y) . In case of false outpt from f2 & l1<>nil and true from(f1 a1 y) ,I
move for next recursive call and new value of a1 appears and this process goes on repeating again and again.
It has no limit untill num is equal to zero. How to write it in the form of lemma statement
so that recursive process can be stop? How i should proceed?
Last updated: Dec 05 2023 at 06:01 UTC