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

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

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

for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

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

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

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

for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

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

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

for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

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

for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

let p be q -autonomic FinPartState of S; :: thesis: ( IC in dom p implies for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )

assume A1: IC in dom p ; :: thesis: for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

let s be State of S; :: thesis: ( IncIC (p,k) c= s implies for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )

assume A2: IncIC (p,k) c= s ; :: thesis: for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

let P be Instruction-Sequence of S; :: thesis: ( Reloc (q,k) c= P implies for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )

assume A3: Reloc (q,k) c= P ; :: thesis: for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

defpred S_{1}[ Nat] means Comput (P,s,$1) = IncIC ((Comput ((P +* q),(s +* p),$1)),k);

A4: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

A17: dom (Start-At ((IC p),S)) = {(IC )} ;

A18: Start-At (((IC p) + k),S) c= IncIC (p,k) by MEMSTR_0:55;

A19: IC (Comput ((P +* q),(s +* p),0)) = IC p by A1, FUNCT_4:13;

set DP = DataPart p;

DataPart (IncIC (p,k)) c= IncIC (p,k) by RELAT_1:59;

then DataPart (IncIC (p,k)) c= s by A2, XBOOLE_1:1;

then A20: DataPart p c= s by MEMSTR_0:51;

set PR = Reloc (q,k);

set IS = Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S);

A21: dom (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) = {(IC )} ;

Comput (P,s,0) = s +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A19, A2, A18, FUNCT_4:98, XBOOLE_1:1

.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A20, FUNCT_4:98

.= ((s +* (DataPart p)) +* (Start-At ((IC p),S))) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A21, A17, FUNCT_4:74

.= (s +* ((DataPart p) +* (Start-At ((IC p),S)))) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by FUNCT_4:14

.= IncIC ((Comput ((P +* q),(s +* p),0)),k) by A1, MEMSTR_0:26 ;

then A22: S_{1}[ 0 ]
;

thus for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A22, A4); :: thesis: verum

for k being Nat

for q being NAT -defined the InstructionsF of b

for p being b

for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

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

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

for p being b

for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

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

for p being b

for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

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

for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

let p be q -autonomic FinPartState of S; :: thesis: ( IC in dom p implies for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )

assume A1: IC in dom p ; :: thesis: for s being State of S st IncIC (p,k) c= s holds

for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

let s be State of S; :: thesis: ( IncIC (p,k) c= s implies for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )

assume A2: IncIC (p,k) c= s ; :: thesis: for P being Instruction-Sequence of S st Reloc (q,k) c= P holds

for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

let P be Instruction-Sequence of S; :: thesis: ( Reloc (q,k) c= P implies for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )

assume A3: Reloc (q,k) c= P ; :: thesis: for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

defpred S

A4: for i being Nat st S

S

proof

set IP = Start-At ((IC p),S);
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A5: Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) ; :: thesis: S_{1}[i + 1]

reconsider kk = IC (Comput ((P +* q),(s +* p),i)) as Nat ;

A6: IC in dom (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S)) by TARSKI:def 1;

A7: p c= s +* p by FUNCT_4:25;

A8: q c= P +* q by FUNCT_4:25;

not p is empty by A1;

then A9: IC (Comput ((P +* q),(s +* p),i)) in dom q by Def4, A7, A8;

then A10: IC (Comput ((P +* q),(s +* p),i)) in dom (IncAddr (q,k)) by COMPOS_1:def 21;

A11: (IC (Comput ((P +* q),(s +* p),i))) + k in dom (Reloc (q,k)) by A9, COMPOS_1:46;

reconsider kk = IC (Comput ((P +* q),(s +* p),i)) as Nat ;

A12: IC (Comput (P,s,i)) = IC (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S)) by A5, A6, FUNCT_4:13

.= (IC (Comput ((P +* q),(s +* p),i))) + k by FUNCOP_1:72 ;

A13: q c= P +* q by FUNCT_4:25;

A14: q /. kk = q . kk by A9, PARTFUN1:def 6;

A15: dom (P +* q) = NAT by PARTFUN1:def 2;

dom P = NAT by PARTFUN1:def 2;

then A16: CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by PARTFUN1:def 6

.= (Reloc (q,k)) . (IC (Comput (P,s,i))) by A3, A11, A12, GRFUNC_1:2

.= (IncAddr (q,k)) . kk by A10, A12, VALUED_1:def 12

