Accelerator.SM86.Operands

75def sm86RegisterRun =
76  (lambda unrestricted register : (family SM86Register) .
77    (lambda unrestricted count : Nat .
78      (lambda unrestricted rest : (family StdList Nat) .
79        (let unrestricted index = (sm86RegisterIndex register) in
80        (nat-eliminate
81          (lambda unrestricted current : Nat . (family StdList Nat))
82          rest
83          (lambda unrestricted named : Nat . (lambda unrestricted ignored : (family StdList Nat) .
84            (nat-eliminate
85              (lambda unrestricted current : Nat . (family StdList Nat))
86              rest
87              (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdList Nat) .
88                (constructor StdList StdListCons Nat
89                  (nat-add index (nat-subtract (nat-subtract count 1) predecessor))
90                  induction)))
91              count)))
92          (nat-add (nat-less-than index sm86RegisterZero) (nat-less-than sm86RegisterZero index)))))))