let N be non empty with_non-empty_elements set ; :: thesis: for S being standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for q being NAT -defined the Instructions 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 Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let S be standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized AMI-Struct of N; :: thesis: ( S is CurIns-recognized implies for q being NAT -defined the Instructions 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 Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic ) )
assume A1: S is CurIns-recognized ; :: thesis: for q being NAT -defined the Instructions 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 Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let q be NAT -defined the Instructions 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 Element of 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 Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic ) )
assume A2: IC in dom p ; :: thesis: for k being Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let k be Element of 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 A4: 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 Element of NAT holds (Comput (P,b₁,b₃)) | (proj1 (IncIC (p,k))) = (Comput (Q,b₂,b₃)) | (proj1 (IncIC (p,k))) ) )
assume that
A5: Reloc (q,k) c= P and
A6: 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 Element of NAT 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 Element of NAT holds (Comput (P,s1,b₁)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,b₁)) | (proj1 (IncIC (p,k))) )
assume that
A7: IncIC (p,k) c= s1 and
A8: IncIC (p,k) c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput (P,s1,b₁)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,b₁)) | (proj1 (IncIC (p,k)))
let i be Element of NAT ; :: thesis: (Comput (P,s1,i)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,i)) | (proj1 (IncIC (p,k)))
A12: dom (Start-At (((IC (Comput ((Q +* q),(s2 +* p),i))) + k),S)) = {(IC )} by FUNCOP_1:13;
then A13: dom (DataPart p) misses dom (Start-At (((IC (Comput ((Q +* q),(s2 +* p),i))) + k),S)) by MEMSTR_0:4;
A14: dom (Start-At (((IC (Comput ((P +* q),(s1 +* p),i))) + k),S)) = {(IC )} by FUNCOP_1:13;
then A15: dom (DataPart p) misses dom (Start-At (((IC (Comput ((P +* q),(s1 +* p),i))) + k),S)) by MEMSTR_0:4;
A17: ( 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 A18: (Comput ((P +* q),(s1 +* p),i)) | (dom p) = (Comput ((Q +* q),(s2 +* p),i)) | (dom p) by A4, A17, EXTPRO_1:def 10;
A19: DataPart p c= p by MEMSTR_0:12;
A21: (Comput (P,s1,i)) | (dom (DataPart p)) = (Comput (P,s1,i)) | (dom (DataPart p))
.= (IncIC ((Comput ((P +* q),(s1 +* p),i)),k)) | (dom (DataPart p)) by A2, A4, A7, Th9, A1, A5
.= (IncIC ((Comput ((P +* q),(s1 +* p),i)),k)) | (dom (DataPart p))
.= (Comput ((P +* q),(s1 +* p),i)) | (dom (DataPart p)) by A15, FUNCT_4:72
.= (Comput ((Q +* q),(s2 +* p),i)) | (dom (DataPart p)) by A18, A19, RELAT_1:11, RELAT_1:153
.= (IncIC ((Comput ((Q +* q),(s2 +* p),i)),k)) | (dom (DataPart p)) by A13, FUNCT_4:72
.= (IncIC ((Comput ((Q +* q),(s2 +* p),i)),k)) | (dom (DataPart p))
.= (Comput (Q,s2,i)) | (dom (DataPart p)) by A2, A4, A8, Th9, A1, A6
.= (Comput (Q,s2,i)) | (dom (DataPart p)) ;
IC in dom p by A2;
then A22: {(IC )} c= dom p by ZFMISC_1:31;
A23: 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 A18, A22, RELAT_1:153
.= Start-At ((IC (Comput ((Q +* q),(s2 +* p),i))),S) by MEMSTR_0:18 ;
A24: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:13;
A26: (Comput (P,s1,i)) | (dom (Start-At (((IC p) + k),S))) = (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 A2, A4, A7, Th9, A1, A5
.= (IncIC ((Comput ((P +* q),(s1 +* p),i)),k)) | (dom (Start-At (((IC p) + k),S)))
.= Start-At (((IC (Comput ((P +* q),(s1 +* p),i))) + k),S) by A24, A14, FUNCT_4:23
.= Start-At (((IC (Comput ((Q +* q),(s2 +* p),i))) + k),S) by A23, MEMSTR_0:21
.= (IncIC ((Comput ((Q +* q),(s2 +* p),i)),k)) | (dom (Start-At (((IC p) + k),S))) by A24, A12, FUNCT_4:23
.= (IncIC ((Comput ((Q +* q),(s2 +* p),i)),k)) | (dom (Start-At (((IC p) + k),S)))
.= (Comput (Q,s2,i)) | (dom (Start-At (((IC p) + k),S))) by A2, A4, A8, Th9, A1, A6
.= (Comput (Q,s2,i)) | (dom (Start-At (((IC p) + k),S))) ;
A27: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:13;
A28: dom p = {(IC )} \/ (dom (DataPart p)) by A2, MEMSTR_0:24;
A29: (Comput (P,s1,i)) | (dom p) = ((Comput (P,s1,i)) | {(IC )}) \/ ((Comput (P,s1,i)) | (dom (DataPart p))) by A28, RELAT_1:78
.= (Comput (Q,s2,i)) | (dom p) by A28, A27, A21, A26, RELAT_1:78 ;
A30: dom (IncIC (p,k)) = (dom p) \/ (dom (Start-At (((IC p) + k),S))) by FUNCT_4:def 1
.= (dom p) \/ (dom (Start-At (((IC p) + k),S))) ;
A31: (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 A30, RELAT_1:78
.= (Comput (Q,s2,i)) | (dom (IncIC (p,k))) by A30, A26, A29, RELAT_1:78 ;
thus (Comput (P,s1,i)) | (dom (IncIC (p,k))) = (Comput (P,s1,i)) | (dom (IncIC (p,k)))
.= (Comput (Q,s2,i)) | (dom (IncIC (p,k))) by A31 ; :: thesis: verum

end;

end;

assume A32: IncIC (p,k) is Reloc (q,k) -autonomic ; :: thesis: p is q -autonomic
B33: 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 Element of NAT holds (Comput (P,b₁,b₃)) | (proj1 p) = (Comput (Q,b₂,b₃)) | (proj1 p) ) )
assume that
A34: q c= P and
A35: q c= Q ; :: thesis: for b₁, b₂ being set holds
( not p c= b₁ or not p c= b₂ or for b₃ being Element of NAT holds (Comput (P,b₁,b₃)) | (proj1 p) = (Comput (Q,b₂,b₃)) | (proj1 p) )
A36: ( 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 Element of NAT holds (Comput (P,s1,b₁)) | (proj1 p) = (Comput (Q,s2,b₁)) | (proj1 p) )
assume that
A37: p c= s1 and
A38: p c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput (P,s1,b₁)) | (proj1 p) = (Comput (Q,s2,b₁)) | (proj1 p)
let i be Element of 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 A43: (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 A32, A36, EXTPRO_1:def 10;
A44: dom (Start-At (((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))) -' k),S)) = {(IC )} by FUNCOP_1:13;
then A45: dom (DataPart p) misses dom (Start-At (((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))) -' k),S)) by MEMSTR_0:4;
A46: dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i))) -' k),S)) = {(IC )} by FUNCOP_1:13;
then A47: dom (DataPart p) misses dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i))) -' k),S)) by MEMSTR_0:4;
A49: (Comput (P,s1,i)) | (dom (DataPart p)) = (Comput (P,s1,i)) | (dom (DataPart p))
.= (DecIC ((Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)),k)) | (dom (DataPart p)) by A2, A32, A37, Th10, A1, A34
.= (DecIC ((Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)),k)) | (dom (DataPart p))
.= (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)) | (dom (DataPart p)) by A47, FUNCT_4:72
.= (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)) | (dom (DataPart p)) by A43, B33, RELAT_1:11, RELAT_1:153
.= (DecIC ((Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)),k)) | (dom (DataPart p)) by A45, FUNCT_4:72
.= (DecIC ((Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)),k)) | (dom (DataPart p))
.= (Comput (Q,s2,i)) | (dom (DataPart p)) by A2, A32, A38, Th10, A1, A35
.= (Comput (Q,s2,i)) | (dom (DataPart p)) ;
IC in dom (IncIC (p,k)) by MEMSTR_0:52;
then A50: {(IC )} c= dom (IncIC (p,k)) by ZFMISC_1:31;
A51: 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 A43, A50, RELAT_1:153
.= Start-At ((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))),S) by MEMSTR_0:18 ;
A52: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:13;
A54: (Comput (P,s1,i)) | (dom (Start-At ((IC p),S))) = (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 A2, A32, A37, Th10, A1, A34
.= (DecIC ((Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i)),k)) | (dom (Start-At ((IC p),S)))
.= Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s1 +* (IncIC (p,k))),i))) -' k),S) by A52, A46, FUNCT_4:23
.= Start-At (((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))) -' k),S) by A51, MEMSTR_0:22
.= (DecIC ((Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)),k)) | (dom (Start-At ((IC p),S))) by A52, A44, FUNCT_4:23
.= (DecIC ((Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i)),k)) | (dom (Start-At ((IC p),S)))
.= (Comput (Q,s2,i)) | (dom (Start-At ((IC p),S))) by A2, A32, A38, Th10, A1, A35
.= (Comput (Q,s2,i)) | (dom (Start-At ((IC p),S))) ;
thus (Comput (P,s1,i)) | (dom p) = (Comput (P,s1,i)) | (dom ((Start-At ((IC p),S)) +* (DataPart p))) by A2, 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 A49, A54, 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 A2, MEMSTR_0:19 ; :: thesis: verum