let s be State of SCMPDS ; :: thesis: ( s is halting implies for k being Element of NAT st LifeSpan s <= k holds
CurInstr (Computation s,k) = halt SCMPDS )
assume A1: s is halting ; :: thesis: for k being Element of NAT st LifeSpan s <= k holds
CurInstr (Computation s,k) = halt SCMPDS
let k be Element of NAT ; :: thesis: ( LifeSpan s <= k implies CurInstr (Computation s,k) = halt SCMPDS )
assume A2: LifeSpan s <= k ; :: thesis: CurInstr (Computation s,k) = halt SCMPDS
CurInstr (Computation s,(LifeSpan s)) = halt SCMPDS by A1, AMI_1:def 46;
hence CurInstr (Computation s,k) = halt SCMPDS by A2, AMI_1:52; :: thesis: verum