Runtime.NativePhysicalProgramComposer

892def nativePhysicalProgramComposeRelocateCommands =
893  (lambda unrestricted commands : (family NativePhysicalCommands) .
894    (lambda unrestricted stateBase : (family ModelWord64) .
895      (lambda unrestricted resultBase : (family ModelWord64) .
896        (lambda unrestricted payloadBase : (family ModelWord64) .
897          (eliminate NativePhysicalCommands
898            (lambda unrestricted current : (family NativePhysicalCommands) .
899              (family NativePhysicalProgramComposeCommandsResult))
900            commands
901            (branch NativePhysicalCommandsEnd .
902              (constructor NativePhysicalProgramComposeCommandsResult
903                NativePhysicalProgramComposeCommandsRelocated
904                (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
905                zero zero zero zero))
906            (branch NativePhysicalCommandsNext head tail induction .
907              (eliminate NativePhysicalCommand
908                (lambda unrestricted current : (family NativePhysicalCommand) .
909                  (family NativePhysicalProgramComposeCommandsResult))
910                head
911                (branch NativePhysicalCommandValue operation errorIdentity .
912                  (eliminate NativePhysicalProgramComposeOperationResult
913                    (lambda unrestricted current :
914                      (family NativePhysicalProgramComposeOperationResult) .
915                      (family NativePhysicalProgramComposeCommandsResult))
916                    (app (app (app (app nativePhysicalProgramComposeRelocateOperation operation)
917                      stateBase) resultBase) payloadBase)
918                    (branch NativePhysicalProgramComposeOperationRelocated
919                      relocatedOperation n0 c0 .
920                      (eliminate NativePhysicalProgramComposeCommandsResult
921                        (lambda unrestricted current :
922                          (family NativePhysicalProgramComposeCommandsResult) .
923                          (family NativePhysicalProgramComposeCommandsResult))
924                        induction
925                        (branch NativePhysicalProgramComposeCommandsRelocated
926                          relocatedTail commandsDone operationsDone operandsDone checksDone .
927                          (constructor NativePhysicalProgramComposeCommandsResult
928                            NativePhysicalProgramComposeCommandsRelocated
929                            (constructor NativePhysicalCommands NativePhysicalCommandsNext
930                              (constructor NativePhysicalCommand NativePhysicalCommandValue
931                                relocatedOperation errorIdentity)
932                              relocatedTail)
933                            (succ commandsDone) (succ operationsDone)
934                            (app (app naturalAdd n0) operandsDone)
935                            (app (app naturalAdd c0) checksDone)))
936                        (branch NativePhysicalProgramComposeCommandsRejected
937                          error commandsDone operationsDone operandsDone checksDone .
938                          (constructor NativePhysicalProgramComposeCommandsResult
939                            NativePhysicalProgramComposeCommandsRejected error
940                            (succ commandsDone) (succ operationsDone)
941                            (app (app naturalAdd n0) operandsDone)
942                            (app (app naturalAdd c0) checksDone)))))
943                    (branch NativePhysicalProgramComposeOperationRejected error n c .
944                      (constructor NativePhysicalProgramComposeCommandsResult
945                        NativePhysicalProgramComposeCommandsRejected
946                        error zero zero n c)))))))))))