---

Step * 2 3 1 of Lemma st-lookup-property


1. [T] : Id ─→ Type
2. K : ℕ@i
3. t2 : ℕ@i
4. t3 : ℕK ─→ (Atom1 × ℕ + Atom1 × data(T))@i
5. x : Atom1@i
6. v : ℕ@i
7. mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x)) = v ∈ ℕ@i
8. (↑(t2 <z v ∨bK ≤z v ∨bfst((t3 v)) =a1 x)) ∧ (∀[i:ℕ]. ¬↑(t2 <z i ∨bK ≤z i ∨bfst((t3 i)) =a1 x) supposing i < v)
⊢ ↑isl(let n = v in
           if t2 <z n ∨bK ≤z n then inr ⋅  else inl (snd((t3 n))) fi )
⇐⇒ ∃n:ℕK. ((n ≤ t2) ∧ ((fst((t3 n))) = x ∈ Atom1))
BY
{ (((RepUR ``let`` 0 THEN SplitOnConclITE) THENA Auto) THEN RepUR ``isl bfalse`` 0 THEN Auto THEN ExRepD) }

1
1. T : Id ─→ Type
2. K : ℕ@i
3. t2 : ℕ@i
4. t3 : ℕK ─→ (Atom1 × ℕ + Atom1 × data(T))@i
5. x : Atom1@i
6. v : ℕ@i
7. mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x)) = v ∈ ℕ@i
8. ↑(t2 <z v ∨bK ≤z v ∨bfst((t3 v)) =a1 x)
9. ∀[i:ℕ]. ¬↑(t2 <z i ∨bK ≤z i ∨bfst((t3 i)) =a1 x) supposing i < v
10. t2 < v ∨ (K ≤ v)
11. n : ℕK@i
12. n ≤ t2@i
13. (fst((t3 n))) = x ∈ Atom1@i
⊢ False

2
1. [T] : Id ─→ Type
2. K : ℕ@i
3. t2 : ℕ@i
4. t3 : ℕK ─→ (Atom1 × ℕ + Atom1 × data(T))@i
5. x : Atom1@i
6. v : ℕ@i
7. mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x)) = v ∈ ℕ@i
8. ↑(t2 <z v ∨bK ≤z v ∨bfst((t3 v)) =a1 x)
9. ∀[i:ℕ]. ¬↑(t2 <z i ∨bK ≤z i ∨bfst((t3 i)) =a1 x) supposing i < v
10. v ≤ t2
11. v < K
12. True@i
⊢ ∃n:ℕK. ((n ≤ t2) ∧ ((fst((t3 n))) = x ∈ Atom1))

---

Latex:



1.  [T]  :  Id  {}\mrightarrow{}  Type
2.  K  :  \mBbbN{}@i
3.  t2  :  \mBbbN{}@i
4.  t3  :  \mBbbN{}K  {}\mrightarrow{}  (Atom1  \mtimes{}  \mBbbN{}  +  Atom1  \mtimes{}  data(T))@i
5.  x  :  Atom1@i
6.  v  :  \mBbbN{}@i
7.  mu(\mlambda{}n.(t2  <z  n  \mvee{}\msubb{}K  \mleq{}z  n  \mvee{}\msubb{}fst((t3  n))  =a1  x))  =  v@i
8.  (\muparrow{}(t2  <z  v  \mvee{}\msubb{}K  \mleq{}z  v  \mvee{}\msubb{}fst((t3  v))  =a1  x))
\mwedge{}  (\mforall{}[i:\mBbbN{}].  \mneg{}\muparrow{}(t2  <z  i  \mvee{}\msubb{}K  \mleq{}z  i  \mvee{}\msubb{}fst((t3  i))  =a1  x)  supposing  i  <  v)
\mvdash{}  \muparrow{}isl(let  n  =  v  in
                      if  t2  <z  n  \mvee{}\msubb{}K  \mleq{}z  n  then  inr  \mcdot{}    else  inl  (snd((t3  n)))  fi  )
\mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}K.  ((n  \mleq{}  t2)  \mwedge{}  ((fst((t3  n)))  =  x))


By

(((RepUR  ``let``  0  THEN  SplitOnConclITE)  THENA  Auto)
  THEN  RepUR  ``isl  bfalse``  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index