next up previous
Next: Principal Inhabitants Up: How to use the Previous: Constructing proof-trees and normal

Construction of proof-trees from normal inhabitants

The "Term Proof Tree" button allows us to verify if a normal term is an inhabitant of the type, construct the corresponding proof-tree and again generate all other normal inhabitants that correspond to the same proof-tree.

As such, after pressing this button, one may introduce a normal term in the following window:

So, one may conclude that the following term

is no inhabitant of the type:

On the other hand, for the term

one obtains the corresponding proof-tree

and pressing on the blue region also the set of normal terms that correspond to this proof-tree:

Another term

gives origin to this proof-tree

which corresponds to the following set of normal inhabitants:

Sabine Broda