E.2.2 PATH

spec

Path =

 

Non_Empty_List_Of[ Name fit Item |-> Name ]
with

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