Reduction Semantics Determinism Proofs

[ramsay-t]

Proof of ⟶-det and related lemmas in the metatheory.

⟶-det is the proof that reduction is deterministic, and it depends on the value-¬⟶ and ⟶-¬value lemmas that show that Values do not ever reduce.