1015def nativePhysicalProgramComposeStripTrainingHalt =
1016 (lambda unrestricted commands : (family NativePhysicalCommands) .
1017 (eliminate NativePhysicalCommands
1018 (lambda unrestricted current : (family NativePhysicalCommands) .
1019 (family NativePhysicalProgramComposeStripResult))
1020 commands
1021 (branch NativePhysicalCommandsEnd .
1022 (constructor NativePhysicalProgramComposeStripResult
1023 NativePhysicalProgramComposeStripEmpty))
1024 (branch NativePhysicalCommandsNext head tail induction .
1025 (eliminate NativePhysicalProgramComposeStripResult
1026 (lambda unrestricted current :
1027 (family NativePhysicalProgramComposeStripResult) .
1028 (family NativePhysicalProgramComposeStripResult))
1029 induction
1030 (branch NativePhysicalProgramComposeStripEmpty .
1031 (nat-eliminate
1032 (lambda unrestricted isHalt : Nat .
1033 (family NativePhysicalProgramComposeStripResult))
1034 (constructor NativePhysicalProgramComposeStripResult
1035 NativePhysicalProgramComposeStripRejected
1036 (constructor NativePhysicalProgramComposeErrorCode
1037 NativePhysicalProgramComposeTrainingHaltMissing)
1038 (succ zero))
1039 (lambda unrestricted predecessor : Nat .
1040 (lambda unrestricted ignored :
1041 (family NativePhysicalProgramComposeStripResult) .
1042 (constructor NativePhysicalProgramComposeStripResult
1043 NativePhysicalProgramComposeStripSucceeded
1044 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
1045 zero)))
1046 (app nativePhysicalProgramComposeCommandIsHalt head)))
1047 (branch NativePhysicalProgramComposeStripSucceeded stripped count .
1048 (nat-eliminate
1049 (lambda unrestricted isHalt : Nat .
1050 (family NativePhysicalProgramComposeStripResult))
1051 (constructor NativePhysicalProgramComposeStripResult
1052 NativePhysicalProgramComposeStripSucceeded
1053 (constructor NativePhysicalCommands NativePhysicalCommandsNext
1054 (nativePhysicalProgramComposeRemoveFinalHaltJump (succ count) head) stripped)
1055 (succ count))
1056 (lambda unrestricted predecessor : Nat .
1057 (lambda unrestricted ignored :
1058 (family NativePhysicalProgramComposeStripResult) .
1059 (constructor NativePhysicalProgramComposeStripResult
1060 NativePhysicalProgramComposeStripRejected
1061 (constructor NativePhysicalProgramComposeErrorCode
1062 NativePhysicalProgramComposeTrainingHaltNotFinal)
1063 (succ count))))
1064 (app nativePhysicalProgramComposeCommandIsHalt head)))
1065 (branch NativePhysicalProgramComposeStripRejected error visited . induction)))))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.