---

Step * of Lemma decidable__run-pred

∀[M:Type ⟶ Type]. ∀r:pRunType(P.M[P]). ∀e1,e2:runEvents(r).  Dec(e1 run-pred(r) e2)
BY
{ (UseWitness ⌜λr,e1,e2. if run-event-loc(e1) = run-event-loc(e2) ∧b run-event-step(e1) <z run-event-step(e2)
                           then inl inl <Ax, Ax>
                        if let ev = fst(run-info(r;e2)) in snd(e1) = snd(ev) ∧b (fst(e1) =z fst(ev)) then inl (inr Ax )
                        else inr (λx.Ax) 
                        fi ⌝⋅
   THEN Unfold `uall` 0
   THEN (MemTypeCD THENA Auto)
   THEN (RepeatFor 3 ((MemCD THEN Try (Complete (Auto))))
         THEN RepUR ``let`` 0
         THEN RepUR ``decidable or infix_ap run-pred it and not`` 0⋅
         THEN (GenConcl ⌜(fst(run-info(r;e2))) = ev ∈ (ℤ × Id)⌝⋅ THENA Auto)
         THEN Thin (-1)
         THEN D -1
         THEN RepeatFor 2 (DVar `e1')
         THEN RepeatFor 2 (DVar `e2')
         THEN RepUR ``run-event-loc run-event-step`` 0
         THEN All Thin)⋅) }

1
1. e5 : ℕ@i
2. e6 : Id@i
3. e7 : ℕ@i
4. e8 : Id@i
5. e3 : ℤ@i
6. e4 : Id@i
⊢ if e6 = e8 ∧b e5 <z e7 then inl inl <Ax, Ax>
  if e6 = e4 ∧b (e5 =z e3) then inl (inr Ax )
  else inr (λx.Ax) 
  fi  ∈ e6 = e8 ∈ Id × e5 < e7 + (<e5, e6> = <e3, e4> ∈ (ℤ × Id)) + ((e6 = e8 ∈ Id × e5 < e7 + (<e5, e6>
                                                                                              = <e3, e4>
                                                                                              ∈ (ℤ × Id)))
                                                                   ⇒ False)

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}r:pRunType(P.M[P]).  \mforall{}e1,e2:runEvents(r).    Dec(e1  run-pred(r)  e2)


By

---

Latex:
(UseWitness  \mkleeneopen{}\mlambda{}r,e1,e2.  if  run-event-loc(e1)  =  run-event-loc(e2)
                                                    \mwedge{}\msubb{}  run-event-step(e1)  <z  run-event-step(e2)
                                                  then  inl  inl  <Ax,  Ax>
                                            if  let  ev  =  fst(run-info(r;e2))  in
                                                          snd(e1)  =  snd(ev)  \mwedge{}\msubb{}  (fst(e1)  =\msubz{}  fst(ev))
                                                then  inl  (inr  Ax  )
                                            else  inr  (\mlambda{}x.Ax) 
                                            fi  \mkleeneclose{}\mcdot{}
  THEN  Unfold  `uall`  0
  THEN  (MemTypeCD  THENA  Auto)
  THEN  (RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto))))
              THEN  RepUR  ``let``  0
              THEN  RepUR  ``decidable  or  infix\_ap  run-pred  it  and  not``  0\mcdot{}
              THEN  (GenConcl  \mkleeneopen{}(fst(run-info(r;e2)))  =  ev\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Thin  (-1)
              THEN  D  -1
              THEN  RepeatFor  2  (DVar  `e1')
              THEN  RepeatFor  2  (DVar  `e2')
              THEN  RepUR  ``run-event-loc  run-event-step``  0
              THEN  All  Thin)\mcdot{})

---

Home Index