---

Step * 2 2 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
⊢ ∃n:ℕ. (↑(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x))
BY
{ (Reduce 0 THEN (InstConcl [K])⋅ THEN Try (Complete (Auto))) }

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
⊢ ↑(t2 <z K ∨bK ≤z K ∨bfst((t3 K)) =a1 x)

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

---

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{}  \mexists{}n:\mBbbN{}.  (\muparrow{}(t2  <z  n  \mvee{}\msubb{}K  \mleq{}z  n  \mvee{}\msubb{}fst((t3  n))  =a1  x))


By

(Reduce  0  THEN  (InstConcl  [K])\mcdot{}  THEN  Try  (Complete  (Auto)))

---

Home Index