gapt.examples.nTape5Arith
See thenTape5Arith companion class
object nTape5Arith
Version 5 of the higher-order n-Tape proof, where if-then-else is still proved in arithmetic. 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 nTape5Arith(2) works.
Attributes
- Companion
- class
- Graph
-
- Supertypes
-
class Objecttrait Matchableclass Any
- Self type
-
nTape5Arith.type
Members list
In this article