include "lambda/paths/standard_trace.ma".
include "lambda/paths/labeled_sequential_computation.ma".
+include "lambda/notation/relations/decomposedstd_2.ma".
+
(* DECOMPOSED STANDARD COMPUTATION ***********************************************)
(* Note: this is the "standard" computation of:
interpretation "decomposed standard computation"
'DecomposedStd M N = (dst M N).
-notation "hvbox( M break ⓢ↦* term 46 N )"
- non associative with precedence 45
- for @{ 'DecomposedStd $M $N }.
-
lemma dst_inv_lref: ∀M,N. M ⓢ↦* N → ∀j. #j = N →
∃∃s. is_whd s & M ↦*[s] #j.
#M #N * -M -N