output

$ stack exec abstract samples/4-nested-let.scm
λ > (0 → (+1 → (+ → (* → (^ → (1 → (2 → (^ 2) 2) ((+ 1) 1)) (+1 0)) (num1 num2 → num2 num1)) (num1 num2 succ zero → (num1 (num2 succ)) zero)) (num1 num2 succ zero → (num1 succ) (num2 succ) zero)) (num succ zero → succ ((num succ) zero))) (succ zero → zero)
β > (+1 → (+ → (* → (^ → (1 → (2 → (^ 2) 2) ((+ 1) 1)) (+1 (succ$109 zero$110 → zero$110))) (num1 num2 → num2 num1)) (num1$48 num2$49 succ zero → (num1$48 (num2$49 succ)) zero)) (num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71)) (num succ$92 zero$93 → succ$92 ((num succ$92) zero$93))
β > (+ → (* → (^ → (1 → (2 → (^ 2) 2) ((+ 1) 1)) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num1 num2 → num2 num1)) (num1$48 num2$49 succ zero → (num1$48 (num2$49 succ)) zero)) (num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71)
β > (* → (^ → (1 → (2 → (^ 2) 2) (((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) 1) 1)) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num1 num2 → num2 num1)) (num1$48 num2$49 succ zero → (num1$48 (num2$49 succ)) zero)
β > (^ → (1 → (2 → (^ 2) 2) (((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) 1) 1)) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num1 num2 → num2 num1)
β > (1 → (2 → ((num1 num2 → num2 num1) 2) 2) (((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) 1) 1)) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))
β > (2 → ((num1 num2 → num2 num1) 2) 2) (((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))
β > ((num1 num2 → num2 num1) (((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85))) ((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)
β > (((num1$68$85 num2$69$86 succ$70$87 zero$71$88 → (num1$68$85 succ$70$87) (num2$69$86 succ$70$87) zero$71$88) ((num$108 succ$92$109 zero$93$110 → succ$92$109 ((num$108 succ$92$109) zero$93$110)) (succ$109$125 zero$110$126 → zero$110$126))) (num$67$132 succ$92$68$133 zero$93$69$134 → succ$92$68$133 ((num$67$132 succ$92$68$133) zero$93$69$134)) (succ$109$84$149 zero$110$85$150 → zero$110$85$150)) ((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)
β > (zero$71$88 → (((num$108 succ$92$109 zero$93$110 → succ$92$109 ((num$108 succ$92$109) zero$93$110)) (succ$109$125 zero$110$126 → zero$110$126)) ((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) (((num$67$132 succ$92$68$133 zero$93$69$134 → succ$92$68$133 ((num$67$132 succ$92$68$133) zero$93$69$134)) (succ$109$84$149 zero$110$85$150 → zero$110$85$150)) ((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) zero$71$88)
β > (zero$71$88 → (((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125 zero$110$126 → zero$110$126) (((num1$68 num2$69 succ$70 zero$71 → (num1$68 succ$70) (num2$69 succ$70) zero$71) ((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110))) (num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85))) (((num$67$132 succ$92$68$133 zero$93$69$134 → succ$92$68$133 ((num$67$132 succ$92$68$133) zero$93$69$134)) (succ$109$84$149 zero$110$85$150 → zero$110$85$150)) ((num1$68$127 num2$69$128 succ$70$129 zero$71$130 → (num1$68$127 succ$70$129) (num2$69$128 succ$70$129) zero$71$130) ((num$150 succ$92$151 zero$93$152 → succ$92$151 ((num$150 succ$92$151) zero$93$152)) (succ$109$167 zero$110$168 → zero$110$168))) (num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) zero$71$88)
β > (zero$71$88 zero$71 → (((num succ$92 zero$93 → succ$92 ((num succ$92) zero$93)) (succ$109 zero$110 → zero$110)) ((succ$109$125 zero$110$126 → zero$110$126) (((num1$68$84 num2$69$85 succ$70$86 zero$71$87 → (num1$68$84 succ$70$86) (num2$69$85 succ$70$86) zero$71$87) ((num$107 succ$92$108 zero$93$109 → succ$92$108 ((num$107 succ$92$108) zero$93$109)) (succ$109$124 zero$110$125 → zero$110$125))) (num$67$131 succ$92$68$132 zero$93$69$133 → succ$92$68$132 ((num$67$131 succ$92$68$132) zero$93$69$133)) (succ$109$84$148 zero$110$85$149 → zero$110$85$149))) (((num$67$132 succ$92$68$133 zero$93$69$134 → succ$92$68$133 ((num$67$132 succ$92$68$133) zero$93$69$134)) (succ$109$84$149 zero$110$85$150 → zero$110$85$150)) ((num1$68$127 num2$69$128 succ$70$129 zero$71$130 → (num1$68$127 succ$70$129) (num2$69$128 succ$70$129) zero$71$130) ((num$150 succ$92$151 zero$93$152 → succ$92$151 ((num$150 succ$92$151) zero$93$152)) (succ$109$167 zero$110$168 → zero$110$168))) (num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) zero$71$88) (((num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125 zero$110$126 → zero$110$126) (((num1$68$84 num2$69$85 succ$70$86 zero$71$87 → (num1$68$84 succ$70$86) (num2$69$85 succ$70$86) zero$71$87) ((num$107 succ$92$108 zero$93$109 → succ$92$108 ((num$107 succ$92$108) zero$93$109)) (succ$109$124 zero$110$125 → zero$110$125))) (num$67$131 succ$92$68$132 zero$93$69$133 → succ$92$68$132 ((num$67$131 succ$92$68$132) zero$93$69$133)) (succ$109$84$148 zero$110$85$149 → zero$110$85$149))) (((num$67$132 succ$92$68$133 zero$93$69$134 → succ$92$68$133 ((num$67$132 succ$92$68$133) zero$93$69$134)) (succ$109$84$149 zero$110$85$150 → zero$110$85$150)) ((num1$68$127 num2$69$128 succ$70$129 zero$71$130 → (num1$68$127 succ$70$129) (num2$69$128 succ$70$129) zero$71$130) ((num$150 succ$92$151 zero$93$152 → succ$92$151 ((num$150 succ$92$151) zero$93$152)) (succ$109$167 zero$110$168 → zero$110$168))) (num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) zero$71$88) zero$71)
β > (zero$71$88 zero$71 → (((succ$109$125 zero$110$126 → zero$110$126) (((num1$68$84 num2$69$85 succ$70$86 zero$71$87 → (num1$68$84 succ$70$86) (num2$69$85 succ$70$86) zero$71$87) ((num$107 succ$92$108 zero$93$109 → succ$92$108 ((num$107 succ$92$108) zero$93$109)) (succ$109$124 zero$110$125 → zero$110$125))) (num$67$131 succ$92$68$132 zero$93$69$133 → succ$92$68$132 ((num$67$131 succ$92$68$132) zero$93$69$133)) (succ$109$84$148 zero$110$85$149 → zero$110$85$149))) (((num$67$132 succ$92$68$133 zero$93$69$134 → succ$92$68$133 ((num$67$132 succ$92$68$133) zero$93$69$134)) (succ$109$84$149 zero$110$85$150 → zero$110$85$150)) ((num1$68$127 num2$69$128 succ$70$129 zero$71$130 → (num1$68$127 succ$70$129) (num2$69$128 succ$70$129) zero$71$130) ((num$150 succ$92$151 zero$93$152 → succ$92$151 ((num$150 succ$92$151) zero$93$152)) (succ$109$167 zero$110$168 → zero$110$168))) (num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) zero$71$88) ((succ$109 zero$110 → zero$110) (((succ$109$125 zero$110$126 → zero$110$126) (((num1$68$84 num2$69$85 succ$70$86 zero$71$87 → (num1$68$84 succ$70$86) (num2$69$85 succ$70$86) zero$71$87) ((num$107 succ$92$108 zero$93$109 → succ$92$108 ((num$107 succ$92$108) zero$93$109)) (succ$109$124 zero$110$125 → zero$110$125))) (num$67$131 succ$92$68$132 zero$93$69$133 → succ$92$68$132 ((num$67$131 succ$92$68$132) zero$93$69$133)) (succ$109$84$148 zero$110$85$149 → zero$110$85$149))) (((num$67$132 succ$92$68$133 zero$93$69$134 → succ$92$68$133 ((num$67$132 succ$92$68$133) zero$93$69$134)) (succ$109$84$149 zero$110$85$150 → zero$110$85$150)) ((num1$68$127 num2$69$128 succ$70$129 zero$71$130 → (num1$68$127 succ$70$129) (num2$69$128 succ$70$129) zero$71$130) ((num$150 succ$92$151 zero$93$152 → succ$92$151 ((num$150 succ$92$151) zero$93$152)) (succ$109$167 zero$110$168 → zero$110$168))) (num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) zero$71$88)) (((num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88) zero$71)
β > (zero$71$88 zero$71 → ((((num1$68$127 num2$69$128 succ$70$129 zero$71$130 → (num1$68$127 succ$70$129) (num2$69$128 succ$70$129) zero$71$130) ((num$150 succ$92$151 zero$93$152 → succ$92$151 ((num$150 succ$92$151) zero$93$152)) (succ$109$167 zero$110$168 → zero$110$168))) (num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) ((succ$109$84$149 zero$110$85$150 → zero$110$85$150) (((num1$68$127 num2$69$128 succ$70$129 zero$71$130 → (num1$68$127 succ$70$129) (num2$69$128 succ$70$129) zero$71$130) ((num$150 succ$92$151 zero$93$152 → succ$92$151 ((num$150 succ$92$151) zero$93$152)) (succ$109$167 zero$110$168 → zero$110$168))) (num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192))) zero$71$88) (((num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88) zero$71)
β > (zero$71$88 zero$71 → (((num$150 succ$92$151 zero$93$152 → succ$92$151 ((num$150 succ$92$151) zero$93$152)) (succ$109$167 zero$110$168 → zero$110$168)) ((succ$109$84$149 zero$110$85$150 → zero$110$85$150) (((num1$68$127$86 num2$69$128$87 succ$70$129$88 zero$71$130$89 → (num1$68$127$86 succ$70$129$88) (num2$69$128$87 succ$70$129$88) zero$71$130$89) ((num$150$109 succ$92$151$110 zero$93$152$111 → succ$92$151$110 ((num$150$109 succ$92$151$110) zero$93$152$111)) (succ$109$167$126 zero$110$168$127 → zero$110$168$127))) (num$67$174$133 succ$92$68$175$134 zero$93$69$176$135 → succ$92$68$175$134 ((num$67$174$133 succ$92$68$175$134) zero$93$69$176$135)) (succ$109$84$191$150 zero$110$85$192$151 → zero$110$85$192$151))) zero$71$88) (((num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) ((succ$109$84$149 zero$110$85$150 → zero$110$85$150) (((num1$68$127$86 num2$69$128$87 succ$70$129$88 zero$71$130$89 → (num1$68$127$86 succ$70$129$88) (num2$69$128$87 succ$70$129$88) zero$71$130$89) ((num$150$109 succ$92$151$110 zero$93$152$111 → succ$92$151$110 ((num$150$109 succ$92$151$110) zero$93$152$111)) (succ$109$167$126 zero$110$168$127 → zero$110$168$127))) (num$67$174$133 succ$92$68$175$134 zero$93$69$176$135 → succ$92$68$175$134 ((num$67$174$133 succ$92$68$175$134) zero$93$69$176$135)) (succ$109$84$191$150 zero$110$85$192$151 → zero$110$85$192$151))) zero$71$88) (((num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88) zero$71)
β > (zero$71$88 zero$71 → (((succ$109$84$149 zero$110$85$150 → zero$110$85$150) (((num1$68$127$86 num2$69$128$87 succ$70$129$88 zero$71$130$89 → (num1$68$127$86 succ$70$129$88) (num2$69$128$87 succ$70$129$88) zero$71$130$89) ((num$150$109 succ$92$151$110 zero$93$152$111 → succ$92$151$110 ((num$150$109 succ$92$151$110) zero$93$152$111)) (succ$109$167$126 zero$110$168$127 → zero$110$168$127))) (num$67$174$133 succ$92$68$175$134 zero$93$69$176$135 → succ$92$68$175$134 ((num$67$174$133 succ$92$68$175$134) zero$93$69$176$135)) (succ$109$84$191$150 zero$110$85$192$151 → zero$110$85$192$151))) zero$71$88) ((succ$109$167 zero$110$168 → zero$110$168) (((succ$109$84$149 zero$110$85$150 → zero$110$85$150) (((num1$68$127$86 num2$69$128$87 succ$70$129$88 zero$71$130$89 → (num1$68$127$86 succ$70$129$88) (num2$69$128$87 succ$70$129$88) zero$71$130$89) ((num$150$109 succ$92$151$110 zero$93$152$111 → succ$92$151$110 ((num$150$109 succ$92$151$110) zero$93$152$111)) (succ$109$167$126 zero$110$168$127 → zero$110$168$127))) (num$67$174$133 succ$92$68$175$134 zero$93$69$176$135 → succ$92$68$175$134 ((num$67$174$133 succ$92$68$175$134) zero$93$69$176$135)) (succ$109$84$191$150 zero$110$85$192$151 → zero$110$85$192$151))) zero$71$88)) (((num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) ((succ$109$84$149$138 zero$110$85$150$139 → zero$110$85$150$139) (((num1$68$127$86$146 num2$69$128$87$147 succ$70$129$88$148 zero$71$130$89$149 → (num1$68$127$86$146 succ$70$129$88$148) (num2$69$128$87$147 succ$70$129$88$148) zero$71$130$89$149) ((num$150$109$169 succ$92$151$110$170 zero$93$152$111$171 → succ$92$151$110$170 ((num$150$109$169 succ$92$151$110$170) zero$93$152$111$171)) (succ$109$167$126$186 zero$110$168$127$187 → zero$110$168$127$187))) (num$67$174$133$193 succ$92$68$175$134$194 zero$93$69$176$135$195 → succ$92$68$175$134$194 ((num$67$174$133$193 succ$92$68$175$134$194) zero$93$69$176$135$195)) (succ$109$84$191$150$210 zero$110$85$192$151$211 → zero$110$85$192$151$211))) zero$71$88) (((num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88) zero$71)
β > (zero$71$88 zero$71 → zero$71$88 ((((num$67$174 succ$92$68$175 zero$93$69$176 → succ$92$68$175 ((num$67$174 succ$92$68$175) zero$93$69$176)) (succ$109$84$191 zero$110$85$192 → zero$110$85$192)) ((succ$109$84$149$138 zero$110$85$150$139 → zero$110$85$150$139) (((num1$68$127$86$146 num2$69$128$87$147 succ$70$129$88$148 zero$71$130$89$149 → (num1$68$127$86$146 succ$70$129$88$148) (num2$69$128$87$147 succ$70$129$88$148) zero$71$130$89$149) ((num$150$109$169 succ$92$151$110$170 zero$93$152$111$171 → succ$92$151$110$170 ((num$150$109$169 succ$92$151$110$170) zero$93$152$111$171)) (succ$109$167$126$186 zero$110$168$127$187 → zero$110$168$127$187))) (num$67$174$133$193 succ$92$68$175$134$194 zero$93$69$176$135$195 → succ$92$68$175$134$194 ((num$67$174$133$193 succ$92$68$175$134$194) zero$93$69$176$135$195)) (succ$109$84$191$150$210 zero$110$85$192$151$211 → zero$110$85$192$151$211))) zero$71$88) (((num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88) zero$71))
β > (zero$71$88 zero$71 → zero$71$88 ((((succ$109$84$149$138 zero$110$85$150$139 → zero$110$85$150$139) (((num1$68$127$86$146 num2$69$128$87$147 succ$70$129$88$148 zero$71$130$89$149 → (num1$68$127$86$146 succ$70$129$88$148) (num2$69$128$87$147 succ$70$129$88$148) zero$71$130$89$149) ((num$150$109$169 succ$92$151$110$170 zero$93$152$111$171 → succ$92$151$110$170 ((num$150$109$169 succ$92$151$110$170) zero$93$152$111$171)) (succ$109$167$126$186 zero$110$168$127$187 → zero$110$168$127$187))) (num$67$174$133$193 succ$92$68$175$134$194 zero$93$69$176$135$195 → succ$92$68$175$134$194 ((num$67$174$133$193 succ$92$68$175$134$194) zero$93$69$176$135$195)) (succ$109$84$191$150$210 zero$110$85$192$151$211 → zero$110$85$192$151$211))) zero$71$88) ((succ$109$84$191 zero$110$85$192 → zero$110$85$192) (((succ$109$84$149$138 zero$110$85$150$139 → zero$110$85$150$139) (((num1$68$127$86$146 num2$69$128$87$147 succ$70$129$88$148 zero$71$130$89$149 → (num1$68$127$86$146 succ$70$129$88$148) (num2$69$128$87$147 succ$70$129$88$148) zero$71$130$89$149) ((num$150$109$169 succ$92$151$110$170 zero$93$152$111$171 → succ$92$151$110$170 ((num$150$109$169 succ$92$151$110$170) zero$93$152$111$171)) (succ$109$167$126$186 zero$110$168$127$187 → zero$110$168$127$187))) (num$67$174$133$193 succ$92$68$175$134$194 zero$93$69$176$135$195 → succ$92$68$175$134$194 ((num$67$174$133$193 succ$92$68$175$134$194) zero$93$69$176$135$195)) (succ$109$84$191$150$210 zero$110$85$192$151$211 → zero$110$85$192$151$211))) zero$71$88)) (((num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88) zero$71))
β > (zero$71$88 zero$71 → zero$71$88 (zero$71$88 ((((num$67 succ$92$68 zero$93$69 → succ$92$68 ((num$67 succ$92$68) zero$93$69)) (succ$109$84 zero$110$85 → zero$110$85)) ((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88) zero$71)))
β > (zero$71$88 zero$71 → zero$71$88 (zero$71$88 ((((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88) ((succ$109$84 zero$110$85 → zero$110$85) (((succ$109$125$236 zero$110$126$237 → zero$110$126$237) (((num1$68$84$244 num2$69$85$245 succ$70$86$246 zero$71$87$247 → (num1$68$84$244 succ$70$86$246) (num2$69$85$245 succ$70$86$246) zero$71$87$247) ((num$107$267 succ$92$108$268 zero$93$109$269 → succ$92$108$268 ((num$107$267 succ$92$108$268) zero$93$109$269)) (succ$109$124$284 zero$110$125$285 → zero$110$125$285))) (num$67$131$291 succ$92$68$132$292 zero$93$69$133$293 → succ$92$68$132$292 ((num$67$131$291 succ$92$68$132$292) zero$93$69$133$293)) (succ$109$84$148$308 zero$110$85$149$309 → zero$110$85$149$309))) (((num$67$132$317 succ$92$68$133$318 zero$93$69$134$319 → succ$92$68$133$318 ((num$67$132$317 succ$92$68$133$318) zero$93$69$134$319)) (succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335)) ((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) zero$71$88)) zero$71)))
β > (zero$71$88 zero$71 → zero$71$88 (zero$71$88 (((((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) ((succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335) (((num1$68$127$342 num2$69$128$343 succ$70$129$344 zero$71$130$345 → (num1$68$127$342 succ$70$129$344) (num2$69$128$343 succ$70$129$344) zero$71$130$345) ((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383))) (num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407))) zero$71$88) zero$71)))
β > (zero$71$88 zero$71 → zero$71$88 (zero$71$88 ((((num$150$365 succ$92$151$366 zero$93$152$367 → succ$92$151$366 ((num$150$365 succ$92$151$366) zero$93$152$367)) (succ$109$167$382 zero$110$168$383 → zero$110$168$383)) ((succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335) (((num1$68$127$342$92 num2$69$128$343$93 succ$70$129$344$94 zero$71$130$345$95 → (num1$68$127$342$92 succ$70$129$344$94) (num2$69$128$343$93 succ$70$129$344$94) zero$71$130$345$95) ((num$150$365$115 succ$92$151$366$116 zero$93$152$367$117 → succ$92$151$366$116 ((num$150$365$115 succ$92$151$366$116) zero$93$152$367$117)) (succ$109$167$382$132 zero$110$168$383$133 → zero$110$168$383$133))) (num$67$174$389$139 succ$92$68$175$390$140 zero$93$69$176$391$141 → succ$92$68$175$390$140 ((num$67$174$389$139 succ$92$68$175$390$140) zero$93$69$176$391$141)) (succ$109$84$191$406$156 zero$110$85$192$407$157 → zero$110$85$192$407$157))) zero$71$88) (((num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) ((succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335) (((num1$68$127$342$92 num2$69$128$343$93 succ$70$129$344$94 zero$71$130$345$95 → (num1$68$127$342$92 succ$70$129$344$94) (num2$69$128$343$93 succ$70$129$344$94) zero$71$130$345$95) ((num$150$365$115 succ$92$151$366$116 zero$93$152$367$117 → succ$92$151$366$116 ((num$150$365$115 succ$92$151$366$116) zero$93$152$367$117)) (succ$109$167$382$132 zero$110$168$383$133 → zero$110$168$383$133))) (num$67$174$389$139 succ$92$68$175$390$140 zero$93$69$176$391$141 → succ$92$68$175$390$140 ((num$67$174$389$139 succ$92$68$175$390$140) zero$93$69$176$391$141)) (succ$109$84$191$406$156 zero$110$85$192$407$157 → zero$110$85$192$407$157))) zero$71$88) zero$71)))
β > (zero$71$88 zero$71 → zero$71$88 (zero$71$88 ((((succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335) (((num1$68$127$342$92 num2$69$128$343$93 succ$70$129$344$94 zero$71$130$345$95 → (num1$68$127$342$92 succ$70$129$344$94) (num2$69$128$343$93 succ$70$129$344$94) zero$71$130$345$95) ((num$150$365$115 succ$92$151$366$116 zero$93$152$367$117 → succ$92$151$366$116 ((num$150$365$115 succ$92$151$366$116) zero$93$152$367$117)) (succ$109$167$382$132 zero$110$168$383$133 → zero$110$168$383$133))) (num$67$174$389$139 succ$92$68$175$390$140 zero$93$69$176$391$141 → succ$92$68$175$390$140 ((num$67$174$389$139 succ$92$68$175$390$140) zero$93$69$176$391$141)) (succ$109$84$191$406$156 zero$110$85$192$407$157 → zero$110$85$192$407$157))) zero$71$88) ((succ$109$167$382 zero$110$168$383 → zero$110$168$383) (((succ$109$84$149$334 zero$110$85$150$335 → zero$110$85$150$335) (((num1$68$127$342$92 num2$69$128$343$93 succ$70$129$344$94 zero$71$130$345$95 → (num1$68$127$342$92 succ$70$129$344$94) (num2$69$128$343$93 succ$70$129$344$94) zero$71$130$345$95) ((num$150$365$115 succ$92$151$366$116 zero$93$152$367$117 → succ$92$151$366$116 ((num$150$365$115 succ$92$151$366$116) zero$93$152$367$117)) (succ$109$167$382$132 zero$110$168$383$133 → zero$110$168$383$133))) (num$67$174$389$139 succ$92$68$175$390$140 zero$93$69$176$391$141 → succ$92$68$175$390$140 ((num$67$174$389$139 succ$92$68$175$390$140) zero$93$69$176$391$141)) (succ$109$84$191$406$156 zero$110$85$192$407$157 → zero$110$85$192$407$157))) zero$71$88)) (((num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) ((succ$109$84$149$334$144 zero$110$85$150$335$145 → zero$110$85$150$335$145) (((num1$68$127$342$92$152 num2$69$128$343$93$153 succ$70$129$344$94$154 zero$71$130$345$95$155 → (num1$68$127$342$92$152 succ$70$129$344$94$154) (num2$69$128$343$93$153 succ$70$129$344$94$154) zero$71$130$345$95$155) ((num$150$365$115$175 succ$92$151$366$116$176 zero$93$152$367$117$177 → succ$92$151$366$116$176 ((num$150$365$115$175 succ$92$151$366$116$176) zero$93$152$367$117$177)) (succ$109$167$382$132$192 zero$110$168$383$133$193 → zero$110$168$383$133$193))) (num$67$174$389$139$199 succ$92$68$175$390$140$200 zero$93$69$176$391$141$201 → succ$92$68$175$390$140$200 ((num$67$174$389$139$199 succ$92$68$175$390$140$200) zero$93$69$176$391$141$201)) (succ$109$84$191$406$156$216 zero$110$85$192$407$157$217 → zero$110$85$192$407$157$217))) zero$71$88) zero$71)))
β > (zero$71$88 zero$71 → zero$71$88 (zero$71$88 (zero$71$88 ((((num$67$174$389 succ$92$68$175$390 zero$93$69$176$391 → succ$92$68$175$390 ((num$67$174$389 succ$92$68$175$390) zero$93$69$176$391)) (succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407)) ((succ$109$84$149$334$144 zero$110$85$150$335$145 → zero$110$85$150$335$145) (((num1$68$127$342$92$152 num2$69$128$343$93$153 succ$70$129$344$94$154 zero$71$130$345$95$155 → (num1$68$127$342$92$152 succ$70$129$344$94$154) (num2$69$128$343$93$153 succ$70$129$344$94$154) zero$71$130$345$95$155) ((num$150$365$115$175 succ$92$151$366$116$176 zero$93$152$367$117$177 → succ$92$151$366$116$176 ((num$150$365$115$175 succ$92$151$366$116$176) zero$93$152$367$117$177)) (succ$109$167$382$132$192 zero$110$168$383$133$193 → zero$110$168$383$133$193))) (num$67$174$389$139$199 succ$92$68$175$390$140$200 zero$93$69$176$391$141$201 → succ$92$68$175$390$140$200 ((num$67$174$389$139$199 succ$92$68$175$390$140$200) zero$93$69$176$391$141$201)) (succ$109$84$191$406$156$216 zero$110$85$192$407$157$217 → zero$110$85$192$407$157$217))) zero$71$88) zero$71))))
β > (zero$71$88 zero$71 → zero$71$88 (zero$71$88 (zero$71$88 ((((succ$109$84$149$334$144 zero$110$85$150$335$145 → zero$110$85$150$335$145) (((num1$68$127$342$92$152 num2$69$128$343$93$153 succ$70$129$344$94$154 zero$71$130$345$95$155 → (num1$68$127$342$92$152 succ$70$129$344$94$154) (num2$69$128$343$93$153 succ$70$129$344$94$154) zero$71$130$345$95$155) ((num$150$365$115$175 succ$92$151$366$116$176 zero$93$152$367$117$177 → succ$92$151$366$116$176 ((num$150$365$115$175 succ$92$151$366$116$176) zero$93$152$367$117$177)) (succ$109$167$382$132$192 zero$110$168$383$133$193 → zero$110$168$383$133$193))) (num$67$174$389$139$199 succ$92$68$175$390$140$200 zero$93$69$176$391$141$201 → succ$92$68$175$390$140$200 ((num$67$174$389$139$199 succ$92$68$175$390$140$200) zero$93$69$176$391$141$201)) (succ$109$84$191$406$156$216 zero$110$85$192$407$157$217 → zero$110$85$192$407$157$217))) zero$71$88) ((succ$109$84$191$406 zero$110$85$192$407 → zero$110$85$192$407) (((succ$109$84$149$334$144 zero$110$85$150$335$145 → zero$110$85$150$335$145) (((num1$68$127$342$92$152 num2$69$128$343$93$153 succ$70$129$344$94$154 zero$71$130$345$95$155 → (num1$68$127$342$92$152 succ$70$129$344$94$154) (num2$69$128$343$93$153 succ$70$129$344$94$154) zero$71$130$345$95$155) ((num$150$365$115$175 succ$92$151$366$116$176 zero$93$152$367$117$177 → succ$92$151$366$116$176 ((num$150$365$115$175 succ$92$151$366$116$176) zero$93$152$367$117$177)) (succ$109$167$382$132$192 zero$110$168$383$133$193 → zero$110$168$383$133$193))) (num$67$174$389$139$199 succ$92$68$175$390$140$200 zero$93$69$176$391$141$201 → succ$92$68$175$390$140$200 ((num$67$174$389$139$199 succ$92$68$175$390$140$200) zero$93$69$176$391$141$201)) (succ$109$84$191$406$156$216 zero$110$85$192$407$157$217 → zero$110$85$192$407$157$217))) zero$71$88)) zero$71))))
β > (zero$71$88 zero$71 → zero$71$88 (zero$71$88 (zero$71$88 (zero$71$88 zero$71))))
Natural number detected: 4