---

Step * of Lemma coded-code-pair

∀[a,b:ℕ].  (coded-pair(code-pair(a;b)) = <a, b> ∈ (ℕ × ℕ))
BY
{ TACTIC:(Auto
          THEN RepUR ``coded-pair`` 0
          THEN (CallByValueReduce 0 THENA Auto)
          THEN RepUR ``code-pair`` 0
          THEN (GenConcl ⌜tsqrt(t(a + b) + a) = x ∈ ℕ⌝⋅ THENA Auto')
          THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))) }

1
1. a : ℕ
2. b : ℕ
3. x : ℕ@i
4. tsqrt(t(a + b) + a) = x ∈ ℕ
⊢ <(t(a + b) + a) - t(x), x - (t(a + b) + a) - t(x)> = <a, b> ∈ (ℕ × ℕ)

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbN{}].    (coded-pair(code-pair(a;b))  =  <a,  b>)


By

---

Latex:
TACTIC:(Auto
                THEN  RepUR  ``coded-pair``  0
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  RepUR  ``code-pair``  0
                THEN  (GenConcl  \mkleeneopen{}tsqrt(t(a  +  b)  +  a)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto')
                THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index