let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N
for q being NAT -defined the InstructionsF of b₁ -valued finite non halt-free Function
for p being non empty FinPartState of S st IC in dom p holds
for k being Nat holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty FinPartState of S st IC in dom p holds
for k being Nat holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being non empty FinPartState of S st IC in dom p holds
for k being Nat holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let p be non empty FinPartState of S; :: thesis: ( IC in dom p implies for k being Nat holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic ) )
assume A1: IC in dom p ; :: thesis: for k being Nat holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let k be Nat; :: thesis: ( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )

hereby :: thesis: ( IncIC (p,k) is Reloc (q,k) -autonomic implies p is q -autonomic )

assume A2: p is q -autonomic ; :: thesis: IncIC (p,k) is Reloc (q,k) -autonomic
thus IncIC (p,k) is Reloc (q,k) -autonomic :: thesis: verum

proof

let P, Q be Instruction-Sequence of S; :: according to EXTPRO_1:def 10 :: thesis: ( not Reloc (q,k) c= P or not Reloc (q,k) c= Q or for b₁, b₂ being set holds
( not IncIC (p,k) c= b₁ or not IncIC (p,k) c= b₂ or for b₃ being set holds (Comput (P,b₁,b₃)) | (proj1 (IncIC (p,k))) = (Comput (Q,b₂,b₃)) | (proj1 (IncIC (p,k))) ) )
assume that
A3: Reloc (q,k) c= P and
A4: Reloc (q,k) c= Q ; :: thesis: for b₁, b₂ being set holds
( not IncIC (p,k) c= b₁ or not IncIC (p,k) c= b₂ or for b₃ being set holds (Comput (P,b₁,b₃)) | (proj1 (IncIC (p,k))) = (Comput (Q,b₂,b₃)) | (proj1 (IncIC (p,k))) )
let s1, s2 be State of S; :: thesis: ( not IncIC (p,k) c= s1 or not IncIC (p,k) c= s2 or for b₁ being set holds (Comput (P,s1,b₁)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,b₁)) | (proj1 (IncIC (p,k))) )
assume that
A5: IncIC (p,k) c= s1 and
A6: IncIC (p,k) c= s2 ; :: thesis: for b₁ being set holds (Comput (P,s1,b₁)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,b₁)) | (proj1 (IncIC (p,k)))
let i be Nat; :: thesis: (Comput (P,s1,i)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,i)) | (proj1 (IncIC (p,k)))
A7: dom (Start-At (((IC (Comput ((Q +* q),(s2 +* p),i))) + k),S)) = {(IC )} ;
A8: dom (DataPart p) misses dom (Start-At (((IC (Comput ((Q +* q),(s2 +* p),i))) + k),S)) by MEMSTR_0:4;
A9: dom (Start-At (((IC (Comput ((P +* q),(s1 +* p),i))) + k),S)) = {(IC )} ;
A10: dom (DataPart p) misses dom (Start-At (((IC (Comput ((P +* q),(s1 +* p),i))) + k),S)) by MEMSTR_0:4;
A11: ( q c= P +* q & q c= Q +* q ) by FUNCT_4:25;
( p c= s1 +* p & p c= s2 +* p ) by FUNCT_4:25;
then A12: (Comput ((P +* q),(s1 +* p),i)) | (dom p) = (Comput ((Q +* q),(s2 +* p),i)) | (dom p) by A2, A11;
A13: DataPart p c= p by MEMSTR_0:12;
A14: (Comput (P,s1,i)) | (dom (DataPart p)) = (IncIC ((Comput ((P +* q),(s1 +* p),i)),k)) | (dom (DataPart p)) by A1, A2, A5, Th9, A3
.= (Comput ((P +* q),(s1 +* p),i)) | (dom (DataPart p)) by A10, FUNCT_4:72
.= (Comput ((Q +* q),(s2 +* p),i)) | (dom (DataPart p)) by A12, A13, RELAT_1:11, RELAT_1:153
.= (IncIC ((Comput ((Q +* q),(s2 +* p),i)),k)) | (dom (DataPart p)) by A8, FUNCT_4:72
.= (Comput (Q,s2,i)) | (dom (DataPart p)) by A1, A2, A6, Th9, A4 ;
A15: {(IC )} c= dom p by A1, ZFMISC_1:31;
A16: Start-At ((IC (Comput ((P +* q),(s1 +* p),i))),S) = (Comput ((P +* q),(s1 +* p),i)) | {(IC )} by MEMSTR_0:18
.= (Comput ((Q +* q),(s2 +* p),i)) | {(IC )} by A12, A15, RELAT_1:153
.= Start-At ((IC (Comput ((Q +* q),(s2 +* p),i))),S) by MEMSTR_0:18 ;
A18: (Comput (P,s1,i)) | (dom (Start-At (((IC p) + k),S))) = (IncIC ((Comput ((P +* q),(s1 +* p),i)),k)) | (dom (Start-At (((IC p) + k),S))) by A1, A2, A5, Th9, A3
.= Start-At (((IC (Comput ((P +* q),(s1 +* p),i))) + k),S) by A9
.= Start-At (((IC (Comput ((Q +* q),(s2 +* p),i))) + k),S) by A16, MEMSTR_0:21
.= (IncIC ((Comput ((Q +* q),(s2 +* p),i)),k)) | (dom (Start-At (((IC p) + k),S))) by A7
.= (Comput (Q,s2,i)) | (dom (Start-At (((IC p) + k),S))) by A1, A2, A6, Th9, A4 ;
A20: dom p = {(IC )} \/ (dom (DataPart p)) by A1, MEMSTR_0:24;
A21: (Comput (P,s1,i)) | (dom p) = ((Comput (P,s1,i)) | {(IC )}) \/ ((Comput (P,s1,i)) | (dom (DataPart p))) by A20, RELAT_1:78
.= (Comput (Q,s2,i)) | (dom p) by A20, A14, A18, RELAT_1:78 ;
A22: dom (IncIC (p,k)) = (dom p) \/ (dom (Start-At (((IC p) + k),S))) by FUNCT_4:def 1;
A23: (Comput (P,s1,i)) | (dom (IncIC (p,k))) = ((Comput (P,s1,i)) | (dom p)) \/ ((Comput (P,s1,i)) | (dom (Start-At (((IC p) + k),S)))) by A22, RELAT_1:78
.= (Comput (Q,s2,i)) | (dom (IncIC (p,k))) by A22, A18, A21, RELAT_1:78 ;
thus (Comput (P,s1,i)) | (dom (IncIC (p,k))) = (Comput (Q,s2,i)) | (dom (IncIC (p,k))) by A23; :: thesis: verum

