--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/class_c_1.ma".
+include "ground/lib/subset.ma".
+
+include "delayed_updating/syntax/path_depth.ma".
+include "delayed_updating/syntax/path_height.ma".
+
+(* CLOSED CONDITION FOR PATH ************************************************)
+
+axiom pcc: relation2 nat path.
+
+interpretation
+ "closed condition (path)"
+ 'ClassC n = (pcc n).
+
+(* Basic destructions *******************************************************)
+
+axiom pcc_empty:
+ (š) Ļµ šāØšā©.
+
+axiom pcc_d (p) (d) (n:pnat):
+ p Ļµ šāØd+nā© ā pāš±n Ļµ šāØdā©.
+
+axiom pcc_L (p) (d):
+ p Ļµ šāØdā© ā pāš Ļµ šāØādā©.
+
+axiom pcc_A (p) (d):
+ p Ļµ šāØdā© ā pāš Ļµ šāØdā©.
+
+axiom pcc_S (p) (d):
+ p Ļµ šāØdā© ā pāš¦ Ļµ šāØdā©.
+
+axiom pcc_des_gen (p) (d):
+ p Ļµ šāØdā© ā d + āÆp = āpā.