Proofs
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
.
Requires a proof checker that has a reasonably efficient interpreter. Others have worked on this problem [3].