---

Step * 1 of Lemma ctrex1-calculation

.....equality..... 
small-ctrex1() 10^1143 ~ eval N = 10^126 in
                         eval M = 10^1143 in
                           un-ctrex1(un-ctrex1((r1)/N)) M
BY
{ RepeatFor 2 ((CallByValueReduce 0 THENA Auto)) }

1
small-ctrex1() 10^1143 ~ un-ctrex1(un-ctrex1((r1)/10^126)) 10^1143

---

Latex:

---

Latex:
.....equality..... 
small-ctrex1()  10\^{}1143  \msim{}  eval  N  =  10\^{}126  in
                                                  eval  M  =  10\^{}1143  in
                                                      un-ctrex1(un-ctrex1((r1)/N))  M


By

---

Latex:
RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))

---

Home Index