- Having some infinite branch
- Having only infinite branches
- Having some finite branch
- Having only finite branches (
*i.e.*being finite)

For each of the preceding predicates, build an example tree, then prove that it satisfies this predicate.

Prove the following theorems (for any tree

- If every branch of
*t*is finite, t has no infinite branch. - If t has some infinite branch, the not every branch of
*t*is finite. - If t has some finite branch, then not every branch of
*t*is infinite. - If t has no finite branch, then every branch of
*t*is infinite. - If t is finite, then
`(graft t (LLeaf A))=t.` `(in classical logic :) if not every branch of t is finite, then t has some infinite branch.`

Moreover, the last theorem of the list above can't be proved in the intuitionnistic framework of

Section classic. Hypothesis class : forall P:Prop, ~~P->P. ...

Going home

Pierre Castéran