f_puzzle: typo in informal specification, better reference

parent 2e61d48b
(* Let f be a function over natural numbers such that, for all n
f(f(n)) < f(n)+1
Show that f(n)=n for all n. *)
f(f(n)) < f(n+1)
Show that f(n)=n for all n.
Inspired by a Dafny example (see http://searchco.de/codesearch/view/28108482)
Original reference is
Edsger W. Dijkstra: Heuristics for a Calculational Proof.
Inf. Process. Lett. (IPL) 53(3):141-143 (1995)
*)
theory Puzzle
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment