Computing the memory address for given screen coordinates:
charAddr ∈ Column → Row → ScreenAddr charAddr (x,xr) (y,yr) = (lo screen + 2*(80*x+y),
A lemma for
All x,y . InRange xRange x ⇒ InRange yRange y ⇒ InRange screen (lo screen + 2*(80*x+y))
Decidable, should prove itself:
Formulate it as an expression of type
. The proof that a boolean is
Requires a proof checker that has a reasonably efficient interpreter. Others have worked on this problem .