, Definition CNFO := {o : Ord | CNF o = true}

, Definition CNFO_plus (o : CNFO) (o' : CNFO) : CNFO. destruct o as (o, CNFo

, Definition CNFO_pred (o : CNFO) : CNFO. destruct o as (o, CNFO)

, Definition CNFO_minus (o : CNFO) (o' : CNFO) : CNFO. destruct o as (o, CNFo

, Definition CNFO_nat (n : nat) : CNFO. exists (fin n)

, Definition CNFO_btb (o o' : CNFO) := btb_ord (proj1_sig o) (proj1_sig o')

, Definition CNFO_beq (o o' : CNFO) := beq_ord (proj1_sig o) (proj1_sig o')

, Infinite Paths We shall now proceed in a similar way to define the join of two paths, by first concatenating them

. ***********************************************************************,

A. ***********************************************************************)-variable and . Type, Variable eq_A : A -> A -> bool. Definition domain (o : CNFO) := {i: CNFO|CNFO_btb o i = true}. Definition path (o : CNFO) := (domain o) -> A. (*The definition of a join is complex, and requires much effort*) (*we skip it and refer to the development*) Definition join

N. Dershowitz, Jumping and Escaping: Modular Termination and the Abstract Path Ordering, Theoretical Computer Science, vol.464, pp.35-47, 2012.

R. Diestel, Graph Theory, 2005.

J. Goubault-larrecq, A Constructive Proof of the Topological Kruskal Theorem, 2013.

M. Marx, Algebraic Relativization and Arrow Logic, PhD Dissertation, 1995.