closure pair(s, f) is closed under f.list(usable). a(closedunder,pair(a(closure,pair(xs,xf)),xf)) = p1. end_of_list.
Proof that closure pair(s, f) is closed under f | OTTER output file
up | previous | next | detailed contents | brief contents