let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for F being NAT -defined the Instructions of b₁ -valued total Function
for s being State of S
for k being Element of 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 stored-program IC-Ins-separated definite halting AMI-Struct of N; :: thesis: for F being NAT -defined the Instructions of S -valued total Function
for s being State of S
for k being Element of 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 NAT -defined the Instructions of S -valued total Function; :: thesis: for s being State of S
for k being Element of 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 Element of 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 Element of 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
A2: F halts_on Comput (F,s,k) and
A3: 0 < LifeSpan (F,(Comput (F,s,k))) ; :: thesis: LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
consider l being Nat such that
A4: LifeSpan (F,(Comput (F,s,k))) = l + 1 by A3, NAT_1:6;
reconsider l = l as Element of NAT by ORDINAL1:def 13;
F . (IC (Comput (F,(Comput (F,s,k)),(l + 1)))) = halt S by A2, A4, Th33;
then F . (IC (Comput (F,s,(k + (l + 1))))) = halt S by Th5;
then A5: F . (IC (Comput (F,s,(k + (l + 1))))) = halt S ;
F . (IC (Comput (F,(Comput (F,s,k)),l))) <> halt S by A2, A4, Th33;
then F . (IC (Comput (F,s,(k + l)))) <> halt S by Th5;
then F . (IC (Comput (F,s,(k + l)))) <> halt S ;
hence LifeSpan (F,s) = (k + l) + 1 by A5, Th33
.= k + (LifeSpan (F,(Comput (F,s,k)))) by A4 ;
:: thesis: verum