let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being Program of SCM+FSA st I is parahalting holds
ProperTimesBody a,I,s,p
let p be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for I being Program of SCM+FSA st I is parahalting holds
ProperTimesBody a,I,s,p
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA st I is parahalting holds
ProperTimesBody a,I,s,p
let I be Program of SCM+FSA; :: thesis: ( I is parahalting implies ProperTimesBody a,I,s,p )
assume A1: I is parahalting ; :: thesis: ProperTimesBody a,I,s,p
then reconsider I9 = I as parahalting Program of SCM+FSA ;
let k be Element of NAT ; :: according to SFMASTR2:def 4 :: thesis: ( k < s . a implies ( I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) ) )
assume k < s . a ; :: thesis: ( I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) )
I9 is paraclosed ;
hence I is_closed_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) by SCMFSA7B:18; :: thesis: I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I))
thus I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) by A1, SCMFSA7B:19; :: thesis: verum