let p be Instruction-Sequence of SCM+FSA; 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; 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 ; 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; ( 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
; 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 S1[ 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:
S1[ 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;
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;
SCMFSA7B:def 6 verum
end;
A7:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A8:
S1[
k]
;
S1[k + 1]
thus A9:
((StepTimes (a,I,p,s)) . (k + 1)) . (intloc 0) = 1
by A8, A1, SCMFSA9A:48;
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;
SCMFSA7B:def 6 verum
end;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A3, A7); verum