Stream: Coq users

Topic: theorem statement

zohaze (Dec 09 2022 at 03:54):

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: Apr 19 2024 at 20:01 UTC