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 l being Nat

for P being NAT -defined the InstructionsF of b_{1} -valued Function st l .--> (halt S) c= P holds

for p being b_{2} -started PartState of S holds p is P -autonomic

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for l being Nat

for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds

for p being b_{1} -started PartState of S holds p is P -autonomic

let l be Nat; :: thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds

for p being l -started PartState of S holds p is P -autonomic

set h = halt S;

set p = Start-At (l,S);

let P be NAT -defined the InstructionsF of S -valued Function; :: thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p is P -autonomic )

assume A1: l .--> (halt S) c= P ; :: thesis: for p being l -started PartState of S holds p is P -autonomic

let p be l -started PartState of S; :: thesis: p is P -autonomic

set I = p +* P;

let Q1, Q2 be Instruction-Sequence of S; :: according to EXTPRO_1:def 10 :: thesis: ( P c= Q1 & P c= Q2 implies for s1, s2 being State of S st p c= s1 & p c= s2 holds

for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) )

assume A2: ( P c= Q1 & P c= Q2 ) ; :: thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds

for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)

let s1, s2 be State of S; :: thesis: ( p c= s1 & p c= s2 implies for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) )

assume that

A3: p c= s1 and

A4: p c= s2 ; :: thesis: for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)

let i be Nat; :: thesis: (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)

A5: ( l .--> (halt S) c= Q1 & l .--> (halt S) c= Q2 ) by A1, A2, XBOOLE_1:1;

hence (Comput (Q1,s1,i)) | (dom p) = s1 | (dom p) by A3, Th11

.= p by A3, GRFUNC_1:23

.= s2 | (dom p) by A4, GRFUNC_1:23

.= (Comput (Q2,s2,i)) | (dom p) by A4, Th11, A5 ;

:: thesis: verum

for l being Nat

for P being NAT -defined the InstructionsF of b

for p being b

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for l being Nat

for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds

for p being b

let l be Nat; :: thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds

for p being l -started PartState of S holds p is P -autonomic

set h = halt S;

set p = Start-At (l,S);

let P be NAT -defined the InstructionsF of S -valued Function; :: thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p is P -autonomic )

assume A1: l .--> (halt S) c= P ; :: thesis: for p being l -started PartState of S holds p is P -autonomic

let p be l -started PartState of S; :: thesis: p is P -autonomic

set I = p +* P;

let Q1, Q2 be Instruction-Sequence of S; :: according to EXTPRO_1:def 10 :: thesis: ( P c= Q1 & P c= Q2 implies for s1, s2 being State of S st p c= s1 & p c= s2 holds

for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) )

assume A2: ( P c= Q1 & P c= Q2 ) ; :: thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds

for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)

let s1, s2 be State of S; :: thesis: ( p c= s1 & p c= s2 implies for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) )

assume that

A3: p c= s1 and

A4: p c= s2 ; :: thesis: for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)

let i be Nat; :: thesis: (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)

A5: ( l .--> (halt S) c= Q1 & l .--> (halt S) c= Q2 ) by A1, A2, XBOOLE_1:1;

hence (Comput (Q1,s1,i)) | (dom p) = s1 | (dom p) by A3, Th11

.= p by A3, GRFUNC_1:23

.= s2 | (dom p) by A4, GRFUNC_1:23

.= (Comput (Q2,s2,i)) | (dom p) by A4, Th11, A5 ;

:: thesis: verum