let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for l being Nat
for p being FinPartState of S st p = (IC S),l --> l,(halt S) holds
p is halting
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N; :: thesis: for l being Nat
for p being FinPartState of S st p = (IC S),l --> l,(halt S) holds
p is halting
let l be Nat; :: thesis: for p being FinPartState of S st p = (IC S),l --> l,(halt S) holds
p is halting
set h = halt S;
let p be FinPartState of S; :: thesis: ( p = (IC S),l --> l,(halt S) implies p is halting )
assume Z: p = (IC S),l --> l,(halt S) ; :: thesis: p is halting
let s be State of S; :: according to AMI_1:def 26 :: thesis: ( p c= s implies ProgramPart s halts_on s )
assume A3: p c= s ; :: thesis: ProgramPart s halts_on s
take 0 ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput (ProgramPart s),s,0 ) in dom (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,0 )) = halt S )
IC (Comput (ProgramPart s),s,0 ) in NAT ;
hence IC (Comput (ProgramPart s),s,0 ) in dom (ProgramPart s) by LmU; :: thesis: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,0 )) = halt S
u: Comput (ProgramPart s),s,0 = s by Th13;
CurInstr (ProgramPart (Comput (ProgramPart s),s,0 )),(Comput (ProgramPart s),s,0 ) = CurInstr (ProgramPart s),s by u
.= halt S by A3, Th64, Z ;
hence (ProgramPart s) /. (IC (Comput (ProgramPart s),s,0 )) = halt S by LmX; :: thesis: verum