let p be Instruction-Sequence of SCM+FSA; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 :: thesis: 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 s
let s be State of SCM+FSA; :: thesis: ( 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 ; :: thesis: for p being Instruction-Sequence of SCM+FSA st if>0 (a,I,J) c= p holds
b3 halts_on b2
then A1: s = Initialized s by FUNCT_4:98;
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( if>0 (a,I,J) c= p implies b2 halts_on b1 )
assume if>0 (a,I,J) c= p ; :: thesis: b2 halts_on b1
then 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;
per cases ( s . a > 0 or s . a <= 0 ) ;
end;
end;
hence if>0 (a,I,J) is InitHalting ; :: thesis: ( ( 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 Th36; :: thesis: ( 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 Th38; :: thesis: verum