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 relocable1 relocable2 AMI-Struct over N

for F being data-only PartFunc of (FinPartSt S),(FinPartSt S)

for l being Nat

for q being NAT -defined the InstructionsF of b_{1} -valued finite non halt-free Function

for p being non empty b_{4} -autonomic b_{4} -halted FinPartState of S st IC in dom p holds

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N; :: thesis: for F being data-only PartFunc of (FinPartSt S),(FinPartSt S)

for l being Nat

for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b_{3} -autonomic b_{3} -halted FinPartState of S st IC in dom p holds

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let F be data-only PartFunc of (FinPartSt S),(FinPartSt S); :: thesis: for l being Nat

for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b_{2} -autonomic b_{2} -halted FinPartState of S st IC in dom p holds

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let l be Nat; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b_{1} -autonomic b_{1} -halted FinPartState of S st IC in dom p holds

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic q -halted FinPartState of S st IC in dom p holds

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let p be non empty q -autonomic q -halted FinPartState of S; :: thesis: ( IC in dom p implies for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F ) )

assume A1: IC in dom p ; :: thesis: for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let k be Nat; :: thesis: ( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in proj1 F or ex b_{1} being set st

( x = b_{1} & p +* b_{1} is Autonomy of q & F . b_{1} c= Result (q,(p +* b_{1})) ) )

assume A14: x in dom F ; :: thesis: ex b_{1} being set st

( x = b_{1} & p +* b_{1} is Autonomy of q & F . b_{1} c= Result (q,(p +* b_{1})) )

then consider d1 being FinPartState of S such that

A15: x = d1 and

A16: (IncIC (p,k)) +* d1 is Autonomy of Reloc (q,k) and

A17: F . d1 c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d1)) by A13;

dom F c= FinPartSt S by RELAT_1:def 18;

then reconsider d = x as FinPartState of S by A14, MEMSTR_0:76;

reconsider d = d as data-only FinPartState of S by A14, MEMSTR_0:def 17;

A18: dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;

then A19: IC in dom (p +* d) by A1, XBOOLE_0:def 3;

A20: (IncIC (p,k)) +* d = IncIC ((p +* d),k) by MEMSTR_0:54;

IncIC ((p +* d),k) is Reloc (q,k) -autonomic by A15, A16, A20, EXTPRO_1:def 12;

then A21: p +* d is q -autonomic by A19, Th11;

A22: IncIC ((p +* d),k) is Reloc (q,k) -halted by A15, A16, A20, EXTPRO_1:def 12;

A23: p +* d is q -halted by A19, Th12, A21, A22;

reconsider pd = p +* d as non empty q -autonomic q -halted FinPartState of S by A19, Th12, A21, A22;

A24: IC in dom pd by A18, A1, XBOOLE_0:def 3;

A25: DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d1))) = DataPart (Result ((Reloc (q,k)),(IncIC ((p +* d),k)))) by A15, MEMSTR_0:54

.= DataPart (Result (q,(p +* d))) by Th13, A24 ;

take d ; :: thesis: ( x = d & p +* d is Autonomy of q & F . d c= Result (q,(p +* d)) )

thus x = d ; :: thesis: ( p +* d is Autonomy of q & F . d c= Result (q,(p +* d)) )

thus p +* d is Autonomy of q by A21, A23, EXTPRO_1:def 12; :: thesis: F . d c= Result (q,(p +* d))

reconsider Fs1 = F . d1 as FinPartState of S by A17;

A26: Fs1 is data-only by A14, A15, MEMSTR_0:def 17;

then F . d1 c= DataPart (Result (q,(p +* d))) by A25, A17, MEMSTR_0:5;

hence F . d c= Result (q,(p +* d)) by A15, A26, MEMSTR_0:5; :: thesis: verum

for F being data-only PartFunc of (FinPartSt S),(FinPartSt S)

for l being Nat

for q being NAT -defined the InstructionsF of b

for p being non empty b

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N; :: thesis: for F being data-only PartFunc of (FinPartSt S),(FinPartSt S)

