Accelerator.SM121.Lowering

891def sm121LowerMaskInsert =
892  (lambda unrestricted mask : (family SM121LowerMask) .
893    (lambda unrestricted register : Nat .
894      (eliminate
895        SM121LowerMask
896        (lambda unrestricted current : (family SM121LowerMask) . (family SM121LowerMask))
897        mask
898        (branch SM121LowerMaskValue w0 w1 w2 w3 .
899          (let unrestricted index = (nat-divide register sm121LowerMaskWordBits) in
900          (let unrestricted bit = (nat-modulo register sm121LowerMaskWordBits) in
901            (constructor SM121LowerMask SM121LowerMaskValue
902              (nat-eliminate (lambda unrestricted current : Nat . Nat)
903                w0
904                (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (sm121LowerMaskSet w0 bit)))
905                (naturalEqual index zero))
906              (nat-eliminate (lambda unrestricted current : Nat . Nat)
907                w1
908                (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (sm121LowerMaskSet w1 bit)))
909                (naturalEqual index 1))
910              (nat-eliminate (lambda unrestricted current : Nat . Nat)
911                w2
912                (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (sm121LowerMaskSet w2 bit)))
913                (naturalEqual index 2))
914              (nat-eliminate (lambda unrestricted current : Nat . Nat)
915                w3
916                (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (sm121LowerMaskSet w3 bit)))
917                (naturalEqual index 3)))))))))