The joins of `placed` (the last op first), from its words alone: a BRA
and the position its sm_121 displacement lands on.
2330def sm121LowerJoinsOf =
2331 (lambda unrestricted placed : (family SM121LowerOps) .
2332 (eliminate
2333 SM121LowerOps
2334 (lambda unrestricted current : (family SM121LowerOps) . (family SM121LowerJoins))
2335 placed
2336 (branch SM121LowerOpsEnd .
2337 (constructor SM121LowerJoins SM121LowerJoinsValue zero sm121LowerNone zero))
2338 (branch SM121LowerOpsNext last earlier induction .
2339 (eliminate
2340 SM121LowerJoins
2341 (lambda unrestricted current : (family SM121LowerJoins) . (family SM121LowerJoins))
2342 induction
2343 (branch SM121LowerJoinsValue position joins bad .
2344 (eliminate
2345 SM121LowerOp
2346 (lambda unrestricted current : (family SM121LowerOp) . (family SM121LowerJoins))
2347 last
2348 (branch SM121LowerOpValue low high class reads writes predicateReads predicateWrites constantLoad label join target .
2349 (let unrestricted encoded =
2350 (nat-add
2351 (nat-add
2352 (sm121LowerField low sm121LowerBranchLowPlace sm121LowerRegisterSpan)
2353 (nat-multiply (sm121LowerField low sm121LowerBranchMiddlePlace sm121LowerBranchMiddleSpan)
2354 sm121LowerRegisterSpan))
2355 (nat-multiply (sm121LowerField high 1 sm121LowerBranchHighSpan)
2356 (nat-multiply sm121LowerRegisterSpan sm121LowerBranchMiddleSpan))) in
2357 (let unrestricted next = (succ position) in
2358 (let unrestricted forward = (nat-less-than encoded (nat-divide sm121LowerBranchWordSpan 2)) in
2359 (let unrestricted words =
2360 (naturalSelect forward encoded (nat-subtract sm121LowerBranchWordSpan encoded)) in
2361 (let unrestricted aligned =
2362 (naturalIsZero (nat-modulo words sm121LowerBranchUnit)) in
2363 (let unrestricted distance = (nat-divide words sm121LowerBranchUnit) in
2364 (let unrestricted inside = (naturalOr forward (naturalIsZero (nat-less-than next distance))) in
2365 (let unrestricted landing =
2366 (naturalSelect forward (nat-add next distance) (nat-subtract next distance)) in
2367 (sm121LowerSelect (family SM121LowerJoins)
2368 (naturalEqual (nat-modulo low sm121LowerOpcodeSpan) sm121LowerOpcodeBranch)
2369 (constructor SM121LowerJoins SM121LowerJoinsValue
2370 next
2371 (sm121LowerCons position (sm121LowerCons landing joins))
2372 (naturalSelect (naturalAnd aligned inside) bad (succ bad)))
2373 (constructor SM121LowerJoins SM121LowerJoinsValue next joins bad)))))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.