Step
*
1
1
1
of Lemma
code-coded-seq1
1. k : ℤ@i
2. ¬k + 1 < 1
3. k ≠ 0
4. 0 < k
5. ∀[x:ℕ]. (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
6. x : ℕ
7. v1 : ℕ@i
8. v2 : ℕ@i
9. coded-pair(x) = <v1, v2> ∈ (ℕ × ℕ)
10. code-seq1(k;λn.coded-seq1(k - 1;v1;n)) = v1 ∈ ℤ
⊢ code-pair(code-seq1(k;λn.if (n =z k) then v2 else coded-seq1(k - 1;v1;n) fi );v2) = x ∈ ℤ
BY
{ TACTIC:Subst ⌜(λn.if (n =z k) then v2 else coded-seq1(k - 1;v1;n) fi ) = (λn.coded-seq1(k - 1;v1;n)) ∈ (ℕk ⟶ ℕ)⌝ 0⋅ }
1
.....equality.....
1. k : ℤ@i
2. ¬k + 1 < 1
3. k ≠ 0
4. 0 < k
5. ∀[x:ℕ]. (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
6. x : ℕ
7. v1 : ℕ@i
8. v2 : ℕ@i
9. coded-pair(x) = <v1, v2> ∈ (ℕ × ℕ)
10. code-seq1(k;λn.coded-seq1(k - 1;v1;n)) = v1 ∈ ℤ
⊢ (λn.if (n =z k) then v2 else coded-seq1(k - 1;v1;n) fi ) = (λn.coded-seq1(k - 1;v1;n)) ∈ (ℕk ⟶ ℕ)
2
1. k : ℤ@i
2. ¬k + 1 < 1
3. k ≠ 0
4. 0 < k
5. ∀[x:ℕ]. (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
6. x : ℕ
7. v1 : ℕ@i
8. v2 : ℕ@i
9. coded-pair(x) = <v1, v2> ∈ (ℕ × ℕ)
10. code-seq1(k;λn.coded-seq1(k - 1;v1;n)) = v1 ∈ ℤ
⊢ code-pair(code-seq1(k;λn.coded-seq1(k - 1;v1;n));v2) = x ∈ ℤ
3
.....wf.....
1. k : ℤ@i
2. ¬k + 1 < 1
3. k ≠ 0
4. 0 < k
5. ∀[x:ℕ]. (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
6. x : ℕ
7. v1 : ℕ@i
8. v2 : ℕ@i
9. coded-pair(x) = <v1, v2> ∈ (ℕ × ℕ)
10. code-seq1(k;λn.coded-seq1(k - 1;v1;n)) = v1 ∈ ℤ
11. z : ℕk ⟶ ℕ
⊢ code-pair(code-seq1(k;z);v2) = x ∈ ℤ ∈ ℙ
Latex:
Latex:
1. k : \mBbbZ{}@i
2. \mneg{}k + 1 < 1
3. k \mneq{} 0
4. 0 < k
5. \mforall{}[x:\mBbbN{}]. (code-seq1(k;\mlambda{}n.coded-seq1(k - 1;x;n)) = x)
6. x : \mBbbN{}
7. v1 : \mBbbN{}@i
8. v2 : \mBbbN{}@i
9. coded-pair(x) = <v1, v2>
10. code-seq1(k;\mlambda{}n.coded-seq1(k - 1;v1;n)) = v1
\mvdash{} code-pair(code-seq1(k;\mlambda{}n.if (n =\msubz{} k) then v2 else coded-seq1(k - 1;v1;n) fi );v2) = x
By
Latex:
TACTIC:Subst \mkleeneopen{}(\mlambda{}n.if (n =\msubz{} k) then v2 else coded-seq1(k - 1;v1;n) fi )
= (\mlambda{}n.coded-seq1(k - 1;v1;n))\mkleeneclose{} 0\mcdot{}
Home
Index