(**************************************************************************)
include "basic_2/grammar/tstc.ma".
-include "basic_2/computation/llpxs_cpxs.ma".
+include "basic_2/computation/lpxs_cpxs.ma".
(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
elim (IHn … Hnl) -IHn
[ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
| generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n
- /4 width=3 by cpxs_strap2, cpx_sort, or_intror/
+ /4 width=3 by cpxs_strap2, cpx_st, or_intror/
| >iter_SO >iter_n_Sm //
]
]