gapt.examples.nTape5
See thenTape5 companion class
object nTape5
Version 5 of the higher-order n-Tape proof. In contrast to nTape4 it cuts on instances of the theorem C for specific upper bounds n. Since the instantiated proofs were generated manually, only nTape5(2) to nTape5(4) work.
Attributes
Members list
In this article