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 ;
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 ;
hence contradiction by A4, A6, Th5; :: thesis: verum
end;
A8: F halts_on s by ;
CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by ;
hence ( LifeSpan (F,s) = k + 1 & F halts_on s ) by ; :: 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 ;
hence contradiction by NAT_1:13; :: thesis: verum
end;
CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by ;
hence ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) by ; :: thesis: verum