let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being 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 with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for F being Instruction-Sequence of S
for s being State of S
for k being 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 Instruction-Sequence of S; :: thesis: for s being State of S
for k being 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 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 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 2;

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, A1, PARTFUN1:def 6;

A5: now :: thesis: for i being Nat st CurInstr (F,(Comput (F,s,i))) = halt S holds
not k + 1 > i

let i be 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, Th5; :: thesis: verum

end;

A8: F halts_on s by A3, Th30;
CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A3, A1, PARTFUN1:def 6;
hence ( LifeSpan (F,s) = k + 1 & F halts_on s ) by A5, Def15, 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 :: thesis: not CurInstr (F,(Comput (F,s,k))) = halt S

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

end;

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