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
for k being Nat holds
( ((StepTimes (a,I,p,s)) . k) . (intloc 0) = 1 & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) )
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
for k being Nat holds
( ((StepTimes (a,I,p,s)) . k) . (intloc 0) = 1 & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) )
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
for k being Nat holds
( ((StepTimes (a,I,p,s)) . k) . (intloc 0) = 1 & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) )
let a be read-write Int-Location; :: thesis: ( not I destroys a & s . (intloc 0) = 1 implies for k being Nat holds
( ((StepTimes (a,I,p,s)) . k) . (intloc 0) = 1 & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) ) )
assume that
A1: not I destroys a and
A2: s . (intloc 0) = 1 ; :: thesis: for k being Nat holds
( ((StepTimes (a,I,p,s)) . k) . (intloc 0) = 1 & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) )
defpred S₁[ Nat] means ( ((StepTimes (a,I,p,s)) . $1) . (intloc 0) = 1 & I is_halting_on (StepTimes (a,I,p,s)) . $1,p +* (Times (a,I)) );
A3: S₁[ 0 ]

proof

A4: (StepTimes (a,I,p,s)) . 0 = Initialized s by SCMFSA_9:def 5;
(Initialized s) . (intloc 0) = 1 by SCMFSA_M:5
.= s . (intloc 0) by A2 ;
hence A5: ((StepTimes (a,I,p,s)) . 0) . (intloc 0) = 1 by A4, A2; :: thesis: I is_halting_on (StepTimes (a,I,p,s)) . 0,p +* (Times (a,I))
intloc 0 in dom ((StepTimes (a,I,p,s)) . 0) by SCMFSA_2:42;
then (intloc 0) .--> 1 c= (StepTimes (a,I,p,s)) . 0 by A5, FUNCOP_1:84;
then A6: Initialize ((intloc 0) .--> 1) c= Initialize ((StepTimes (a,I,p,s)) . 0) by FUNCT_4:123;
I c= (p +* (Times (a,I))) +* I by FUNCT_4:25;
hence (p +* (Times (a,I))) +* I halts_on Initialize ((StepTimes (a,I,p,s)) . 0) by A6, Def1; :: according to SCMFSA7B:def 6 :: thesis: verum

end;

A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus A9: ((StepTimes (a,I,p,s)) . (k + 1)) . (intloc 0) = 1 by A8, A1, SCMFSA9A:48; :: thesis: I is_halting_on (StepTimes (a,I,p,s)) . (k + 1),p +* (Times (a,I))
intloc 0 in dom ((StepTimes (a,I,p,s)) . (k + 1)) by SCMFSA_2:42;
then (intloc 0) .--> 1 c= (StepTimes (a,I,p,s)) . (k + 1) by A9, FUNCOP_1:84;
then A10: Initialize ((intloc 0) .--> 1) c= Initialize ((StepTimes (a,I,p,s)) . (k + 1)) by FUNCT_4:123;
I c= (p +* (Times (a,I))) +* I by FUNCT_4:25;
hence (p +* (Times (a,I))) +* I halts_on Initialize ((StepTimes (a,I,p,s)) . (k + 1)) by A10, Def1; :: according to SCMFSA7B:def 6 :: thesis: verum

end;

thus for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A7); :: thesis: verum