for l being Nat

for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let F be data-only PartFunc of (FinPartSt S),(FinPartSt S); :: thesis: for l being Nat

for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let l be Nat; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being non empty b

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic q -halted FinPartState of S st IC in dom p holds

for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let p be non empty q -autonomic q -halted FinPartState of S; :: thesis: ( IC in dom p implies for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F ) )

assume A1: IC in dom p ; :: thesis: for k being Nat holds

( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

let k be Nat; :: thesis: ( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

hereby :: thesis: ( Reloc (q,k), IncIC (p,k) computes F implies q,p computes F )

assume A13:
Reloc (q,k), IncIC (p,k) computes F
; :: thesis: q,p computes Fassume A2:
q,p computes F
; :: thesis: Reloc (q,k), IncIC (p,k) computes F

thus Reloc (q,k), IncIC (p,k) computes F :: thesis: verum

end;thus Reloc (q,k), IncIC (p,k) computes F :: thesis: verum

proof

let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in proj1 F or ex b_{1} being set st

( x = b_{1} & (IncIC (p,k)) +* b_{1} is Autonomy of Reloc (q,k) & F . b_{1} c= Result ((Reloc (q,k)),((IncIC (p,k)) +* b_{1})) ) )

assume A3: x in dom F ; :: thesis: ex b_{1} being set st

( x = b_{1} & (IncIC (p,k)) +* b_{1} is Autonomy of Reloc (q,k) & F . b_{1} c= Result ((Reloc (q,k)),((IncIC (p,k)) +* b_{1})) )

then consider d1 being FinPartState of S such that

A4: x = d1 and

A5: p +* d1 is Autonomy of q and

A6: F . d1 c= Result (q,(p +* d1)) by A2;

dom F c= FinPartSt S by RELAT_1:def 18;

then reconsider d = x as FinPartState of S by A3, MEMSTR_0:76;

reconsider d = d as data-only FinPartState of S by A3, MEMSTR_0:def 17;

dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;

then A7: IC in dom (p +* d) by A1, XBOOLE_0:def 3;

A8: p +* d is q -autonomic by A4, A5, EXTPRO_1:def 12;

then A9: IncIC ((p +* d),k) is Reloc (q,k) -autonomic by A7, Th11;

A10: p +* d is q -halted by A4, A5, EXTPRO_1:def 12;

reconsider pd = p +* d as non empty q -autonomic q -halted FinPartState of S by A4, A5, EXTPRO_1:def 12;

A11: DataPart (Result (q,pd)) = DataPart (Result ((Reloc (q,k)),(IncIC ((p +* d),k)))) by A7, Th13

.= DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d))) by MEMSTR_0:54 ;

reconsider Fs1 = F . d1 as FinPartState of S by A6;

take d ; :: thesis: ( x = d & (IncIC (p,k)) +* d is Autonomy of Reloc (q,k) & F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d)) )

thus x = d ; :: thesis: ( (IncIC (p,k)) +* d is Autonomy of Reloc (q,k) & F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d)) )

(IncIC (p,k)) +* d = IncIC ((p +* d),k) by MEMSTR_0:54;

hence (IncIC (p,k)) +* d is Autonomy of Reloc (q,k) by A8, A10, A9, EXTPRO_1:def 12; :: thesis: F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d))

A12: Fs1 is data-only by A3, A4, MEMSTR_0:def 17;

F . d1 c= DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d))) by A6, A12, A4, A11, MEMSTR_0:5;

hence F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d)) by A4, A12, MEMSTR_0:5; :: thesis: verum

