theorem
Compiler.Commons.iter_inc
{x : Ident}
{σ : SCORE.Store}
{k : ℤ}
(v : ℕ)
:
(σ x).head? = some k →
(fun (t : SCORE.State) => SCORE.eval (SCORE.Com.INC x) t)^[v] (some σ) = some (σ[x ↦ (k + ↑v) :: (σ x).tail])
theorem
Compiler.Commons.iter_dec
{x : Ident}
{σ : SCORE.Store}
{k : ℤ}
(v : ℕ)
:
(σ x).head? = some k →
(fun (t : SCORE.State) => SCORE.eval (SCORE.Com.DEC x) t)^[v] (some σ) = some (σ[x ↦ (k - ↑v) :: (σ x).tail])
theorem
Compiler.Commons.for_inc
{x : Ident}
{y : Ident}
{v₁ : ℤ}
{v₂ : ℤ}
{σ : SCORE.Store}
:
(σ x).head? = some v₁ →
(σ y).head? = some v₂ →
SCORE.eval (SCORE.Com.FOR y (SCORE.Com.INC x)) (some σ) = some (σ[x ↦ (v₁ + v₂) :: (σ x).tail])
theorem
Compiler.Commons.for_dec
{x : Ident}
{y : Ident}
{v₁ : ℤ}
{v₂ : ℤ}
{σ : SCORE.Store}
:
(σ x).head? = some v₁ →
(σ y).head? = some v₂ →
SCORE.eval (SCORE.Com.FOR y (SCORE.Com.DEC x)) (some σ) = some (σ[x ↦ (v₁ - v₂) :: (σ x).tail])