(* *)
(**************************************************************************)
-include "basic_2/rt_transition/lfpx_aaa.ma".
+include "basic_2/rt_transition/lpx_aaa.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
(* Properties with atomic arity assignment on terms *************************)
-lemma cpxs_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpxs h G L).
+lemma cpxs_aaa_conf (G) (L):
+ Conf3 … (aaa G L) (cpxs G L).
#h #G #L @TC_Conf3 @cpx_aaa_conf (**) (* auto fails *)
qed-.