:: by Andrzej Trybulec

::

:: Received November 20, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

theorem :: AMISTD_5:1

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of S st I is jump-only holds

for k being Nat holds IncAddr (I,k) is jump-only by COMPOS_0:def 9;

for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of S st I is jump-only holds

for k being Nat holds IncAddr (I,k) is jump-only by COMPOS_0:def 9;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N;

let I be IC-relocable Instruction of S;

let k be Nat;

coherence

IncAddr (I,k) is IC-relocable

end;
let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N;

let I be IC-relocable Instruction of S;

let k be Nat;

coherence

IncAddr (I,k) is IC-relocable

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

let I be Instruction of S;

end;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

let I be Instruction of S;

:: deftheorem Def1 defines relocable AMISTD_5:def 1 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N

for I being Instruction of S holds

( I is relocable iff for j, k being Nat

for s being State of S holds Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k) );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N

for I being Instruction of S holds

( I is relocable iff for j, k being Nat

for s being State of S holds Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k) );

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

coherence

for b_{1} being Instruction of S st b_{1} is relocable holds

b_{1} is IC-relocable

end;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

coherence

for b

b

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

end;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

attr S is relocable means :Def2: :: AMISTD_5:def 2

for I being Instruction of S holds I is relocable ;

for I being Instruction of S holds I is relocable ;

:: deftheorem Def2 defines relocable AMISTD_5:def 2 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds

( S is relocable iff for I being Instruction of S holds I is relocable );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds

( S is relocable iff for I being Instruction of S holds I is relocable );

theorem Th2: :: AMISTD_5:2

for N being with_zero set

for I being Instruction of (STC N)

for s being State of (STC N)

for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

for I being Instruction of (STC N)

for s being State of (STC N)

for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

end;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

attr S is IC-recognized means :: AMISTD_5:def 3

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 not p is empty holds

IC in dom p;

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

for p being b

IC in dom p;

:: deftheorem defines IC-recognized AMISTD_5:def 3 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds

( S is IC-recognized iff for q being NAT -defined the InstructionsF of b_{2} -valued finite non halt-free Function

for p being b_{3} -autonomic FinPartState of S st not p is empty holds

IC in dom p );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds

( S is IC-recognized iff for q being NAT -defined the InstructionsF of b

for p being b

IC in dom p );

theorem Th3: :: AMISTD_5:3

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds

( S is IC-recognized iff for q being NAT -defined the InstructionsF of b_{2} -valued finite non halt-free Function

for p being b_{3} -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p )

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds

( S is IC-recognized iff for q being NAT -defined the InstructionsF of b

for p being b

IC in dom p )

proof end;

registration
end;

registration
end;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st

( b_{1} is relocable & b_{1} is IC-recognized )

end;
cluster non empty with_non-empty_values IC-Ins-separated halting standard relocable IC-recognized for AMI-Struct over N;

existence ex b

( b

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N;

coherence

for b_{1} being Instruction of S holds b_{1} is relocable
by Def2;

end;
let S be non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N;

coherence

for b

theorem Th4: :: AMISTD_5:4

for k being Nat

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N

for INS being Instruction of S

for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N

for INS being Instruction of S

for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

proof end;

theorem Th5: :: AMISTD_5:5

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N

for INS being Instruction of S

for s being State of S

for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N

for INS being Instruction of S

for s being State of S

for j, k being Nat st IC s = j + k holds

Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

proof end;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N st

( b_{1} is relocable & b_{1} is IC-recognized )

end;
cluster non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized for AMI-Struct over N;

existence ex b

( b

proof end;

theorem Th6: :: AMISTD_5:6

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized AMI-Struct over N

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

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

for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized AMI-Struct over N

for q being NAT -defined the InstructionsF of b

for p being non empty b

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

end;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

attr S is CurIns-recognized means :Def4: :: AMISTD_5:def 4

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

for p being non empty b_{1} -autonomic FinPartState of S

for s being State of S st p c= s holds

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

for i being Nat holds IC (Comput (P,s,i)) in dom q;

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

for p being non empty b

for s being State of S st p c= s holds

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

for i being Nat holds IC (Comput (P,s,i)) in dom q;

:: deftheorem Def4 defines CurIns-recognized AMISTD_5:def 4 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds

( S is CurIns-recognized iff for q being NAT -defined the InstructionsF of b_{2} -valued finite non halt-free Function

for p being non empty b_{3} -autonomic FinPartState of S

for s being State of S st p c= s holds

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

for i being Nat holds IC (Comput (P,s,i)) in dom q );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds

( S is CurIns-recognized iff for q being NAT -defined the InstructionsF of b

for p being non empty b

for s being State of S st p c= s holds

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

for i being Nat holds IC (Comput (P,s,i)) in dom q );

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N st

( b_{1} is relocable & b_{1} is IC-recognized & b_{1} is CurIns-recognized )

end;
cluster non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized for AMI-Struct over N;

existence ex b

( b

proof end;

theorem :: AMISTD_5:7

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N

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

for p being non empty b_{3} -autonomic FinPartState of S

for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N

for q being NAT -defined the InstructionsF of b

for p being non empty b

for s1, s2 being State of S st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds

for i being Nat holds

( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

proof end;

theorem :: AMISTD_5:8

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

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

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

for s being State of S st p c= s holds

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

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

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

for p being b

for s being State of S st p c= s holds

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

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

proof end;

theorem Th9: :: AMISTD_5:9

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

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

for p being b_{4} -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)

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

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)

proof end;

theorem Th10: :: AMISTD_5:10

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

for q being NAT -defined the InstructionsF of b_{2} -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)

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

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)

