1 include "apps_2/notation/models/upspoon_3.ma".
3 al: nat → dd → dd; (* alignment *)
5 interpretation "alignment (model)"
6 'UpSpoon M i d = (al M i d).
8 (* Note: lift: compatibility *)
9 mf: compatible_3 … (al M) (eq …) (sq M) (sq M);
10 (* Note: lift: swap *)
11 mw: ∀l1,l2,d. l2 ≤ l1 → ⫯[l2]⫯[l1]d ≗{M} ⫯[↑l1]⫯[l2]d;
12 (* Note: lift: sort evaluation *)
13 mv: ∀l,s. ⫯[l](sv M s) ≗ sv M s;
15 theorem valign_swap (M): is_model M →
17 ∀lv:evaluation …. ⫯[l2]⫯[l1]lv ≗{M} ⫯[↑l1]⫯[l2]lv.
18 /2 width=1 by mw/ qed.
20 lemma valign_comp (M): is_model M →
21 ∀l. compatible_2 … (valign M l) (veq M) (veq M).
22 /2 width=1 by mf/ qed-.