.= IncAddr ((q /. kk),k) by A9, COMPOS_1:def 21

.= IncAddr (((P +* q) . (IC (Comput ((P +* q),(s +* p),i)))),k) by A9, A14, A13, GRFUNC_1:2

.= IncAddr ((CurInstr ((P +* q),(Comput ((P +* q),(s +* p),i)))),k) by A15, PARTFUN1:def 6 ;

thus Comput (P,s,(i + 1)) = Following (P,(Comput (P,s,i))) by EXTPRO_1:3

.= IncIC ((Following ((P +* q),(Comput ((P +* q),(s +* p),i)))),k) by A5, A16, Th4

.= IncIC ((Comput ((P +* q),(s +* p),(i + 1))),k) by EXTPRO_1:3 ; :: thesis: verum

end;assume A5: Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) ; :: thesis: S

reconsider kk = IC (Comput ((P +* q),(s +* p),i)) as Nat ;

A6: IC in dom (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S)) by TARSKI:def 1;

A7: p c= s +* p by FUNCT_4:25;

A8: q c= P +* q by FUNCT_4:25;

not p is empty by A1;

then A9: IC (Comput ((P +* q),(s +* p),i)) in dom q by Def4, A7, A8;

then A10: IC (Comput ((P +* q),(s +* p),i)) in dom (IncAddr (q,k)) by COMPOS_1:def 21;

A11: (IC (Comput ((P +* q),(s +* p),i))) + k in dom (Reloc (q,k)) by A9, COMPOS_1:46;

reconsider kk = IC (Comput ((P +* q),(s +* p),i)) as Nat ;

A12: IC (Comput (P,s,i)) = IC (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S)) by A5, A6, FUNCT_4:13

.= (IC (Comput ((P +* q),(s +* p),i))) + k by FUNCOP_1:72 ;

A13: q c= P +* q by FUNCT_4:25;

A14: q /. kk = q . kk by A9, PARTFUN1:def 6;

A15: dom (P +* q) = NAT by PARTFUN1:def 2;

dom P = NAT by PARTFUN1:def 2;

then A16: CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by PARTFUN1:def 6

.= (Reloc (q,k)) . (IC (Comput (P,s,i))) by A3, A11, A12, GRFUNC_1:2

.= (IncAddr (q,k)) . kk by A10, A12, VALUED_1:def 12

.= IncAddr ((q /. kk),k) by A9, COMPOS_1:def 21

.= IncAddr (((P +* q) . (IC (Comput ((P +* q),(s +* p),i)))),k) by A9, A14, A13, GRFUNC_1:2

.= IncAddr ((CurInstr ((P +* q),(Comput ((P +* q),(s +* p),i)))),k) by A15, PARTFUN1:def 6 ;

thus Comput (P,s,(i + 1)) = Following (P,(Comput (P,s,i))) by EXTPRO_1:3

.= IncIC ((Following ((P +* q),(Comput ((P +* q),(s +* p),i)))),k) by A5, A16, Th4

.= IncIC ((Comput ((P +* q),(s +* p),(i + 1))),k) by EXTPRO_1:3 ; :: thesis: verum

A17: dom (Start-At ((IC p),S)) = {(IC )} ;

A18: Start-At (((IC p) + k),S) c= IncIC (p,k) by MEMSTR_0:55;

A19: IC (Comput ((P +* q),(s +* p),0)) = IC p by A1, FUNCT_4:13;

set DP = DataPart p;

DataPart (IncIC (p,k)) c= IncIC (p,k) by RELAT_1:59;

then DataPart (IncIC (p,k)) c= s by A2, XBOOLE_1:1;

then A20: DataPart p c= s by MEMSTR_0:51;

set PR = Reloc (q,k);

set IS = Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S);

A21: dom (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) = {(IC )} ;

Comput (P,s,0) = s +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A19, A2, A18, FUNCT_4:98, XBOOLE_1:1

.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A20, FUNCT_4:98

.= ((s +* (DataPart p)) +* (Start-At ((IC p),S))) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A21, A17, FUNCT_4:74

.= (s +* ((DataPart p) +* (Start-At ((IC p),S)))) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by FUNCT_4:14

.= IncIC ((Comput ((P +* q),(s +* p),0)),k) by A1, MEMSTR_0:26 ;

then A22: S

thus for i being Nat holds S