# Library Copland.Term_system

Copland specific event systems.
Construct an event system from an annotated term, place, and evidence.

Fixpoint ev_sys (t: AnnoTerm) p e: EvSys Ev :=
match t with
| aasp (i, j) xleaf (i, j) (asp_event i x p e)
| aatt (i, j) q x
before (i, j)
(leaf (i, S i) (req i p q e))
(before (S i, j)
(ev_sys x q e)
(leaf (pred j, j) (rpy (pred j) p q (aeval x q e))))
| alseq r x ybefore r (ev_sys x p e)
(ev_sys y p (aeval x p e))
| abseq (i, j) s x y
before (i, j)
(leaf (i, S i)
(split i p e (sp (fst s) e)
(sp (snd s) e)))
(before (S i, j)
(before (S i, (pred j))
(ev_sys x p (sp (fst s) e))
(ev_sys y p (sp (snd s) e)))
(leaf ((pred j), j)
(join (pred j) p
(aeval x p (sp (fst s) e))
(aeval y p (sp (snd s) e))
(ss (aeval x p (sp (fst s) e))
(aeval y p (sp (snd s) e))))))
| abpar (i, j) s x y
before (i, j)
(leaf (i, S i)
(split i p e (sp (fst s) e)
(sp (snd s) e)))
(before (S i, j)
(merge (S i, (pred j))
(ev_sys x p (sp (fst s) e))
(ev_sys y p (sp (snd s) e)))
(leaf ((pred j), j)
(join (pred j) p
(aeval x p (sp (fst s) e))
(aeval y p (sp (snd s) e))
(pp (aeval x p (sp (fst s) e))
(aeval y p (sp (snd s) e))))))
end.

Lemma evsys_range:
t p e,
es_range (ev_sys t p e) = range t.

Lemma well_structured_evsys:
t p e,
well_formed t
well_structured ev (ev_sys t p e).

The events in the event system correspond to the events associated with a term, a place, and some evidence.

Lemma evsys_events:
t p e ev,
well_formed t
ev_in ev (ev_sys t p e) events t p e ev.

Maximal events are unique.

Lemma supreme_unique:
t p e,
well_formed t
! v, supreme (ev_sys t p e) v.

Lemma evsys_max_unique:
t p e,
well_formed t
unique (supreme (ev_sys t p e)) (max (ev_sys t p e)).

Maximal event evidence output matches aeval.

Definition out_ev v :=
match v with
| copy _ _ ee
| kmeas _ _ _ _ ee
| umeas _ _ _ _ ee
| sign _ _ _ ee
| hash _ _ _ ee
| req _ _ _ ee
| rpy _ _ _ ee
| split _ _ _ _ ee
| join _ _ _ _ ee
end.

Lemma max_eval:
t p e,
well_formed t
out_ev (max (ev_sys t p e)) = aeval t p e.

lseq is associative relative to the event semantics

Lemma lseq_assoc:
t1 t2 t3 i p e,
same_rel
(ev_sys (snd (anno (lseq t1 (lseq t2 t3)) i)) p e)
(ev_sys (snd (anno (lseq (lseq t1 t2) t3) i)) p e).