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 non empty FinPartState of S st IC in dom p holds

for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds

for P being Instruction-Sequence of S st q c= P holds

for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 non empty FinPartState of S st IC in dom p holds

for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds

for P being Instruction-Sequence of S st q c= P holds

for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 non empty FinPartState of S st IC in dom p holds

for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds

for P being Instruction-Sequence of S st q c= P holds

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

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 s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds

for P being Instruction-Sequence of S st q c= P holds

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

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

for P being Instruction-Sequence of S st q c= P holds

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

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

for P being Instruction-Sequence of S st q c= P holds

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

then A2: Start-At ((IC p),S) c= p by FUNCOP_1:84;

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

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

assume that

A3: p c= s and

A4: IncIC (p,k) is Reloc (q,k) -autonomic ; :: thesis: for P being Instruction-Sequence of S st q c= P holds

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

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

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

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

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

S_{1}[i + 1]

A25: IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)) = IC (IncIC (p,k)) by A24, FUNCT_4:13;

A26: DataPart p c= p by RELAT_1:59;

set DP = DataPart p;

set IP = Start-At (((IC p) + k),S);

set PP = q;

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

A27: dom (Start-At (((IC p) + k),S)) = {(IC )} ;

set PR = Reloc (q,k);

set SD = s | (dom (Reloc (q,k)));

A28: {(IC )} misses dom (DataPart p) by MEMSTR_0:4;

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

A30: dom (Start-At (((IC p) + k),S)) misses dom (DataPart p) by A28;

A31: (Start-At (((IC p) + k),S)) +* (DataPart p) = (DataPart p) +* (Start-At (((IC p) + k),S)) by A30, FUNCT_4:35

.= IncIC (p,k) by A1, MEMSTR_0:56 ;

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

.= s +* (Start-At ((((IC p) + k) -' k),S)) by NAT_D:34

.= s +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A25, MEMSTR_0:53

.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A26, A3, FUNCT_4:98, XBOOLE_1:1

.= ((s +* (DataPart p)) +* (Start-At (((IC p) + k),S))) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A29, A27, FUNCT_4:74

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

.= DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)),k) by A31, A27, A28, FUNCT_4:35 ;

then A32: S_{1}[ 0 ]
;

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

for k being Nat

for q being NAT -defined the InstructionsF of b

for p being non empty FinPartState of S st IC in dom p holds

for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds

for P being Instruction-Sequence of S st q c= P holds

for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 non empty FinPartState of S st IC in dom p holds

for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds

for P being Instruction-Sequence of S st q c= P holds

for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 non empty FinPartState of S st IC in dom p holds

for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds

for P being Instruction-Sequence of S st q c= P holds

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

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 s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds

for P being Instruction-Sequence of S st q c= P holds

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

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

for P being Instruction-Sequence of S st q c= P holds

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

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

for P being Instruction-Sequence of S st q c= P holds

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

then A2: Start-At ((IC p),S) c= p by FUNCOP_1:84;

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

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

assume that

A3: p c= s and

A4: IncIC (p,k) is Reloc (q,k) -autonomic ; :: thesis: for P being Instruction-Sequence of S st q c= P holds

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

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

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

defpred S

A6: for i being Nat st S

S

proof

A24:
IC in dom (IncIC (p,k))
by MEMSTR_0:52;
reconsider pp = q as preProgram of S ;

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

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

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

reconsider jk = IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) as Nat ;

A8: IncIC (p,k) c= s +* (IncIC (p,k)) by FUNCT_4:25;

A9: Reloc (q,k) c= P +* (Reloc (q,k)) by FUNCT_4:25;

A10: IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) in dom (Reloc (q,k)) by A4, Def4, A8, A9;

then A11: jk in { (j + k) where j is Nat : j in dom q } by COMPOS_1:33;

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

consider j being Nat such that

A13: jk = j + k and

A14: j in dom q by A11;

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

A16: Reloc (q,k) c= P +* (Reloc (q,k)) by FUNCT_4:25;

A17: Reloc (q,k) = IncAddr ((Shift (q,k)),k) by COMPOS_1:34;

dom (Shift (pp,k)) = { (m + k) where m is Nat : m in dom pp } by VALUED_1:def 12;

then A18: j + k in dom (Shift (q,k)) by A14;

