, 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
,
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 ,
Jumping and Escaping: Modular Termination and the Abstract Path Ordering, Theoretical Computer Science, vol.464, pp.35-47, 2012. ,
, Graph Theory, 2005.
A Constructive Proof of the Topological Kruskal Theorem, 2013. ,
Algebraic Relativization and Arrow Logic, PhD Dissertation, 1995. ,