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 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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))) ; :: thesis: 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 ;
:: thesis: verum