This file proves that verifyEvaluatePair queries are well-behaved.

theorem Cedar.Thm.verifyMatchesEquivalent_wbepq : WellBehavedEvaluatePairQuery (fun (t₁ t₂ : SymCC.Term) => have t₁matches := SymCC.Factory.eq t₁ (⊙SymCC.Term.prim (SymCC.TermPrim.bool true)); have t₂matches := SymCC.Factory.eq t₂ (⊙SymCC.Term.prim (SymCC.TermPrim.bool true)); SymCC.Factory.eq t₁matches t₂matches) fun (r₁ r₂ : Spec.Result Spec.Value) => (r₁ == Except.ok (Spec.Value.prim (Spec.Prim.bool true))) == (r₂ == Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

theorem Cedar.Thm.verifyMatchesImplies_wbepq : WellBehavedEvaluatePairQuery (fun (t₁ t₂ : SymCC.Term) => have t₁matches := SymCC.Factory.eq t₁ (⊙SymCC.Term.prim (SymCC.TermPrim.bool true)); have t₂matches := SymCC.Factory.eq t₂ (⊙SymCC.Term.prim (SymCC.TermPrim.bool true)); SymCC.Factory.implies t₁matches t₂matches) fun (r₁ r₂ : Spec.Result Spec.Value) => r₁ != Except.ok (Spec.Value.prim (Spec.Prim.bool true)) || r₂ == Except.ok (Spec.Value.prim (Spec.Prim.bool true))

theorem Cedar.Thm.verifyMatchesDisjoint_wbepq : WellBehavedEvaluatePairQuery (fun (t₁ t₂ : SymCC.Term) => have t₁matches := SymCC.Factory.eq t₁ (⊙SymCC.Term.prim (SymCC.TermPrim.bool true)); have t₂matches := SymCC.Factory.eq t₂ (⊙SymCC.Term.prim (SymCC.TermPrim.bool true)); SymCC.Factory.not (SymCC.Factory.and t₁matches t₂matches)) fun (r₁ r₂ : Spec.Result Spec.Value) => !(r₁ == Except.ok (Spec.Value.prim (Spec.Prim.bool true)) && r₂ == Except.ok (Spec.Value.prim (Spec.Prim.bool true)))