As part of a little separation logic theory I'm working on, I have the following axiomatisation of a star operator:
> Star :: "assertion => assertion => assertion"
> where star_comm: "Star p q = Star q p"
> and star_assoc: "Star (Star p q) r = Star p (Star q r)"
> and star_emp: "Star p Emp = p"
> and emp_star: "Star Emp p = p"
I would now like to add a couple more properties of "star", such as:
> and dist_conj: "Star p (Conj q r) ≤ Conj (Star p q) (Star p r)"
However, before I can use "≤" to compare assertions, I need "assertion :: order". I don't want to *prove* this (by giving a concrete definition for ≤), instead I want simply to *assume* this. How is this done?
This archive was generated by a fusion of
Pipermail (Mailman edition) and