Manuscript I@2 · I.tex · lemma · 85631fa7

Lemma: Typed substitution bound

Configurations and specified Born semantics › A syntactic linear step bound · lines 658–680 · proof included or linked

I@2#lem:measure

Under the hypotheses of Lemma lem:substitution,

m (t [v / x]) \leq m (t) + m (v) .

Simultaneous substitutions for disjoint linear resources increase $m$ by at most the sum of the inserted measures.

Proof. Induct on typing, simultaneously proving the multiple-substitution statement. Multiplicative premises receive disjoint substitutions. If substitutions of total measure $a$ enter the shared alternative context, then

max {m (u [\cdot]), m (u^{'} [\cdot])} \leq max {m (u), m (u^{'})} + a .

Substitutions in the guard are disjoint from these. This proves the conditional case; the other cases are additive.

Displayed formulas in this passage

unlabeled · line 661
$m (t [v / x]) \leq m (t) + m (v) .$
unlabeled · line 674
$max {m (u [\cdot]), m (u^{'} [\cdot])} \leq max {m (u), m (u^{'})} + a .$

Lemma: Typed substitution bound

Displayed formulas in this passage

Nearby in this section