! -----    HAMILTON CYCLE     ---- !

! Returns a Hamilton Cycle of the Graph G as a list of node names.
  Standard input values:
  l0 = ( )
  init_call = ("HML_make_path") !

HML_H_Cycle		and
	T	(G	l0	init_call)
		(crd		G_size			(G)
		 add		l1			(init_call		G)
		 add		l2			(l1			G_size)
		 add		call_make_path		(l2			l0)
     	 	 at		Path			(call_make_path)
 	 	 HML_check_path	HC			(G_size			Path))


! Creates and returns a path.
  Standard input value:
  l0 = ( ) !

  HML_make_path		and
	T	(G	G_size	l0)
		(HML_init_path		P_1	(G	l0)
     	 	 HML_extend_path	Path	(G	G_size	G	G_size	P_1))


! This formula is confirmed if Path is a Hamilton Cycle of a Graph with G_size nodes. In the case of confirmation Path is returned without its last element (since this equals the first element) !

HML_check_path		and
	T	(G_size  Path)
		(bl		P_bl		(Path)
		 crd		P_size		(P_bl)
		 eq		NULL		(G_size		P_size)
		 cp		HC 		(P_bl))


! Path is a one-element list that contains a node name of G. This formula returns Path increased by a number of names of nodes that constitute a path, such that there is no next "valid connection" of the last element of Path !

HML_extend_path	rec
	T	(G	G_size		G	G_size		Path)
		(HML_not_next
		 HML_incr_path)


! Path can not be increased, i.e. there do no exist "valid connections" for the last
  element of Path !

HML_not_next		not
	NULL	(G	G_size		Path)
		(HML_has_next		NULL		(G	G_size		Path))


! Path can be increased, i.e. there exist "valid connections" for the last element of Path !

HML_has_next		and
	NULL	(G	G_size		Path)
		(HML_valid_cons	T	(G	G_size		Path))


! Returns Path increased by a node-name that represents a "valid connection" for the last element of Path !

HML_incr_path		and
	T	(G	G_size	Path)
		(HML_valid_cons		v_cons		(G	G_size		Path)
		 mem			nnn		(v_cons)
		 add			P_inc		(Path  	nnn))


! Returns a one-element list that includes the first node name of the Graph G !

HML_init_path		and
	T	(G	l0)
		(fi		n1		(G)
		 fi		nn1		(n1)
		 add		P_1		(l0	nn1))


! Returns the list of "valid connections" of the last element of the list Path. !

HML_valid_cons		and
	T	(G	G_size	Path)
		(la			nn		(Path)
		 pl			nn_con		(G		nn)
		 crd			P_size		(Path)
		 HML_sel_pot		v_cons		(nn_con	Path	G_size	P_size))


! Returns the "potential connections" for the last element of Path as the list of the elements of the list nn_con that confirm HML_ret_pot !

HML_sel_pot		chs
	T	(nn_con	Path		G_size		P_size)
		(HML_ret_pot)


! Returns the node name nn if nn represents a "potential connection" for the Path !

HML_ret_pot		and
	T	(nn	Path	G_size		P_size)
		(HML_pot_con		NULL		(nn	Path	G_size	P_size)
		 cp			Tout		(nn))


! The node named nn is a "potential connection", i.e. either it does not belong to the Path or it is the first node of Path while Path contains all the nodes of G !

HML_pot_con		or
	NULL	(nn	Path	G_size	P_size)
		(not_ism		NULL		(Path	nn)
		 HML_close_cycle	NULL		(Path	G_size	     P_size	nn))


! Path contains all the nodes of G (since G_size = P_size) and nn is the name of its first node !

HML_close_cycle		and
	NULL	(Path	G_size	P_size	nn)
		(eq		NULL		(G_size	P_size)
		 fi		nn_1		(Path)
		 eq		NULL		(nn	nn_1))


! The element nn is not contained in the list Path !

not_ism			not
	NULL	(Path		nn)
		(ism		NULL		(Path		nn))