This file proves the compilation lemmas for .ite, .and, and .or expressions.

theorem Cedar.Thm.compile_evaluate_ite {x₁ x₂ x₃ : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : env ∼ εnv) (h₂ : env.WellFormedFor (x₁.ite x₂ x₃)) (h₃ : εnv.WellFormedFor (x₁.ite x₂ x₃)) (h₄ : SymCC.compile (x₁.ite x₂ x₃) εnv = Except.ok t) (ih₁ : CompileEvaluate x₁) (ih₂ : CompileEvaluate x₂) (ih₃ : CompileEvaluate x₃) : Spec.evaluate (x₁.ite x₂ x₃) env.request env.entities ∼ t

theorem Cedar.Thm.compile_interpret_ite {x₁ x₂ x₃ : Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {t : SymCC.Term} (h₁ : I.WellFormed εnv.entities) (h₂ : εnv.WellFormedFor (x₁.ite x₂ x₃)) (h₃ : SymCC.compile (x₁.ite x₂ x₃) εnv = Except.ok t) (ih₁ : CompileInterpret x₁) (ih₂ : CompileInterpret x₂) (ih₃ : CompileInterpret x₃) : SymCC.compile (x₁.ite x₂ x₃) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)

theorem Cedar.Thm.compile_evaluate_and {x₁ x₂ : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : env ∼ εnv) (h₂ : env.WellFormedFor (x₁.and x₂)) (h₃ : εnv.WellFormedFor (x₁.and x₂)) (h₄ : SymCC.compile (x₁.and x₂) εnv = Except.ok t) (ih₁ : CompileEvaluate x₁) (ih₂ : CompileEvaluate x₂) : Spec.evaluate (x₁.and x₂) env.request env.entities ∼ t

theorem Cedar.Thm.compile_interpret_and {x₁ x₂ : Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {t : SymCC.Term} (h₁ : I.WellFormed εnv.entities) (h₂ : εnv.WellFormedFor (x₁.and x₂)) (h₃ : SymCC.compile (x₁.and x₂) εnv = Except.ok t) (ih₁ : CompileInterpret x₁) (ih₂ : CompileInterpret x₂) : SymCC.compile (x₁.and x₂) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)

theorem Cedar.Thm.compile_evaluate_or {x₁ x₂ : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} (h₁ : env ∼ εnv) (h₂ : env.WellFormedFor (x₁.or x₂)) (h₃ : εnv.WellFormedFor (x₁.or x₂)) (h₄ : SymCC.compile (x₁.or x₂) εnv = Except.ok t) (ih₁ : CompileEvaluate x₁) (ih₂ : CompileEvaluate x₂) : Spec.evaluate (x₁.or x₂) env.request env.entities ∼ t

theorem Cedar.Thm.compile_interpret_or {x₁ x₂ : Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {t : SymCC.Term} (h₁ : I.WellFormed εnv.entities) (h₂ : εnv.WellFormedFor (x₁.or x₂)) (h₃ : SymCC.compile (x₁.or x₂) εnv = Except.ok t) (ih₁ : CompileInterpret x₁) (ih₂ : CompileInterpret x₂) : SymCC.compile (x₁.or x₂) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)