1635def sm121LowerPendingRemove =
1636 (lambda unrestricted pending : (family SM121LowerPending) .
1637 (lambda unrestricted register : Nat .
1638 (eliminate
1639 SM121LowerPending
1640 (lambda unrestricted current : (family SM121LowerPending) . (family SM121LowerPending))
1641 pending
1642 (branch SM121LowerPendingEnd . sm121LowerPendingNone)
1643 (branch SM121LowerPendingNext entry time class tail induction .
1644 (nat-eliminate (lambda unrestricted current : Nat . (family SM121LowerPending))
1645 (constructor SM121LowerPending SM121LowerPendingNext entry time class induction)
1646 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : (family SM121LowerPending) . induction))
1647 (nat-eliminate (lambda unrestricted current : Nat . Nat)
1648 (nat-eliminate (lambda unrestricted current : Nat . Nat)
1649 (succ zero)
1650 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero))
1651 (nat-less-than register entry))
1652 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero))
1653 (nat-less-than entry register)))))))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.