---

Step * 1 of Lemma norm-intransit_wf


1. M : Type ─→ Type
2. intr : pInTransit(P.M[P])
⊢ norm-intransit(intr) ∈ {intr':pInTransit(P.M[P])| intr' = intr ∈ pInTransit(P.M[P])} 
BY
{ ((D -1 THEN D -2 THEN D -1)
   THEN RepUR ``norm-intransit pInTransit`` 0
   THEN (Repeat (CallByValueReduce 0) THENM (MemTypeCD THEN Auto))
   THEN Try ((BLemma `Id-has-value` THEN Declaration))) }

1
.....aux..... 
1. M : Type ─→ Type
2. i3 : ℤ
3. i4 : Id
4. i5 : Id
5. i6 : pCom(P.M[P])
⊢ (i3)↓

2
.....aux..... 
1. M : Type ─→ Type
2. i3 : ℤ
3. i4 : Id
4. i5 : Id
5. i6 : pCom(P.M[P])
⊢ (i6)↓

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  intr  :  pInTransit(P.M[P])
\mvdash{}  norm-intransit(intr)  \mmember{}  \{intr':pInTransit(P.M[P])|  intr'  =  intr\} 


By

---

Latex:
((D  -1  THEN  D  -2  THEN  D  -1)
  THEN  RepUR  ``norm-intransit  pInTransit``  0
  THEN  (Repeat  (CallByValueReduce  0)  THENM  (MemTypeCD  THEN  Auto))
  THEN  Try  ((BLemma  `Id-has-value`  THEN  Declaration)))

---

Home Index