let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for F being NAT -defined the Instructions of b₁ -valued total Function
for s being State of S
for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N; :: thesis: for F being NAT -defined the Instructions of S -valued total Function
for s being State of S
for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
let F be NAT -defined the Instructions of S -valued total Function; :: thesis: for s being State of S
for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
let s be State of S; :: thesis: for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
let k be Element of NAT ; :: thesis: ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
YY: dom F = NAT by PARTFUN1:def 4;
then XX: IC (Comput (F,s,k)) in dom F ;
XX1: IC (Comput (F,s,(k + 1))) in dom F by YY;

hereby :: thesis: ( LifeSpan (F,s) = k + 1 & F halts_on s implies ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) )

assume that
A1: F . (IC (Comput (F,s,k))) <> halt S and
A2: F . (IC (Comput (F,s,(k + 1)))) = halt S ; :: thesis: ( LifeSpan (F,s) = k + 1 & F halts_on s )
A3: CurInstr (F,(Comput (F,s,k))) <> halt S by A1, PARTFUN1:def 8, XX;

A4: now

let i be Element of NAT ; :: thesis: ( CurInstr (F,(Comput (F,s,i))) = halt S implies not k + 1 > i )
assume that
A5: CurInstr (F,(Comput (F,s,i))) = halt S and
A6: k + 1 > i ; :: thesis: contradiction
i <= k by A6, NAT_1:13;
hence contradiction by A3, A5, Th6; :: thesis: verum

end;

X1: F halts_on s by A2, Th31;
CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A2, PARTFUN1:def 8, XX1;
hence ( LifeSpan (F,s) = k + 1 & F halts_on s ) by A4, Def46, X1; :: thesis: verum

end;

assume A7: ( LifeSpan (F,s) = k + 1 & F halts_on s ) ; :: thesis: ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S )

A8: now

assume CurInstr (F,(Comput (F,s,k))) = halt S ; :: thesis: contradiction
then k + 1 <= k by A7, Def46;
hence contradiction by NAT_1:13; :: thesis: verum

end;

CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A7, Def46;
hence ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) by A8, PARTFUN1:def 8, XX, XX1; :: thesis: verum