then A19: IncAddr (((Shift (q,k)) /. kk),k) = (Reloc (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A13, A17, COMPOS_1:def 21

.= (P +* (Reloc (q,k))) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A10, A16, GRFUNC_1:2

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

A20: (j + k) -' k = j by NAT_D:34;

A21: dom P = NAT by PARTFUN1:def 2;

A22: IC (DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)) = (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) -' k),S)) . (IC ) by A12, FUNCT_4:13

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

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

.= q . (IC (Comput (P,s,i))) by A7, A13, A14, A20, A5, A22, GRFUNC_1:2

.= (Shift (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A13, A14, A20, A7, A22, VALUED_1:def 12

.= (Shift (q,k)) /. kk by A13, A18, PARTFUN1:def 6 ;

then A23: ( Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),(i + 1)) = Following ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) & Exec ((CurInstr (P,(Comput (P,s,i)))),(DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k))) = DecIC ((Following ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)))),k) ) by A13, A19, Th5, EXTPRO_1:3;

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

.= DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),(i + 1))),k) by A7, A23 ; :: thesis: verum

end;let i be Nat; :: thesis: ( S

assume A7: Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k) ; :: thesis: S

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

reconsider jk = IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) as Nat ;

A8: IncIC (p,k) c= s +* (IncIC (p,k)) by FUNCT_4:25;

A9: Reloc (q,k) c= P +* (Reloc (q,k)) by FUNCT_4:25;

A10: IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) in dom (Reloc (q,k)) by A4, Def4, A8, A9;

then A11: jk in { (j + k) where j is Nat : j in dom q } by COMPOS_1:33;

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

consider j being Nat such that

A13: jk = j + k and

A14: j in dom q by A11;

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

A16: Reloc (q,k) c= P +* (Reloc (q,k)) by FUNCT_4:25;

A17: Reloc (q,k) = IncAddr ((Shift (q,k)),k) by COMPOS_1:34;

dom (Shift (pp,k)) = { (m + k) where m is Nat : m in dom pp } by VALUED_1:def 12;

then A18: j + k in dom (Shift (q,k)) by A14;

then A19: IncAddr (((Shift (q,k)) /. kk),k) = (Reloc (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A13, A17, COMPOS_1:def 21

.= (P +* (Reloc (q,k))) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A10, A16, GRFUNC_1:2

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

A20: (j + k) -' k = j by NAT_D:34;

A21: dom P = NAT by PARTFUN1:def 2;

A22: IC (DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)) = (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) -' k),S)) . (IC ) by A12, FUNCT_4:13

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

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

.= q . (IC (Comput (P,s,i))) by A7, A13, A14, A20, A5, A22, GRFUNC_1:2

.= (Shift (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A13, A14, A20, A7, A22, VALUED_1:def 12

.= (Shift (q,k)) /. kk by A13, A18, PARTFUN1:def 6 ;

then A23: ( Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),(i + 1)) = Following ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) & Exec ((CurInstr (P,(Comput (P,s,i)))),(DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k))) = DecIC ((Following ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)))),k) ) by A13, A19, Th5, EXTPRO_1:3;

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

.= DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),(i + 1))),k) by A7, A23 ; :: thesis: verum

A25: IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)) = IC (IncIC (p,k)) by A24, FUNCT_4:13;

A26: DataPart p c= p by RELAT_1:59;

set DP = DataPart p;

set IP = Start-At (((IC p) + k),S);

set PP = q;

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

A27: dom (Start-At (((IC p) + k),S)) = {(IC )} ;

set PR = Reloc (q,k);

set SD = s | (dom (Reloc (q,k)));

A28: {(IC )} misses dom (DataPart p) by MEMSTR_0:4;

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

A30: dom (Start-At (((IC p) + k),S)) misses dom (DataPart p) by A28;

A31: (Start-At (((IC p) + k),S)) +* (DataPart p) = (DataPart p) +* (Start-At (((IC p) + k),S)) by A30, FUNCT_4:35

.= IncIC (p,k) by A1, MEMSTR_0:56 ;

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

.= s +* (Start-At ((((IC p) + k) -' k),S)) by NAT_D:34

.= s +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A25, MEMSTR_0:53

.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A26, A3, FUNCT_4:98, XBOOLE_1:1

.= ((s +* (DataPart p)) +* (Start-At (((IC p) + k),S))) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A29, A27, FUNCT_4:74

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

.= DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)),k) by A31, A27, A28, FUNCT_4:35 ;

then A32: S

thus for i being Nat holds S