---

Step * 2 of Lemma st-lookup-outl


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
⊢ (↑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)
     ∧ (outl(let n = v in
                 if t2 <z n ∨bK ≤z n then inr ⋅  else inl (snd((t3 n))) fi )
       = <key(<K, t2, t3>;n), data(<K, t2, t3>;n)>
       ∈ (ℕ + Atom1 × data(T)))))
BY
{ ((InstLemma `mu-property` [λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x)])⋅ THEN All Reduce) }

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
⊢ λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x) ∈ ℕ ─→ 𝔹

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
⊢ ∃n:ℕ. (↑(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x))

3
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 mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x))
∨bK ≤z mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x))
∨bfst((t3 mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x)))) =a1 x))
∧ (∀[i:ℕ]. ¬↑(t2 <z i ∨bK ≤z i ∨bfst((t3 i)) =a1 x) supposing i < mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x)))
⊢ (↑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)
     ∧ (outl(let n = v in
                 if t2 <z n ∨bK ≤z n then inr ⋅  else inl (snd((t3 n))) fi )
       = <key(<K, t2, t3>;n), data(<K, t2, t3>;n)>
       ∈ (ℕ + Atom1 × data(T)))))

---

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
\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  ))
{}\mRightarrow{}  (\mexists{}n:\mBbbN{}K
          ((n  \mleq{}  t2)
          \mwedge{}  ((fst((t3  n)))  =  x)
          \mwedge{}  (outl(let  n  =  v  in
                                  if  t2  <z  n  \mvee{}\msubb{}K  \mleq{}z  n  then  inr  \mcdot{}    else  inl  (snd((t3  n)))  fi  )
              =  <key(<K,  t2,  t3>n),  data(<K,  t2,  t3>n)>)))


By

((InstLemma  `mu-property`  [\mlambda{}n.(t2  <z  n  \mvee{}\msubb{}K  \mleq{}z  n  \mvee{}\msubb{}fst((t3  n))  =a1  x)])\mcdot{}  THEN  All  Reduce)

---

Home Index