let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for l being Nat
for p being PartState of S st p = (IC S),l --> l,(halt S) holds
p is halting
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N; :: thesis: for l being Nat
for p being PartState of S st p = (IC S),l --> l,(halt S) holds
p is halting
let l be Nat; :: thesis: for p being PartState of S st p = (IC S),l --> l,(halt S) holds
p is halting
set h = halt S;
let p be PartState 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) & CurInstr (ProgramPart s),(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 COMPOS_1:34; :: thesis: CurInstr (ProgramPart s),(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, Z, COMPOS_1:6 ;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,0 ) = halt S by u; :: thesis: verum