---

Step * of Lemma total-run-lt

∀[M:Type ─→ Type]
  ∀r:pRunType(P.M[P]). ∀e1,e2:runEvents(r).
    (e1 = e2 ∈ runEvents(r)) ∨ (e1 run-lt(r) e2) ∨ (e2 run-lt(r) e1) 
    supposing run-event-loc(e1) = run-event-loc(e2) ∈ Id
BY
{ (Auto
   THEN Unfold `run-lt` 0
   THEN (Decide run-event-step(e1) ≤ run-event-step(e2) THENA Auto)
   THEN (Decide run-event-step(e2) ≤ run-event-step(e1) THENA Auto)) }

1
1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : runEvents(r)@i
4. e2 : runEvents(r)@i
5. run-event-loc(e1) = run-event-loc(e2) ∈ Id
6. run-event-step(e1) ≤ run-event-step(e2)
7. run-event-step(e2) ≤ run-event-step(e1)
⊢ (e1 = e2 ∈ runEvents(r)) ∨ (e1 run-pred(r)+ e2) ∨ (e2 run-pred(r)+ e1)

2
1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : runEvents(r)@i
4. e2 : runEvents(r)@i
5. run-event-loc(e1) = run-event-loc(e2) ∈ Id
6. run-event-step(e1) ≤ run-event-step(e2)
7. ¬(run-event-step(e2) ≤ run-event-step(e1))
⊢ (e1 = e2 ∈ runEvents(r)) ∨ (e1 run-pred(r)+ e2) ∨ (e2 run-pred(r)+ e1)

3
1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : runEvents(r)@i
4. e2 : runEvents(r)@i
5. run-event-loc(e1) = run-event-loc(e2) ∈ Id
6. ¬(run-event-step(e1) ≤ run-event-step(e2))
7. run-event-step(e2) ≤ run-event-step(e1)
⊢ (e1 = e2 ∈ runEvents(r)) ∨ (e1 run-pred(r)+ e2) ∨ (e2 run-pred(r)+ e1)

4
1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : runEvents(r)@i
4. e2 : runEvents(r)@i
5. run-event-loc(e1) = run-event-loc(e2) ∈ Id
6. ¬(run-event-step(e1) ≤ run-event-step(e2))
7. ¬(run-event-step(e2) ≤ run-event-step(e1))
⊢ (e1 = e2 ∈ runEvents(r)) ∨ (e1 run-pred(r)+ e2) ∨ (e2 run-pred(r)+ e1)

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P]).  \mforall{}e1,e2:runEvents(r).
        (e1  =  e2)  \mvee{}  (e1  run-lt(r)  e2)  \mvee{}  (e2  run-lt(r)  e1) 
        supposing  run-event-loc(e1)  =  run-event-loc(e2)


By

---

Latex:
(Auto
  THEN  Unfold  `run-lt`  0
  THEN  (Decide  run-event-step(e1)  \mleq{}  run-event-step(e2)  THENA  Auto)
  THEN  (Decide  run-event-step(e2)  \mleq{}  run-event-step(e1)  THENA  Auto))

---

Home Index