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;

hence ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) by A10, A1, PARTFUN1:def 6; :: thesis: verum

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 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 )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 A2, A1, PARTFUN1:def 6;

CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A3, A1, PARTFUN1:def 6;

hence ( LifeSpan (F,s) = k + 1 & F halts_on s ) by A5, Def15, A8; :: thesis: verum

end;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 A2, A1, PARTFUN1:def 6;

A5: now :: thesis: for i being Nat st CurInstr (F,(Comput (F,s,i))) = halt S holds

not k + 1 > i

A8:
F halts_on s
by A3, Th30;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 A7, NAT_1:13;

hence contradiction by A4, A6, Th5; :: thesis: verum

end;assume that

A6: CurInstr (F,(Comput (F,s,i))) = halt S and

A7: k + 1 > i ; :: thesis: contradiction

i <= k by A7, NAT_1:13;

hence contradiction by A4, A6, Th5; :: thesis: verum

CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A3, A1, PARTFUN1:def 6;

hence ( LifeSpan (F,s) = k + 1 & F halts_on s ) by A5, Def15, A8; :: thesis: verum

A10: now :: thesis: not CurInstr (F,(Comput (F,s,k))) = halt S

CurInstr (F,(Comput (F,s,(k + 1)))) = halt S
by A9, Def15;assume
CurInstr (F,(Comput (F,s,k))) = halt S
; :: thesis: contradiction

then k + 1 <= k by A9, Def15;

hence contradiction by NAT_1:13; :: thesis: verum

end;then k + 1 <= k by A9, Def15;

hence contradiction by NAT_1:13; :: thesis: verum

hence ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) by A10, A1, PARTFUN1:def 6; :: thesis: verum