Step
*
1
of Lemma
mu-dec-in-bar-nat
1. A : Type
2. P : A ⟶ ℕ ⟶ ℙ
3. d : a:A ⟶ k:ℕ ⟶ Dec(P[a;k])
4. a : A
⊢ mu-dec(d;a) ∈ partial(ℕ)
BY
{ RepUR ``mu-dec mu mu-ge`` 0 }
1
1. A : Type
2. P : A ⟶ ℕ ⟶ ℙ
3. d : a:A ⟶ k:ℕ ⟶ Dec(P[a;k])
4. a : A
⊢ fix((λmu-ge,n. if isl(d a n) then n else eval m = n + 1 in mu-ge m fi )) 0 ∈ partial(ℕ)
Latex:
Latex:
1. A : Type
2. P : A {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}
3. d : a:A {}\mrightarrow{} k:\mBbbN{} {}\mrightarrow{} Dec(P[a;k])
4. a : A
\mvdash{} mu-dec(d;a) \mmember{} partial(\mBbbN{})
By
Latex:
RepUR ``mu-dec mu mu-ge`` 0
Home
Index