proof end;

theorem Th11: :: AMISTD_5:11

for N being 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 b_{2} -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 )

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 b

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 )

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N;

end;
let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N;

attr S is relocable1 means :Def5: :: AMISTD_5:def 5

for k 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 FinPartState of S

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

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

for i being Nat holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i)));

for k being Nat

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

for p being non empty b

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

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

for i being Nat holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i)));

attr S is relocable2 means :Def6: :: AMISTD_5:def 6

for k 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 FinPartState of S

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

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

for i being Nat holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p));

for k being Nat

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

for p being non empty b

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

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

for i being Nat holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p));

:: deftheorem Def5 defines relocable1 AMISTD_5:def 5 :

for N being 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 holds

( S is relocable1 iff for k being Nat

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

for p being non empty b_{4} -autonomic FinPartState of S

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

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

for i being Nat holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) );

for N being 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 holds

( S is relocable1 iff for k being Nat

for q being NAT -defined the InstructionsF of b

for p being non empty b

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

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

for i being Nat holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) );

:: deftheorem Def6 defines relocable2 AMISTD_5:def 6 :

for N being 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 holds

( S is relocable2 iff for k being Nat

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

for p being non empty b_{4} -autonomic FinPartState of S

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

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

for i being Nat holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) );

for N being 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 holds

( S is relocable2 iff for k being Nat

for q being NAT -defined the InstructionsF of b

for p being non empty b

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

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

for i being Nat holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) );

Lm1: for N being with_zero set

for k being Nat

for q being NAT -defined the InstructionsF of (STC b

for p being non empty b

for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

proof end;

registration
end;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N st

( b_{1} is relocable1 & b_{1} is relocable2 )

end;
cluster non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 for AMI-Struct over N;

existence ex b

( b

proof end;

theorem Th12: :: AMISTD_5:12

for N being with_zero set

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 q being NAT -defined the InstructionsF of b_{2} -valued finite non halt-free Function

for p being non empty b_{3} -autonomic FinPartState of S

for k being Nat st IC in dom p holds

( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )

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 q being NAT -defined the InstructionsF of b

for p being non empty b

for k being Nat st IC in dom p holds

( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )

proof end;

theorem Th13: :: AMISTD_5:13

for N being with_zero set

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 q being NAT -defined the InstructionsF of b_{2} -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 DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

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 q being NAT -defined the InstructionsF of b

for p being non empty b

for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N;

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function;

let p be non empty q -autonomic q -halted FinPartState of S;

let k be Nat;

coherence

IncIC (p,k) is Reloc (q,k) -halted

end;
let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N;

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function;

let p be non empty q -autonomic q -halted FinPartState of S;

let k be Nat;

coherence

IncIC (p,k) is Reloc (q,k) -halted

proof end;

theorem :: AMISTD_5:14

for N being with_zero set

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_{2} -valued finite non halt-free Function

for p being non empty b_{5} -autonomic b_{5} -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 )

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

for p being non empty b

for k being Nat holds

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

proof end;

theorem :: AMISTD_5:15

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N

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

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

IC p in dom q

for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N

for q being NAT -defined the InstructionsF of b

for p being b

IC p in dom q

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

let k be Nat;

let F be NAT -defined the InstructionsF of S -valued Function;

end;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

let k be Nat;

let F be NAT -defined the InstructionsF of S -valued Function;

attr F is k -halting means :: AMISTD_5:def 7

for s being k -started State of S

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

P halts_on s;

for s being k -started State of S

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

P halts_on s;

:: deftheorem defines -halting AMISTD_5:def 7 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N

for k being Nat

for F being NAT -defined the InstructionsF of b_{2} -valued Function holds

( F is k -halting iff for s being b_{3} -started State of S

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

P halts_on s );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N

for k being Nat

for F being NAT -defined the InstructionsF of b

( F is k -halting iff for s being b

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

P halts_on s );

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

for b_{1} being NAT -defined the InstructionsF of S -valued Function st b_{1} is parahalting holds

b_{1} is 0 -halting
;

for b_{1} being NAT -defined the InstructionsF of S -valued Function st b_{1} is 0 -halting holds

b_{1} is parahalting
;

end;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

cluster Relation-like NAT -defined the InstructionsF of S -valued Function-like parahalting -> NAT -defined the InstructionsF of S -valued 0 -halting for set ;

coherence for b

b

cluster Relation-like NAT -defined the InstructionsF of S -valued Function-like 0 -halting -> NAT -defined the InstructionsF of S -valued parahalting for set ;

coherence for b

b