:: 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;