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

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