---

Step * of Lemma coded-code-pair

∀[a,b:ℕ].  (coded-pair(code-pair(a;b)) = <a, b> ∈ (ℕ × ℕ))
BY
{ xxx(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)))xxx }

1
1. a : ℕ
2. b : ℕ
3. x : ℕ
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:
xxx(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)))xxx

---

Home Index