ΣE-algebra -
M
\skipx
= ( T
Σ
/ ∼ , Σ/ ∼ )
no junk
- \A a : T
Σ
/ ∼ \E t [e\dot]val
M
\skipx
(t) = a
no confusion
-
M
\skipx
\models t
1
= t
2
\desdak E \vdash t
1
= t
2
slide
:
Initial models