end;( x = b

assume A3: x in dom F ; :: thesis: ex b

( x = b

then consider d1 being FinPartState of S such that

A4: x = d1 and

A5: p +* d1 is Autonomy of q and

A6: F . d1 c= Result (q,(p +* d1)) by A2;

dom F c= FinPartSt S by RELAT_1:def 18;

then reconsider d = x as FinPartState of S by A3, MEMSTR_0:76;

reconsider d = d as data-only FinPartState of S by A3, MEMSTR_0:def 17;

dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;

then A7: IC in dom (p +* d) by A1, XBOOLE_0:def 3;

A8: p +* d is q -autonomic by A4, A5, EXTPRO_1:def 12;

then A9: IncIC ((p +* d),k) is Reloc (q,k) -autonomic by A7, Th11;

A10: p +* d is q -halted by A4, A5, EXTPRO_1:def 12;

reconsider pd = p +* d as non empty q -autonomic q -halted FinPartState of S by A4, A5, EXTPRO_1:def 12;

A11: DataPart (Result (q,pd)) = DataPart (Result ((Reloc (q,k)),(IncIC ((p +* d),k)))) by A7, Th13

.= DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d))) by MEMSTR_0:54 ;

reconsider Fs1 = F . d1 as FinPartState of S by A6;

take d ; :: thesis: ( x = d & (IncIC (p,k)) +* d is Autonomy of Reloc (q,k) & F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d)) )

thus x = d ; :: thesis: ( (IncIC (p,k)) +* d is Autonomy of Reloc (q,k) & F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d)) )

(IncIC (p,k)) +* d = IncIC ((p +* d),k) by MEMSTR_0:54;

hence (IncIC (p,k)) +* d is Autonomy of Reloc (q,k) by A8, A10, A9, EXTPRO_1:def 12; :: thesis: F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d))

A12: Fs1 is data-only by A3, A4, MEMSTR_0:def 17;

F . d1 c= DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d))) by A6, A12, A4, A11, MEMSTR_0:5;

hence F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d)) by A4, A12, MEMSTR_0:5; :: thesis: verum

let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in proj1 F or ex b

( x = b

assume A14: x in dom F ; :: thesis: ex b

( x = b

then consider d1 being FinPartState of S such that

A15: x = d1 and

A16: (IncIC (p,k)) +* d1 is Autonomy of Reloc (q,k) and

A17: F . d1 c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d1)) by A13;

dom F c= FinPartSt S by RELAT_1:def 18;

then reconsider d = x as FinPartState of S by A14, MEMSTR_0:76;

reconsider d = d as data-only FinPartState of S by A14, MEMSTR_0:def 17;

A18: dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;

then A19: IC in dom (p +* d) by A1, XBOOLE_0:def 3;

A20: (IncIC (p,k)) +* d = IncIC ((p +* d),k) by MEMSTR_0:54;

IncIC ((p +* d),k) is Reloc (q,k) -autonomic by A15, A16, A20, EXTPRO_1:def 12;

then A21: p +* d is q -autonomic by A19, Th11;

A22: IncIC ((p +* d),k) is Reloc (q,k) -halted by A15, A16, A20, EXTPRO_1:def 12;

A23: p +* d is q -halted by A19, Th12, A21, A22;

reconsider pd = p +* d as non empty q -autonomic q -halted FinPartState of S by A19, Th12, A21, A22;

A24: IC in dom pd by A18, A1, XBOOLE_0:def 3;

A25: DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d1))) = DataPart (Result ((Reloc (q,k)),(IncIC ((p +* d),k)))) by A15, MEMSTR_0:54

.= DataPart (Result (q,(p +* d))) by Th13, A24 ;

take d ; :: thesis: ( x = d & p +* d is Autonomy of q & F . d c= Result (q,(p +* d)) )

thus x = d ; :: thesis: ( p +* d is Autonomy of q & F . d c= Result (q,(p +* d)) )

thus p +* d is Autonomy of q by A21, A23, EXTPRO_1:def 12; :: thesis: F . d c= Result (q,(p +* d))

reconsider Fs1 = F . d1 as FinPartState of S by A17;

A26: Fs1 is data-only by A14, A15, MEMSTR_0:def 17;

then F . d1 c= DataPart (Result (q,(p +* d))) by A25, A17, MEMSTR_0:5;

hence F . d c= Result (q,(p +* d)) by A15, A26, MEMSTR_0:5; :: thesis: verum