Title: Verification and derivation of infinite-list programs