let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I, J being really-closed InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location holds
( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
let s be State of SCM+FSA; for I, J being really-closed InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location holds
( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
let I, J be really-closed InitHalting MacroInstruction of SCM+FSA ; for a being read-write Int-Location holds
( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
let a be read-write Int-Location; ( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
now for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
for p being Instruction-Sequence of SCM+FSA st if=0 (a,I,J) c= p holds
p halts_on slet s be
State of
SCM+FSA;
( Initialize ((intloc 0) .--> 1) c= s implies for p being Instruction-Sequence of SCM+FSA st if=0 (a,I,J) c= p holds
b3 halts_on b2 )assume
Initialize ((intloc 0) .--> 1) c= s
;
for p being Instruction-Sequence of SCM+FSA st if=0 (a,I,J) c= p holds
b3 halts_on b2then A1:
s = Initialized s
by FUNCT_4:98;
let p be
Instruction-Sequence of
SCM+FSA;
( if=0 (a,I,J) c= p implies b2 halts_on b1 )assume
if=0 (
a,
I,
J)
c= p
;
b2 halts_on b1then A2:
p = p +* (if=0 (a,I,J))
by FUNCT_4:98;
A3:
J is_halting_onInit s,
p
by Th23;
A4:
I is_halting_onInit s,
p
by Th23;
end;
hence
if=0 (a,I,J) is InitHalting
; ( ( s . a = 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
I is_halting_onInit s,p
by Th23;
hence
( s . a = 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
by Th30; ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
J is_halting_onInit s,p
by Th23;
hence
( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
by Th32; verum