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