`a`'s instructions with `b`'s interleaved: one of `b` after every `every`
of `a` (the first after `every`), the rest of either after the other ends
1088def sfpInterleaveFrom = (lambda unrestricted every : Nat . (lambda unrestricted a : (family SM86Program) .
1089 (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . (pi unrestricted b : (family SM86Program) . (pi unrestricted n : Nat . (family SM86Program)))) a
1090 (branch SM86ProgramEnd . (lambda unrestricted b : (family SM86Program) . (lambda unrestricted n : Nat . b)))
1091 (branch SM86ProgramNext instruction rest induction .
1092 (lambda unrestricted b : (family SM86Program) . (lambda unrestricted n : Nat .
1093 (nat-eliminate (lambda unrestricted m : Nat . (family SM86Program))
1094 (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . (family SM86Program)) b
1095 (branch SM86ProgramEnd . (constructor SM86Program SM86ProgramNext instruction (induction b every)))
1096 (branch SM86ProgramNext bInstruction bRest bInduction .
1097 (constructor SM86Program SM86ProgramNext bInstruction
1098 (constructor SM86Program SM86ProgramNext instruction (induction bRest every)))))
1099 (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family SM86Program) .
1100 (constructor SM86Program SM86ProgramNext instruction (induction b p))))
1101 n)))))))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.