2.2 PATH

spec

PATH =

 

NON_EMPTY_LIST_OF[ NAME fit Item |-> Name ]
rename

List[Name]	|-> Path,
add__to__	|-> __/__ ,
first	|-> the_first_name_of__ ,
tail	|-> the_last_part_of__ ,
__is_a_singleton	|-> __is_a_name

then

ops

the_first_part_of__ : Path ->? Path;
the_last_name_of__ : Path -> Name

vars

n : Name; p : Path

axioms

def (the_first_part_of p) <=> ¬ (p in Name);
¬ (p in Name) =>
  the_first_part_of (n/p) =e= n/the_first_part_of p;
p in Name => the_first_part_of (n/p) =e= n;
the_last_name_of n = n;
the_last_name_of (n/p) = the_last_name_of p

end