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 ) )
A1: dom F = NAT by PARTFUN1:def 4;

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
A2: F . (IC (Comput (F,s,k))) <> halt S and
A3: F . (IC (Comput (F,s,(k + 1)))) = halt S ; :: thesis: ( LifeSpan (F,s) = k + 1 & F halts_on s )
A4: CurInstr (F,(Comput (F,s,k))) <> halt S by A2, PARTFUN1:def 8, A1;

A5: now

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

end;

A8: F halts_on s by A3, Th31;
CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A3, PARTFUN1:def 8, A1;
hence ( LifeSpan (F,s) = k + 1 & F halts_on s ) by A5, Def14, A8; :: thesis: verum

end;

assume A9: ( 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 )

A10: now

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

end;

CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A9, Def14;
hence ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) by A10, PARTFUN1:def 8, A1; :: thesis: verum