let N be non empty with_zero set ; 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 st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
let S be 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 st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
let F be Instruction-Sequence of S; for s being State of S
for k being Nat st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
let s be State of S; for k being Nat st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
let k be Nat; ( F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) implies LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) )
set s2 = Comput (F,s,k);
set c = LifeSpan (F,(Comput (F,s,k)));
assume that
A1:
F halts_on Comput (F,s,k)
and
A2:
0 < LifeSpan (F,(Comput (F,s,k)))
; LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
consider l being Nat such that
A3:
LifeSpan (F,(Comput (F,s,k))) = l + 1
by A2, NAT_1:6;
reconsider l = l as Nat ;
F . (IC (Comput (F,(Comput (F,s,k)),(l + 1)))) = halt S
by A1, A3, Th31;
then A4:
F . (IC (Comput (F,s,(k + (l + 1))))) = halt S
by Th4;
F . (IC (Comput (F,(Comput (F,s,k)),l))) <> halt S
by A1, A3, Th31;
then
F . (IC (Comput (F,s,(k + l)))) <> halt S
by Th4;
hence LifeSpan (F,s) =
(k + l) + 1
by A4, Th31
.=
k + (LifeSpan (F,(Comput (F,s,k))))
by A3
;
verum