:: AMISTD_5 semantic presentation
begin
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 Element of NAT holds IncAddr (I,k) is jump-only
proof
let N be with_zero set ; ::_thesis: 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 Element of NAT holds IncAddr (I,k) is jump-only
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of S st I is jump-only holds
for k being Element of NAT holds IncAddr (I,k) is jump-only
let I be Instruction of S; ::_thesis: ( I is jump-only implies for k being Element of NAT holds IncAddr (I,k) is jump-only )
assume A1: I is jump-only ; ::_thesis: for k being Element of NAT holds IncAddr (I,k) is jump-only
let k be Element of NAT ; ::_thesis: IncAddr (I,k) is jump-only
A2: InsCode I = InsCode (IncAddr (I,k)) by COMPOS_0:def_9;
InsCode I is jump-only by A1, AMISTD_1:def_2;
hence IncAddr (I,k) is jump-only by A2, AMISTD_1:def_2; ::_thesis: verum
end;
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 Element of NAT ;
cluster IncAddr (I,k) -> IC-relocable ;
coherence
IncAddr (I,k) is IC-relocable
proof
let j, i be Nat; :: according to AMISTD_2:def_3 ::_thesis: for b1 being set holds (IC (Exec ((IncAddr ((IncAddr (I,k)),j)),b1))) + i = IC (Exec ((IncAddr ((IncAddr (I,k)),(j + i))),(IncIC (b1,i))))
let s be State of S; ::_thesis: (IC (Exec ((IncAddr ((IncAddr (I,k)),j)),s))) + i = IC (Exec ((IncAddr ((IncAddr (I,k)),(j + i))),(IncIC (s,i))))
thus (IC (Exec ((IncAddr ((IncAddr (I,k)),j)),s))) + i = (IC (Exec ((IncAddr (I,(k + j))),s))) + i by COMPOS_0:7
.= IC (Exec ((IncAddr (I,((k + j) + i))),(IncIC (s,i)))) by AMISTD_2:def_3
.= IC (Exec ((IncAddr (I,(k + (j + i)))),(IncIC (s,i))))
.= IC (Exec ((IncAddr ((IncAddr (I,k)),(j + i))),(IncIC (s,i)))) by COMPOS_0:7 ; ::_thesis: verum
end;
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;
attrI is relocable means :Def1: :: AMISTD_5:def 1
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);
end;
:: 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) );
registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
cluster relocable -> IC-relocable for Element of the InstructionsF of S;
coherence
for b1 being Instruction of S st b1 is relocable holds
b1 is IC-relocable
proof
let I be Instruction of S; ::_thesis: ( I is relocable implies I is IC-relocable )
assume A1: I is relocable ; ::_thesis: I is IC-relocable
let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for b1 being set holds (IC (Exec ((IncAddr (I,j)),b1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k))))
let s be State of S; ::_thesis: (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))
reconsider kk = k as Element of NAT by ORDINAL1:def_12;
thus (IC (Exec ((IncAddr (I,j)),s))) + k = IC (IncIC ((Exec ((IncAddr (I,j)),s)),kk)) by MEMSTR_0:53
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) by A1, Def1 ; ::_thesis: verum
end;
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;
attrS is relocable means :Def2: :: AMISTD_5:def 2
for I being Instruction of S holds I is relocable ;
end;
:: 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 );
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)
proof
let N be with_zero set ; ::_thesis: 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)
let I be Instruction of (STC N); ::_thesis: for s being State of (STC N)
for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)
let s be State of (STC N); ::_thesis: for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)
let k be Nat; ::_thesis: Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)
percases ( InsCode I = 1 or InsCode I = 0 ) by AMISTD_1:6;
supposeA1: InsCode I = 1 ; ::_thesis: Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)
hence Exec (I,(IncIC (s,k))) = IncIC ((IncIC (s,k)),1) by AMISTD_1:20
.= IncIC (s,(1 + k)) by MEMSTR_0:57
.= IncIC ((IncIC (s,1)),k) by MEMSTR_0:57
.= IncIC ((Exec (I,s)),k) by A1, AMISTD_1:20 ;
::_thesis: verum
end;
suppose InsCode I = 0 ; ::_thesis: Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)
then A2: I is halting by AMISTD_1:4;
hence Exec (I,(IncIC (s,k))) = IncIC (s,k) by EXTPRO_1:def_3
.= IncIC ((Exec (I,s)),k) by A2, EXTPRO_1:def_3 ;
::_thesis: verum
end;
end;
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;
attrS is IC-recognized means :Def3: :: AMISTD_5:def 3
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of S st not p is empty holds
IC in dom p;
end;
:: deftheorem Def3 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 b2 -valued finite non halt-free Function
for p being b3 -autonomic FinPartState of S st not p is empty holds
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 b2 -valued finite non halt-free Function
for p being b3 -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p )
proof
let N be with_zero set ; ::_thesis: 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 b1 -valued finite non halt-free Function
for p being b2 -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: ( S is IC-recognized iff for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p )
thus ( S is IC-recognized implies for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p ) ::_thesis: ( ( for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p ) implies S is IC-recognized )
proof
assume A1: S is IC-recognized ; ::_thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p
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 DataPart p <> {} holds
IC in dom p
let p be q -autonomic FinPartState of S; ::_thesis: ( DataPart p <> {} implies IC in dom p )
assume DataPart p <> {} ; ::_thesis: IC in dom p
then not p is empty ;
hence IC in dom p by A1, Def3; ::_thesis: verum
end;
assume A2: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p ; ::_thesis: S is IC-recognized
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: according to AMISTD_5:def_3 ::_thesis: for p being q -autonomic FinPartState of S st not p is empty holds
IC in dom p
let p be q -autonomic FinPartState of S; ::_thesis: ( not p is empty implies IC in dom p )
A3: dom p c= {(IC )} \/ (dom (DataPart p)) by MEMSTR_0:32;
assume A4: not p is empty ; ::_thesis: IC in dom p
percases ( IC in dom p or not IC in dom p ) ;
supposeA5: IC in dom p ; ::_thesis: IC in dom p
thus IC in dom p by A5; ::_thesis: verum
end;
suppose not IC in dom p ; ::_thesis: IC in dom p
then {(IC )} misses dom p by ZFMISC_1:50;
then not dom (DataPart p) is empty by A4, A3, XBOOLE_1:3, XBOOLE_1:73;
then not DataPart p is empty ;
hence IC in dom p by A2; ::_thesis: verum
end;
end;
end;
registration
let N be with_zero set ;
cluster NonZero (STC N) -> empty ;
coherence
Data-Locations is empty
proof
the carrier of (STC N) = {0} by AMISTD_1:def_7
.= {(IC )} by AMISTD_1:def_7 ;
hence Data-Locations is empty by XBOOLE_1:37; ::_thesis: verum
end;
end;
registration
let N be with_zero set ;
let p be PartState of (STC N);
cluster DataPart p -> empty ;
coherence
DataPart p is empty ;
end;
registration
let N be with_zero set ;
cluster STC N -> relocable IC-recognized ;
coherence
( STC N is IC-recognized & STC N is relocable )
proof
for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of (STC N) st DataPart p <> {} holds
IC in dom p ;
hence STC N is IC-recognized by Th3; ::_thesis: STC N is relocable
let I be Instruction of (STC N); :: according to AMISTD_5:def_2 ::_thesis: I is relocable
let j, k be Nat; :: according to AMISTD_5:def_1 ::_thesis: for s being State of (STC N) holds Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k)
let s be State of (STC N); ::_thesis: Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k)
thus Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = Exec (I,(IncIC (s,k))) by COMPOS_0:4
.= IncIC ((Exec (I,s)),k) by Th2
.= IncIC ((Exec ((IncAddr (I,j)),s)),k) by COMPOS_0:4 ; ::_thesis: verum
end;
end;
registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting standard relocable IC-recognized for AMI-Struct over N;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st
( b1 is relocable & b1 is IC-recognized )
proof
take STC N ; ::_thesis: ( STC N is relocable & STC N is IC-recognized )
thus ( STC N is relocable & STC N is IC-recognized ) ; ::_thesis: verum
end;
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;
cluster -> relocable for Element of the InstructionsF of S;
coherence
for b1 being Instruction of S holds b1 is relocable by Def2;
end;
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)
proof
let k be Nat; ::_thesis: 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)
let N be with_zero set ; ::_thesis: 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)
let S be non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N; ::_thesis: 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)
let INS be Instruction of S; ::_thesis: for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)
let s be State of S; ::_thesis: Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)
thus Exec ((IncAddr (INS,k)),(IncIC (s,k))) = Exec ((IncAddr (INS,(0 + k))),(IncIC (s,k)))
.= IncIC ((Exec ((IncAddr (INS,0)),s)),k) by Def1
.= IncIC ((Exec (INS,s)),k) by COMPOS_0:3 ; ::_thesis: verum
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 Element of NAT st IC s = j + k holds
Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)
proof
let N be with_zero set ; ::_thesis: 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 Element of NAT st IC s = j + k holds
Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)
let S be non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N; ::_thesis: for INS being Instruction of S
for s being State of S
for j, k being Element of NAT st IC s = j + k holds
Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)
let INS be Instruction of S; ::_thesis: for s being State of S
for j, k being Element of NAT st IC s = j + k holds
Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)
let s be State of S; ::_thesis: for j, k being Element of NAT st IC s = j + k holds
Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)
let j, k be Element of NAT ; ::_thesis: ( IC s = j + k implies Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k) )
assume A1: IC s = j + k ; ::_thesis: Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)
set s1 = s +* (Start-At (j,S));
A2: IncIC ((s +* (Start-At (j,S))),k) = s +* (Start-At ((IC s),S)) by A1, MEMSTR_0:58
.= s by MEMSTR_0:31 ;
thus Exec (INS,(DecIC (s,k))) = Exec (INS,(s +* (Start-At (j,S)))) by A1, NAT_D:34
.= (Exec (INS,(s +* (Start-At (j,S))))) +* (Start-At ((IC (Exec (INS,(s +* (Start-At (j,S)))))),S)) by MEMSTR_0:31
.= (IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)) +* (Start-At ((IC (Exec (INS,(s +* (Start-At (j,S)))))),S)) by FUNCT_4:114
.= DecIC ((IncIC ((Exec (INS,(s +* (Start-At (j,S))))),k)),k) by MEMSTR_0:59
.= DecIC ((Exec ((IncAddr (INS,k)),s)),k) by A2, Th4 ; ::_thesis: verum
end;
registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized for AMI-Struct over N;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N st
( b1 is relocable & b1 is IC-recognized )
proof
take STC N ; ::_thesis: ( STC N is relocable & STC N is IC-recognized )
thus ( STC N is relocable & STC N is IC-recognized ) ; ::_thesis: verum
end;
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 b2 -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of S holds IC in dom p
proof
let N be with_zero set ; ::_thesis: 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 b1 -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of S holds IC in dom p
let S be non empty with_non-empty_values IC-Ins-separated halting IC-recognized AMI-Struct over N; ::_thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of S holds IC in dom p
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of S holds IC in dom p
let p be non empty q -autonomic FinPartState of S; ::_thesis: IC in dom p
A1: dom p meets {(IC )} \/ (Data-Locations ) by MEMSTR_0:41;
percases ( dom p meets {(IC )} or dom p meets Data-Locations ) by A1, XBOOLE_1:70;
suppose dom p meets {(IC )} ; ::_thesis: IC in dom p
hence IC in dom p by ZFMISC_1:50; ::_thesis: verum
end;
suppose dom p meets Data-Locations ; ::_thesis: IC in dom p
then (dom p) /\ (Data-Locations ) <> {} by XBOOLE_0:def_7;
then DataPart p <> {} by RELAT_1:38, RELAT_1:61;
hence IC in dom p by Th3; ::_thesis: verum
end;
end;
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;
attrS 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 b1 -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 Element of NAT holds IC (Comput (P,s,i)) in dom q;
end;
:: 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 b2 -valued finite non halt-free Function
for p being non empty b3 -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 Element of NAT holds IC (Comput (P,s,i)) in dom q );
registration
let N be with_zero set ;
cluster STC N -> CurIns-recognized ;
coherence
STC N is CurIns-recognized
proof
let q be NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function; :: according to AMISTD_5:def_4 ::_thesis: for p being non empty q -autonomic FinPartState of (STC N)
for s being State of (STC N) st p c= s holds
for P being Instruction-Sequence of (STC N) st q c= P holds
for i being Element of NAT holds IC (Comput (P,s,i)) in dom q
let p be non empty q -autonomic FinPartState of (STC N); ::_thesis: for s being State of (STC N) st p c= s holds
for P being Instruction-Sequence of (STC N) st q c= P holds
for i being Element of NAT holds IC (Comput (P,s,i)) in dom q
let s be State of (STC N); ::_thesis: ( p c= s implies for P being Instruction-Sequence of (STC N) st q c= P holds
for i being Element of NAT holds IC (Comput (P,s,i)) in dom q )
assume A1: p c= s ; ::_thesis: for P being Instruction-Sequence of (STC N) st q c= P holds
for i being Element of NAT holds IC (Comput (P,s,i)) in dom q
let P be Instruction-Sequence of (STC N); ::_thesis: ( q c= P implies for i being Element of NAT holds IC (Comput (P,s,i)) in dom q )
assume A2: q c= P ; ::_thesis: for i being Element of NAT holds IC (Comput (P,s,i)) in dom q
let i be Element of NAT ; ::_thesis: IC (Comput (P,s,i)) in dom q
set Csi = Comput (P,s,i);
set loc = IC (Comput (P,s,i));
set loc1 = (IC (Comput (P,s,i))) + 1;
assume A3: not IC (Comput (P,s,i)) in dom q ; ::_thesis: contradiction
the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def_7;
then reconsider I = [1,0,0] as Instruction of (STC N) by TARSKI:def_2;
set p1 = q +* ((IC (Comput (P,s,i))) .--> I);
set p2 = q +* ((IC (Comput (P,s,i))) .--> (halt (STC N)));
reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> I) as Instruction-Sequence of (STC N) ;
reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt (STC N))) as Instruction-Sequence of (STC N) ;
A4: dom ((IC (Comput (P,s,i))) .--> (halt (STC N))) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13;
then A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt (STC N))) by TARSKI:def_1;
A6: dom ((IC (Comput (P,s,i))) .--> I) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13;
then A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> I) by TARSKI:def_1;
A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt (STC N))) by A3, A4, ZFMISC_1:50;
A9: dom q misses dom ((IC (Comput (P,s,i))) .--> I) by A3, A6, ZFMISC_1:50;
A10: q +* ((IC (Comput (P,s,i))) .--> I) c= P1 by A2, FUNCT_4:123;
A11: q +* ((IC (Comput (P,s,i))) .--> (halt (STC N))) c= P2 by A2, FUNCT_4:123;
set Cs2i = Comput (P2,s,i);
set Cs1i = Comput (P1,s,i);
not p is q -autonomic
proof
((IC (Comput (P,s,i))) .--> (halt (STC N))) . (IC (Comput (P,s,i))) = halt (STC N) by FUNCOP_1:72;
then A12: P2 . (IC (Comput (P,s,i))) = halt (STC N) by A5, FUNCT_4:13;
((IC (Comput (P,s,i))) .--> I) . (IC (Comput (P,s,i))) = I by FUNCOP_1:72;
then A13: P1 . (IC (Comput (P,s,i))) = I by A7, FUNCT_4:13;
take P1 ; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st
( q c= P1 & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (proj1 p) = (Comput (b1,b3,b4)) | (proj1 p) ) )
take P2 ; ::_thesis: ( q c= P1 & q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> I) by A9, FUNCT_4:32;
hence A14: q c= P1 by A10, XBOOLE_1:1; ::_thesis: ( q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> (halt (STC N))) by A8, FUNCT_4:32;
hence A15: q c= P2 by A11, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) )
take s ; ::_thesis: ex b1 being set st
( p c= s & p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s,b2)) | (proj1 p) = (Comput (P2,b1,b2)) | (proj1 p) )
take s ; ::_thesis: ( p c= s & p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 p) = (Comput (P2,s,b1)) | (proj1 p) )
thus p c= s by A1; ::_thesis: ( p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 p) = (Comput (P2,s,b1)) | (proj1 p) )
A16: (Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p) by A14, A2, A1, EXTPRO_1:def_10;
thus p c= s by A1; ::_thesis: not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 p) = (Comput (P2,s,b1)) | (proj1 p)
A17: (Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p) by A14, A15, A1, EXTPRO_1:def_10;
take k = i + 1; ::_thesis: not (Comput (P1,s,k)) | (proj1 p) = (Comput (P2,s,k)) | (proj1 p)
set Cs1k = Comput (P1,s,k);
A18: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s,i)))),(Comput (P1,s,i))) ;
InsCode I = 1 by RECDEF_2:def_1;
then A19: IC (Exec (I,(Comput (P1,s,i)))) = succ (IC (Comput (P1,s,i))) by AMISTD_1:9;
A20: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by Th6, FUNCT_1:49;
then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, Th6, FUNCT_1:49;
then A21: IC (Comput (P1,s,k)) = (IC (Comput (P,s,i))) + 1 by A19, A18, A13, PBOOLE:143;
set Cs2k = Comput (P2,s,k);
A22: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ;
A23: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:143;
IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A16, A20, A17, Th6, FUNCT_1:49;
then A24: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A22, A12, A23, EXTPRO_1:def_3;
( IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) ) by Th6, FUNCT_1:49;
hence not (Comput (P1,s,k)) | (proj1 p) = (Comput (P2,s,k)) | (proj1 p) by A21, A24; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
end;
registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized for AMI-Struct over N;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N st
( b1 is relocable & b1 is IC-recognized & b1 is CurIns-recognized )
proof
take STC N ; ::_thesis: ( STC N is relocable & STC N is IC-recognized & STC N is CurIns-recognized )
thus ( STC N is relocable & STC N is IC-recognized & STC N is CurIns-recognized ) ; ::_thesis: verum
end;
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 b2 -valued finite non halt-free Function
for p being non empty b3 -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 Element of 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
let N be with_zero set ; ::_thesis: 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 b1 -valued finite non halt-free Function
for p being non empty b2 -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 Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let S be non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N; ::_thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -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 Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; ::_thesis: for p being non empty q -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 Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let p be non empty q -autonomic FinPartState of S; ::_thesis: 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 Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let s1, s2 be State of S; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )
assume that
A1: p c= s1 and
A2: p c= s2 ; ::_thesis: for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let P1, P2 be Instruction-Sequence of S; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )
assume that
A3: q c= P1 and
A4: q c= P2 ; ::_thesis: for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
A5: dom q c= dom P1 by A3, RELAT_1:11;
A6: dom q c= dom P2 by A4, RELAT_1:11;
let i be Element of NAT ; ::_thesis: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
A7: IC (Comput (P1,s1,i)) in dom q by A3, Def4, A1;
A8: IC (Comput (P2,s2,i)) in dom q by A4, Def4, A2;
thus A9: IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) ::_thesis: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i)))
proof
assume A10: IC (Comput (P1,s1,i)) <> IC (Comput (P2,s2,i)) ; ::_thesis: contradiction
( ((Comput (P1,s1,i)) | (dom p)) . (IC ) = (Comput (P1,s1,i)) . (IC ) & ((Comput (P2,s2,i)) | (dom p)) . (IC ) = (Comput (P2,s2,i)) . (IC ) ) by Th6, FUNCT_1:49;
hence contradiction by A10, A3, A4, A1, A2, EXTPRO_1:def_10; ::_thesis: verum
end;
thus CurInstr (P1,(Comput (P1,s1,i))) = P1 . (IC (Comput (P1,s1,i))) by A7, A5, PARTFUN1:def_6
.= q . (IC (Comput (P1,s1,i))) by A7, A3, GRFUNC_1:2
.= P2 . (IC (Comput (P2,s2,i))) by A8, A4, A9, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,i))) by A8, A6, PARTFUN1:def_6 ; ::_thesis: verum
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 Element of NAT
for q being NAT -defined the InstructionsF of b2 -valued finite non halt-free Function
for p being b4 -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 Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)
proof
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 Element of NAT
for q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being b3 -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 Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,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 Element of NAT
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b2 -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 Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)
let k be Element of NAT ; ::_thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -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 Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,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 p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)
let p be q -autonomic FinPartState of S; ::_thesis: ( IC in dom p implies 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 Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k) )
assume A1: IC in dom p ; ::_thesis: 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 Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)
let s be State of S; ::_thesis: ( p c= s implies for P being Instruction-Sequence of S st q c= P holds
for i being Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k) )
assume A2: p c= s ; ::_thesis: for P being Instruction-Sequence of S st q c= P holds
for i being Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)
let P be Instruction-Sequence of S; ::_thesis: ( q c= P implies for i being Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k) )
assume A3: q c= P ; ::_thesis: for i being Element of NAT holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)
defpred S1[ Element of NAT ] means Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),$1) = IncIC ((Comput (P,s,$1)),k);
A4: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A5: Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k) ; ::_thesis: S1[i + 1]
reconsider kk = IC (Comput (P,s,i)) as Element of NAT ;
dom (Start-At (((IC (Comput (P,s,i))) + k),S)) = {(IC )} by FUNCOP_1:13;
then A6: IC in dom (Start-At (((IC (Comput (P,s,i))) + k),S)) by TARSKI:def_1;
A7: IC (IncIC ((Comput (P,s,i)),k)) = IC (Start-At (((IC (Comput (P,s,i))) + k),S)) by A6, FUNCT_4:13
.= (IC (Comput (P,s,i))) + k by FUNCOP_1:72 ;
not p is empty by A1;
then A8: IC (Comput (P,s,i)) in dom q by A3, Def4, A2;
then A9: IC (Comput (P,s,i)) in dom (IncAddr (q,k)) by COMPOS_1:def_21;
A10: q /. kk = q . (IC (Comput (P,s,i))) by A8, PARTFUN1:def_6
.= P . (IC (Comput (P,s,i))) by A8, A3, GRFUNC_1:2 ;
reconsider kk = IC (Comput (P,s,i)) as Element of NAT ;
A11: (IC (Comput (P,s,i))) + k in dom (Reloc (q,k)) by A8, COMPOS_1:46;
A12: CurInstr ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) = (P +* (Reloc (q,k))) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by PBOOLE:143
.= (Reloc (q,k)) . ((IC (Comput (P,s,i))) + k) by A5, A7, A11, FUNCT_4:13
.= (IncAddr (q,k)) . kk by A9, VALUED_1:def_12
.= IncAddr ((q /. kk),k) by A8, COMPOS_1:def_21
.= IncAddr ((CurInstr (P,(Comput (P,s,i)))),k) by A10, PBOOLE:143 ;
thus 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))) by EXTPRO_1:3
.= IncIC ((Following (P,(Comput (P,s,i)))),k) by A5, A12, Th4
.= IncIC ((Comput (P,s,(i + 1))),k) by EXTPRO_1:3 ; ::_thesis: verum
end;
A13: IC p = IC s by A2, A1, GRFUNC_1:2;
A14: DataPart p c= p by MEMSTR_0:12;
Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0) = s +* ((DataPart p) +* (Start-At (((IC p) + k),S))) by A1, MEMSTR_0:56
.= (s +* (DataPart p)) +* (Start-At (((IC p) + k),S)) by FUNCT_4:14
.= IncIC ((Comput (P,s,0)),k) by A13, A14, A2, FUNCT_4:98, XBOOLE_1:1 ;
then A15: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A15, A4); ::_thesis: verum
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 Element of NAT
for q being NAT -defined the InstructionsF of b2 -valued finite non halt-free Function
for p being b4 -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 Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
proof
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 Element of NAT
for q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being b3 -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 Element of 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 Element of NAT
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b2 -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 Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let k be Element of NAT ; ::_thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
defpred S1[ Element of NAT ] means Comput (P,s,$1) = IncIC ((Comput ((P +* q),(s +* p),$1)),k);
A4: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A5: Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) ; ::_thesis: S1[i + 1]
reconsider kk = IC (Comput ((P +* q),(s +* p),i)) as Element of NAT ;
dom (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S)) = {(IC )} by FUNCOP_1:13;
then 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 Element of 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;
set IP = Start-At ((IC p),S);
A17: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:13;
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 )} by FUNCOP_1:13;
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: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A22, A4); ::_thesis: verum
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 Element of NAT
for q being NAT -defined the InstructionsF of b2 -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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)
proof
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 Element of NAT
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 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 Element of 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 Element of 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)
let k be Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)
defpred S1[ Element of NAT ] means Comput (P,s,$1) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),$1)),k);
A6: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
reconsider pp = q as preProgram of S ;
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A7: Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k) ; ::_thesis: S1[i + 1]
reconsider kk = IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) as Element of NAT ;
reconsider jk = IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) as Element of 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 Element of NAT : j in dom q } by COMPOS_1:33;
dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) -' k),S)) = {(IC )} by FUNCOP_1:13;
then 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 Element of 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 Element of 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, COMPOS_1:def_21, A17
.= (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;
A24: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
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 )} by FUNCOP_1:13;
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 )} by FUNCOP_1:13;
A30: dom (Start-At (((IC p) + k),S)) misses dom (DataPart p) by A28, FUNCOP_1:13;
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: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A32, A6); ::_thesis: verum
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 b2 -valued finite non halt-free Function
for p being non empty FinPartState of S st IC in dom p holds
for k being Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
proof
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 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 Element of 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; ::_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 k being Element of 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; ::_thesis: for p being non empty FinPartState of S st IC in dom p holds
for k being Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let p be non empty FinPartState of S; ::_thesis: ( IC in dom p implies for k being Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic ) )
assume A1: IC in dom p ; ::_thesis: for k being Element of NAT holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
let k be Element of NAT ; ::_thesis: ( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )
hereby ::_thesis: ( IncIC (p,k) is Reloc (q,k) -autonomic implies p is q -autonomic )
assume A2: p is q -autonomic ; ::_thesis: IncIC (p,k) is Reloc (q,k) -autonomic
thus IncIC (p,k) is Reloc (q,k) -autonomic ::_thesis: verum
proof
let P, Q be Instruction-Sequence of S; :: according to EXTPRO_1:def_10 ::_thesis: ( 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 Element of NAT 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 ; ::_thesis: for b1, b2 being set holds
( not IncIC (p,k) c= b1 or not IncIC (p,k) c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (IncIC (p,k))) = (Comput (Q,b2,b3)) | (proj1 (IncIC (p,k))) )
let s1, s2 be State of S; ::_thesis: ( not IncIC (p,k) c= s1 or not IncIC (p,k) c= s2 or for b1 being Element of NAT 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 ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (IncIC (p,k))) = (Comput (Q,s2,b1)) | (proj1 (IncIC (p,k)))
let i be Element of NAT ; ::_thesis: (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 )} by FUNCOP_1:13;
then 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 )} by FUNCOP_1:13;
then 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, EXTPRO_1:def_10;
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 ;
A17: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:13;
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 A17, A9, FUNCT_4:23
.= 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 A17, A7, FUNCT_4:23
.= (Comput (Q,s2,i)) | (dom (Start-At (((IC p) + k),S))) by A1, A2, A6, Th9, A4 ;
A19: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:13;
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, A19, 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; ::_thesis: verum
end;
end;
assume A24: IncIC (p,k) is Reloc (q,k) -autonomic ; ::_thesis: p is q -autonomic
A25: DataPart p c= IncIC (p,k) by MEMSTR_0:62;
let P, Q be Instruction-Sequence of S; :: according to EXTPRO_1:def_10 ::_thesis: ( 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 Element of NAT holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
assume that
A26: q c= P and
A27: q c= Q ; ::_thesis: for b1, b2 being set holds
( not p c= b1 or not p c= b2 or for b3 being Element of NAT 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; ::_thesis: ( not p c= s1 or not p c= s2 or for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
assume that
A29: p c= s1 and
A30: p c= s2 ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p)
let i be Element of NAT ; ::_thesis: (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, EXTPRO_1:def_10;
A32: dom (Start-At (((IC (Comput ((Q +* (Reloc (q,k))),(s2 +* (IncIC (p,k))),i))) -' k),S)) = {(IC )} by FUNCOP_1:13;
then 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 )} by FUNCOP_1:13;
then 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 ;
A39: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:13;
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 A39, A34, FUNCT_4:23
.= 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 A39, A32, FUNCT_4:23
.= (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 ; ::_thesis: verum
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;
attrS is relocable1 means :Def5: :: AMISTD_5:def 5
for k being Element of NAT
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b2 -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 Element of NAT holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i)));
attrS is relocable2 means :Def6: :: AMISTD_5:def 6
for k being Element of NAT
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b2 -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 Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p));
end;
:: 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 Element of NAT
for q being NAT -defined the InstructionsF of b2 -valued finite non halt-free Function
for p being non empty b4 -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 Element of 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 Element of NAT
for q being NAT -defined the InstructionsF of b2 -valued finite non halt-free Function
for p being non empty b4 -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 Element of 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 Element of NAT
for q being NAT -defined the InstructionsF of (STC b1) -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of (STC N)
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 Element of 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
let N be with_zero set ; ::_thesis: for k being Element of NAT
for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of (STC N)
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 Element of 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))) )
let k be Element of NAT ; ::_thesis: for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of (STC N)
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 Element of 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))) )
let q be NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of (STC N)
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 Element of 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))) )
let p be non empty q -autonomic FinPartState of (STC N); ::_thesis: 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 Element of 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))) )
let s1, s2 be State of (STC N); ::_thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of 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))) ) )
assume that
A1: p c= s1 and
A2: IncIC (p,k) c= s2 ; ::_thesis: for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of 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))) )
A3: IC in dom p by Th6;
let P1, P2 be Instruction-Sequence of (STC N); ::_thesis: ( q c= P1 & Reloc (q,k) c= P2 implies for i being Element of 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))) ) )
assume A4: ( q c= P1 & Reloc (q,k) c= P2 ) ; ::_thesis: for i being Element of 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))) )
set s3 = s1 +* (DataPart s2);
defpred S1[ Element of NAT ] means ( (IC (Comput (P1,s1,$1))) + k = IC (Comput (P2,s2,$1)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,$1)))),k) = CurInstr (P2,(Comput (P2,s2,$1))) );
A5: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
set DPp = DataPart p;
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume that
A6: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and
A7: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) ; ::_thesis: S1[i + 1]
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i);
set Cs2i = Comput (P2,s2,i);
set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1));
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
A8: now__::_thesis:_(_(IC_(Comput_(P1,s1,(i_+_1))))_+_k_=_IC_(Comput_(P2,s2,(i_+_1)))_implies_IncAddr_((CurInstr_(P1,(Comput_(P1,s1,(i_+_1))))),k)_=_CurInstr_(P2,(Comput_(P2,s2,(i_+_1))))_)
reconsider loc = IC (Comput (P1,s1,(i + 1))) as Element of NAT ;
assume A9: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; ::_thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))
reconsider kk = loc as Element of NAT ;
A10: loc in dom q by Def4, A4, A1;
A11: loc + k in dom (Reloc (q,k)) by A10, COMPOS_1:46;
A12: dom P2 = NAT by PARTFUN1:def_2;
dom P1 = NAT by PARTFUN1:def_2;
then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def_6
.= q . loc by A10, A4, GRFUNC_1:2 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc (q,k)) . (loc + k) by A10, COMPOS_1:35
.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A9, A11, A4, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, PARTFUN1:def_6 ;
::_thesis: verum
end;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A13: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
reconsider j = IC (Comput (P1,s1,i)) as Element of NAT ;
A14: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A15: the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def_7;
percases ( CurInstr (P1,(Comput (P1,s1,i))) = [0,0,0] or CurInstr (P1,(Comput (P1,s1,i))) = [1,0,0] ) by A15, TARSKI:def_2;
suppose CurInstr (P1,(Comput (P1,s1,i))) = [0,0,0] ; ::_thesis: S1[i + 1]
then A16: CurInstr (P1,(Comput (P1,s1,i))) = halt (STC N) ;
thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A14, A16, EXTPRO_1:def_3
.= IC (Comput (P2,s2,(i + 1))) by A6, A13, A16, A7, EXTPRO_1:def_3 ; ::_thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A8; ::_thesis: verum
end;
suppose CurInstr (P1,(Comput (P1,s1,i))) = [1,0,0] ; ::_thesis: S1[i + 1]
then A17: InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 by RECDEF_2:def_1;
then A18: Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i))) = IncIC ((Comput (P2,s2,i)),1) by AMISTD_1:20;
thus (IC (Comput (P1,s1,(i + 1)))) + k = (succ (IC (Comput (P1,s1,i)))) + k by A14, A17, AMISTD_1:9
.= IC (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) by A18, A6, MEMSTR_0:53
.= IC (Comput (P2,s2,(i + 1))) by A13, A7, COMPOS_0:4 ; ::_thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A8; ::_thesis: verum
end;
end;
end;
A19: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
now__::_thesis:_(_(IC_(Comput_(P1,s1,0)))_+_k_=_IC_(Comput_(P2,s2,0))_&_IncAddr_((CurInstr_(P1,(Comput_(P1,s1,0)))),k)_=_CurInstr_(P2,(Comput_(P2,s2,0)))_)
thus (IC (Comput (P1,s1,0))) + k = (IC p) + k by A1, A3, GRFUNC_1:2
.= IC (IncIC (p,k)) by MEMSTR_0:53
.= IC (Comput (P2,s2,0)) by A2, A19, GRFUNC_1:2 ; ::_thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0)))
reconsider loc = IC p as Element of NAT ;
A20: IC p = IC s1 by A1, A3, GRFUNC_1:2;
IC p = IC (Comput (P1,s1,0)) by A1, A3, GRFUNC_1:2;
then A21: loc in dom q by Def4, A4, A1;
A22: (IC p) + k in dom (Reloc (q,k)) by A21, COMPOS_1:46;
A23: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
A24: q . (IC p) = P1 . (IC s1) by A20, A21, A4, GRFUNC_1:2;
dom P2 = NAT by PARTFUN1:def_2;
then A25: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def_6
.= P2 . (IC (IncIC (p,k))) by A2, A23, GRFUNC_1:2
.= P2 . ((IC p) + k) by MEMSTR_0:53
.= (Reloc (q,k)) . ((IC p) + k) by A22, A4, GRFUNC_1:2 ;
A26: dom P1 = NAT by PARTFUN1:def_2;
CurInstr (P1,(Comput (P1,s1,0))) = P1 . (IC s1) by A26, PARTFUN1:def_6;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A25, A21, A24, COMPOS_1:35; ::_thesis: verum
end;
then A27: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A27, A5); ::_thesis: verum
end;
registration
let N be with_zero set ;
cluster STC N -> relocable1 relocable2 ;
coherence
( STC N is relocable1 & STC N is relocable2 )
proof
thus for k being Element of NAT
for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of (STC N)
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 Element of NAT holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) by Lm1; :: according to AMISTD_5:def_5 ::_thesis: STC N is relocable2
let k be Element of NAT ; :: according to AMISTD_5:def_6 ::_thesis: for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of (STC N)
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 Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p))
let q be NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of (STC N)
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 Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p))
let p be non empty q -autonomic FinPartState of (STC N); ::_thesis: 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 Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p))
let s1, s2 be State of (STC N); ::_thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) )
assume that
p c= s1 and
IncIC (p,k) c= s2 ; ::_thesis: for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p))
let P1, P2 be Instruction-Sequence of (STC N); ::_thesis: ( q c= P1 & Reloc (q,k) c= P2 implies for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) )
assume that
q c= P1 and
Reloc (q,k) c= P2 ; ::_thesis: for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p))
let i be Element of NAT ; ::_thesis: (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p))
thus (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) ; ::_thesis: verum
end;
end;
registration
let N be with_zero set ;
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 b1 being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N st
( b1 is relocable1 & b1 is relocable2 )
proof
take STC N ; ::_thesis: ( STC N is relocable1 & STC N is relocable2 )
thus ( STC N is relocable1 & STC N is relocable2 ) ; ::_thesis: verum
end;
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 b2 -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
proof
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 q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
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 q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let p be non empty q -autonomic FinPartState of S; ::_thesis: for k being Element of NAT st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
let k be Element of NAT ; ::_thesis: ( IC in dom p implies ( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted ) )
assume IC in dom p ; ::_thesis: ( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )
hereby ::_thesis: ( IncIC (p,k) is Reloc (q,k) -halted implies p is q -halted )
assume A1: p is q -halted ; ::_thesis: IncIC (p,k) is Reloc (q,k) -halted
thus IncIC (p,k) is Reloc (q,k) -halted ::_thesis: verum
proof
let t be State of S; :: according to EXTPRO_1:def_11 ::_thesis: ( not IncIC (p,k) c= t or for b1 being set holds
( not Reloc (q,k) c= b1 or b1 halts_on t ) )
assume A2: IncIC (p,k) c= t ; ::_thesis: for b1 being set holds
( not Reloc (q,k) c= b1 or b1 halts_on t )
let P be Instruction-Sequence of S; ::_thesis: ( not Reloc (q,k) c= P or P halts_on t )
assume A3: Reloc (q,k) c= P ; ::_thesis: P halts_on t
reconsider Q = P +* q as Instruction-Sequence of S ;
set s = t +* p;
A4: q c= Q by FUNCT_4:25;
A5: p c= t +* p by FUNCT_4:25;
then Q halts_on t +* p by A1, A4, EXTPRO_1:def_11;
then consider u being Element of NAT such that
A6: CurInstr (Q,(Comput (Q,(t +* p),u))) = halt S by EXTPRO_1:29;
take u ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,t,u)) in proj1 P & CurInstr (P,(Comput (P,t,u))) = halt S )
dom P = NAT by PARTFUN1:def_2;
hence IC (Comput (P,t,u)) in dom P ; ::_thesis: CurInstr (P,(Comput (P,t,u))) = halt S
CurInstr (P,(Comput (P,t,u))) = IncAddr ((halt S),k) by A2, A6, Def5, A3, A4, A5
.= halt S by COMPOS_0:4 ;
hence CurInstr (P,(Comput (P,t,u))) = halt S ; ::_thesis: verum
end;
end;
assume A7: IncIC (p,k) is Reloc (q,k) -halted ; ::_thesis: p is q -halted
let t be State of S; :: according to EXTPRO_1:def_11 ::_thesis: ( not p c= t or for b1 being set holds
( not q c= b1 or b1 halts_on t ) )
assume A8: p c= t ; ::_thesis: for b1 being set holds
( not q c= b1 or b1 halts_on t )
let P be Instruction-Sequence of S; ::_thesis: ( not q c= P or P halts_on t )
assume A9: q c= P ; ::_thesis: P halts_on t
reconsider Q = P +* (Reloc (q,k)) as Instruction-Sequence of S ;
set s = t +* (IncIC (p,k));
A10: Reloc (q,k) c= Q by FUNCT_4:25;
A11: IncIC (p,k) c= t +* (IncIC (p,k)) by FUNCT_4:25;
then Q halts_on t +* (IncIC (p,k)) by A7, A10, EXTPRO_1:def_11;
then consider u being Element of NAT such that
A12: CurInstr (Q,(Comput (Q,(t +* (IncIC (p,k))),u))) = halt S by EXTPRO_1:29;
take u ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,t,u)) in proj1 P & CurInstr (P,(Comput (P,t,u))) = halt S )
dom P = NAT by PARTFUN1:def_2;
hence IC (Comput (P,t,u)) in dom P ; ::_thesis: CurInstr (P,(Comput (P,t,u))) = halt S
IncAddr ((CurInstr (P,(Comput (P,t,u)))),k) = halt S by A8, A12, Def5, A11, A9, A10
.= IncAddr ((halt S),k) by COMPOS_0:4 ;
hence CurInstr (P,(Comput (P,t,u))) = halt S by COMPOS_0:6; ::_thesis: verum
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 b2 -valued finite non halt-free Function
for p being non empty b3 -autonomic b3 -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
proof
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 q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being non empty b2 -autonomic b2 -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
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 q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -autonomic b1 -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
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 Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
let p be non empty q -autonomic q -halted FinPartState of S; ::_thesis: ( IC in dom p implies for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k)))) )
assume A1: IC in dom p ; ::_thesis: for k being Element of NAT holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
let k be Element of NAT ; ::_thesis: DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))
consider s being State of S such that
A2: p c= s by PBOOLE:141;
consider P being Instruction-Sequence of S such that
A3: q c= P by PBOOLE:145;
A4: ( IncIC (p,k) is Reloc (q,k) -halted & IncIC (p,k) is Reloc (q,k) -autonomic ) by A1, Th12, Th11;
A5: IncIC (p,k) is Autonomy of Reloc (q,k) by A4, EXTPRO_1:def_12;
P halts_on s by A2, A3, EXTPRO_1:def_11;
then consider j1 being Element of NAT such that
A6: Result (P,s) = Comput (P,s,j1) and
A7: CurInstr (P,(Result (P,s))) = halt S by EXTPRO_1:def_9;
consider t being State of S such that
A8: IncIC (p,k) c= t by PBOOLE:141;
consider Q being Instruction-Sequence of S such that
A9: Reloc (q,k) c= Q by PBOOLE:145;
Q . (IC (Comput (Q,t,j1))) = CurInstr (Q,(Comput (Q,t,j1))) by PBOOLE:143
.= IncAddr ((CurInstr (P,(Comput (P,s,j1)))),k) by Def5, A3, A9, A2, A8
.= halt S by A6, A7, COMPOS_0:4 ;
then A10: Result (Q,t) = Comput (Q,t,j1) by EXTPRO_1:7;
A11: (Comput (Q,t,j1)) | (dom (DataPart p)) = (Comput (P,s,j1)) | (dom (DataPart p)) by Def6, A9, A3, A8, A2;
A12: DataPart p = DataPart (IncIC (p,k)) by MEMSTR_0:51;
A13: p is Autonomy of q by EXTPRO_1:def_12;
thus DataPart (Result (q,p)) = DataPart ((Result (P,s)) | (dom p)) by A2, A3, A13, EXTPRO_1:def_13
.= (Result (P,s)) | ((dom p) /\ (Data-Locations )) by RELAT_1:71
.= (Result (P,s)) | (dom (DataPart p)) by MEMSTR_0:14
.= (Result (Q,t)) | ((dom (IncIC (p,k))) /\ (Data-Locations )) by A6, A10, A11, A12, MEMSTR_0:14
.= ((Result (Q,t)) | (dom (IncIC (p,k)))) | (Data-Locations ) by RELAT_1:71
.= DataPart (Result ((Reloc (q,k)),(IncIC (p,k)))) by A5, A9, A8, EXTPRO_1:def_13 ; ::_thesis: verum
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 Element of NAT ;
cluster IncIC (p,k) -> Reloc (q,k) -halted ;
coherence
IncIC (p,k) is Reloc (q,k) -halted
proof
IC in dom p by Th6;
hence IncIC (p,k) is Reloc (q,k) -halted by Th12; ::_thesis: verum
end;
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 Element of NAT
for q being NAT -defined the InstructionsF of b2 -valued finite non halt-free Function
for p being non empty b5 -autonomic b5 -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds
( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )
proof
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 Element of NAT
for q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being non empty b4 -autonomic b4 -halted FinPartState of S st IC in dom p holds
for k being Element of 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 Element of NAT
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b3 -autonomic b3 -halted FinPartState of S st IC in dom p holds
for k being Element of 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 Element of NAT
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b2 -autonomic b2 -halted FinPartState of S st IC in dom p holds
for k being Element of NAT holds
( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )
let l be Element of NAT ; ::_thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -autonomic b1 -halted FinPartState of S st IC in dom p holds
for k being Element of 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 Element of 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 Element of 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 Element of NAT holds
( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )
let k be Element of 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 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
proof
let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( not x in proj1 F or ex b1 being set st
( x = b1 & (IncIC (p,k)) +* b1 is Autonomy of Reloc (q,k) & F . b1 c= Result ((Reloc (q,k)),((IncIC (p,k)) +* b1)) ) )
assume A3: x in dom F ; ::_thesis: ex b1 being set st
( x = b1 & (IncIC (p,k)) +* b1 is Autonomy of Reloc (q,k) & F . b1 c= Result ((Reloc (q,k)),((IncIC (p,k)) +* b1)) )
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, EXTPRO_1:def_14;
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;
end;
assume A13: Reloc (q,k), IncIC (p,k) computes F ; ::_thesis: q,p computes F
let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( not x in proj1 F or ex b1 being set st
( x = b1 & p +* b1 is Autonomy of q & F . b1 c= Result (q,(p +* b1)) ) )
assume A14: x in dom F ; ::_thesis: ex b1 being set st
( x = b1 & p +* b1 is Autonomy of q & F . b1 c= Result (q,(p +* b1)) )
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, EXTPRO_1:def_14;
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
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 b2 -valued finite non halt-free Function
for p being b3 -autonomic FinPartState of S st IC in dom p holds
IC p in dom q
proof
let N be with_zero set ; ::_thesis: 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 b1 -valued finite non halt-free Function
for p being b2 -autonomic FinPartState of S st IC in dom p holds
IC p in dom q
let S be non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N; ::_thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of S st IC in dom p holds
IC p in dom q
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
IC p in dom q
let p be q -autonomic FinPartState of S; ::_thesis: ( IC in dom p implies IC p in dom q )
assume A1: IC in dom p ; ::_thesis: IC p in dom q
then A2: not p is empty ;
consider s being State of S such that
A3: p c= s by PBOOLE:141;
set P = the Instruction-Sequence of S +* q;
A4: q c= the Instruction-Sequence of S +* q by FUNCT_4:25;
IC (Comput (( the Instruction-Sequence of S +* q),s,0)) in dom q by A4, Def4, A2, A3;
hence IC p in dom q by A3, A1, GRFUNC_1:2; ::_thesis: verum
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;
attrF is k -halting means :Def7: :: 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;
end;
:: deftheorem Def7 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 b2 -valued Function holds
( F is k -halting iff for s being b3 -started State of S
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;
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 b1 being NAT -defined the InstructionsF of S -valued Function st b1 is parahalting holds
b1 is 0 -halting
proof
let F be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( F is parahalting implies F is 0 -halting )
assume A1: F is parahalting ; ::_thesis: F is 0 -halting
let s be 0 -started State of S; :: according to AMISTD_5:def_7 ::_thesis: for P being Instruction-Sequence of S st F c= P holds
P halts_on s
thus for P being Instruction-Sequence of S st F c= P holds
P halts_on s by A1, AMISTD_1:def_11; ::_thesis: verum
end;
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 b1 being NAT -defined the InstructionsF of S -valued Function st b1 is 0 -halting holds
b1 is parahalting
proof
let F be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( F is 0 -halting implies F is parahalting )
assume A2: F is 0 -halting ; ::_thesis: F is parahalting
let s be 0 -started State of S; :: according to AMISTD_1:def_11 ::_thesis: for b1 being set holds
( not F c= b1 or b1 halts_on s )
thus for b1 being set holds
( not F c= b1 or b1 halts_on s ) by A2, Def7; ::_thesis: verum
end;
end;