let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being 0 -started State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds
Times (a,I) is_halting_on s,p
let s be 0 -started State of SCM+FSA; :: thesis: for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds
Times (a,I) is_halting_on s,p
let I be really-closed good InitHalting MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds
Times (a,I) is_halting_on s,p
let a be read-write Int-Location; :: thesis: ( not I destroys a & s . (intloc 0) = 1 implies Times (a,I) is_halting_on s,p )
assume A1: not I destroys a ; :: thesis: ( not s . (intloc 0) = 1 or Times (a,I) is_halting_on s,p )
assume A2: s . (intloc 0) = 1 ; :: thesis: Times (a,I) is_halting_on s,p
ProperTimesBody a,I,s,p
proof
let k be Nat; :: according to SCMFSA9A:def 9 :: thesis: ( s . a <= k or I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) )
assume k < s . a ; :: 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, A2, Lm3; :: thesis: verum
end;
hence Times (a,I) is_halting_on s,p by A1, A2, SCMFSA9A:55; :: thesis: verum