let N be with_zero set ; 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 b1 -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; 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; 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; ( 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
; for k being Nat holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let k be Nat; ( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
hereby ( IncIC (p,k) is Reloc (q,k) -autonomic implies p is q -autonomic )
assume A2:
p is
q -autonomic
;
IncIC (p,k) is Reloc (q,k) -autonomic thus
IncIC (
p,
k) is
Reloc (
q,
k)
-autonomic
verumproof
let P,
Q be
Instruction-Sequence of
S;
EXTPRO_1:def 10 ( not Reloc (q,k) c= P or not Reloc (q,k) c= Q or for b1, b2 being set holds
( not IncIC (p,k) c= b1 or not IncIC (p,k) c= b2 or for b3 being set holds (Comput (P,b1,b3)) | (proj1 (IncIC (p,k))) = (Comput (Q,b2,b3)) | (proj1 (IncIC (p,k))) ) )
assume that A3:
Reloc (
q,
k)
c= P
and A4:
Reloc (
q,
k)
c= Q
;
for b1, b2 being set holds
( not IncIC (p,k) c= b1 or not IncIC (p,k) c= b2 or for b3 being set holds (Comput (P,b1,b3)) | (proj1 (IncIC (p,k))) = (Comput (Q,b2,b3)) | (proj1 (IncIC (p,k))) )
let s1,
s2 be
State of
S;
( not IncIC (p,k) c= s1 or not IncIC (p,k) c= s2 or for b1 being set holds (Comput (P,s1,b1)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,b1)) | (proj1 (IncIC (p,k))) )
assume that A5:
IncIC (
p,
k)
c= s1
and A6:
IncIC (
p,
k)
c= s2
;
for b1 being set holds (Comput (P,s1,b1)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,b1)) | (proj1 (IncIC (p,k)))
let i be
Nat;
(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;
verum
end;
end;
assume A24:
IncIC (p,k) is Reloc (q,k) -autonomic
; p is q -autonomic
A25:
DataPart p c= IncIC (p,k)
by MEMSTR_0:62;
let P, Q be Instruction-Sequence of S; EXTPRO_1:def 10 ( not q c= P or not q c= Q or for b1, b2 being set holds
( not p c= b1 or not p c= b2 or for b3 being set holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
assume that
A26:
q c= P
and
A27:
q c= Q
; for b1, b2 being set holds
( not p c= b1 or not p c= b2 or for b3 being set holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (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; ( not p c= s1 or not p c= s2 or for b1 being set holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
assume that
A29:
p c= s1
and
A30:
p c= s2
; for b1 being set holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p)
let i be Nat; (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
; verum