end;

end;

assume A24: IncIC (p,k) is Reloc (q,k) -autonomic ; :: thesis: p is q -autonomic
A25: DataPart p c= IncIC (p,k) by MEMSTR_0:62;
let P, Q be Instruction-Sequence of S; :: according to EXTPRO_1:def 10 :: thesis: ( not q c= P or not q c= Q or for b₁, b₂ being set holds
( not p c= b₁ or not p c= b₂ or for b₃ being set holds (Comput (P,b₁,b₃)) | (proj1 p) = (Comput (Q,b₂,b₃)) | (proj1 p) ) )
assume that
A26: q c= P and
A27: q c= Q ; :: thesis: for b₁, b₂ being set holds
( not p c= b₁ or not p c= b₂ or for b₃ being set holds (Comput (P,b₁,b₃)) | (proj1 p) = (Comput (Q,b₂,b₃)) | (proj1 p) )
A28: ( Reloc (q,k) c= P +* (Reloc (q,k)) & Reloc (q,k) c= Q +* (Reloc (q,k)) ) by FUNCT_4:25;
let s1, s2 be State of S; :: thesis: ( not p c= s1 or not p c= s2 or for b₁ being set holds (Comput (P,s1,b₁)) | (proj1 p) = (Comput (Q,s2,b₁)) | (proj1 p) )
assume that
A29: p c= s1 and
A30: p c= s2 ; :: thesis: for b₁ being set holds (Comput (P,s1,b₁)) | (proj1 p) = (Comput (Q,s2,b₁)) | (proj1 p)
let i be Nat; :: thesis: (Comput (P,s1,i)) | (proj1 p) = (Comput (Q,s2,i)) | (proj1 p)
( IncIC (p,k) c= s1 +* (IncIC (p,k)) & IncIC (p,k) c= s2 +* (IncIC (p,k)) ) by FUNCT_4:25;
then A31: (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)) | (dom (IncIC (p,k))) = (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)) | (dom (IncIC (p,k))) by A24, A28;
A32: dom (Start-At (((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))) -' k),S)) = {(IC )} ;
A33: dom (DataPart p) misses dom (Start-At (((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))) -' k),S)) by MEMSTR_0:4;
A34: dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i))) -' k),S)) = {(IC )} ;
A35: dom (DataPart p) misses dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i))) -' k),S)) by MEMSTR_0:4;
A36: (Comput (P,s1,i)) | (dom (DataPart p)) = (DecIC ((Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)),k)) | (dom (DataPart p)) by A1, A24, A29, Th10, A26
.= (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)) | (dom (DataPart p)) by A35, FUNCT_4:72
.= (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)) | (dom (DataPart p)) by A31, A25, RELAT_1:11, RELAT_1:153
.= (DecIC ((Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)),k)) | (dom (DataPart p)) by A33, FUNCT_4:72
.= (Comput (Q,s2,i)) | (dom (DataPart p)) by A1, A24, A30, Th10, A27 ;
IC in dom (IncIC (p,k)) by MEMSTR_0:52;
then A37: {(IC )} c= dom (IncIC (p,k)) by ZFMISC_1:31;
A38: Start-At ((IC (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i))),S) = (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)) | {(IC )} by MEMSTR_0:18
.= (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)) | {(IC )} by A31, A37, RELAT_1:153
.= Start-At ((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))),S) by MEMSTR_0:18 ;
A40: (Comput (P,s1,i)) | (dom (Start-At ((IC p),S))) = (DecIC ((Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)),k)) | (dom (Start-At ((IC p),S))) by A1, A24, A29, Th10, A26
.= Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i))) -' k),S) by A34
.= Start-At (((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))) -' k),S) by A38, MEMSTR_0:22
.= (DecIC ((Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)),k)) | (dom (Start-At ((IC p),S))) by A32
.= (Comput (Q,s2,i)) | (dom (Start-At ((IC p),S))) by A1, A24, A30, Th10, A27 ;
thus (Comput (P,s1,i)) | (dom p) = (Comput (P,s1,i)) | (dom ((Start-At ((IC p),S)) +* (DataPart p))) by A1, MEMSTR_0:19
.= (Comput (P,s1,i)) | ((dom (Start-At ((IC p),S))) \/ (dom (DataPart p))) by FUNCT_4:def 1
.= ((Comput (Q,s2,i)) | (dom (Start-At ((IC p),S)))) \/ ((Comput (Q,s2,i)) | (dom (DataPart p))) by A36, A40, RELAT_1:78
.= (Comput (Q,s2,i)) | ((dom (Start-At ((IC p),S))) \/ (dom (DataPart p))) by RELAT_1:78
.= (Comput (Q,s2,i)) | (dom ((Start-At ((IC p),S)) +* (DataPart p))) by FUNCT_4:def 1
.= (Comput (Q,s2,i)) | (dom p) by A1, MEMSTR_0:19 ; :: thesis: verum