---

Step * of Lemma code-coded-pair

∀n:ℕ. (let a,b = coded-pair(n) in code-pair(a;b) = n ∈ ℤ)
BY
{ TACTIC:(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) }

---

Latex:

---

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


By

---

Latex:
TACTIC:(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)

---

Home Index