- 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
`charAddr`

: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
`Bool`

. The proof that a boolean is`True`

is*trivial*. *But*the interpreter in Agda seems to be*too inefficient*to handle this...- Others have worked on this problem [3].

- Formulate it as an expression of type