---

Step * of Lemma code-coded-pair

∀n:ℕ. (let a,b = coded-pair(n) in code-pair(a;b) = n ∈ ℤ)
BY
{ xxx(Auto
      THEN RepUR ``code-pair coded-pair`` 0
      THEN (GenConcl ⌜tsqrt(n) = x ∈ ℕ⌝⋅ THENA Auto')
      THEN RepeatFor 4 ((CallByValueReduce 0 THENA Auto))
      THEN Reduce 0
      THEN RW IntNormC 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (let  a,b  =  coded-pair(n)  in  code-pair(a;b)  =  n)


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``code-pair  coded-pair``  0
        THEN  (GenConcl  \mkleeneopen{}tsqrt(n)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto')
        THEN  RepeatFor  4  ((CallByValueReduce  0  THENA  Auto))
        THEN  Reduce  0
        THEN  RW  IntNormC  0
        THEN  Auto)xxx

---

Home Index