:: AMISTD_2 semantic presentation

begin


theorem :: AMISTD_2:1
for N being with_zero set
for I being Instruction of (STC N) holds JumpPart I = 0 ;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let I be Instruction of S;
attrI is with_explicit_jumps  means :Def1: :: AMISTD_2:def 1
 JUMP I = rng (JumpPart I);
end;

:: deftheorem Def1 defines with_explicit_jumps AMISTD_2:def_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 holds
( I is with_explicit_jumps iff JUMP I = rng (JumpPart I) );

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
attrS is with_explicit_jumps  means :Def2: :: AMISTD_2:def 2
 for I being Instruction of S holds I is with_explicit_jumps ;
end;

:: deftheorem Def2 defines with_explicit_jumps AMISTD_2:def_2_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds
( S is with_explicit_jumps iff for I being Instruction of S holds I is with_explicit_jumps );

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated standard for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b1 is standard
proof
take  STC N ; ::_thesis: STC N is standard
thus  STC N is standard ; ::_thesis: verum
end;
end;

theorem Th2: :: AMISTD_2:2
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for I being Instruction of S st ( for f being Element of NAT holds NIC (I,f) = {(succ f)} ) holds
JUMP I is empty
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for I being Instruction of S st ( for f being Element of NAT holds NIC (I,f) = {(succ f)} ) holds
JUMP I is empty
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of S st ( for f being Element of NAT holds NIC (I,f) = {(succ f)} ) holds
JUMP I is empty
let I be Instruction of S; ::_thesis: ( ( for f being Element of NAT holds NIC (I,f) = {(succ f)} ) implies JUMP I is empty )
assume A1: for f being Element of NAT holds NIC (I,f) = {(succ f)} ; ::_thesis: JUMP I is empty
set p = 1;
set q = 2;
reconsider p = 1, q = 2 as Element of NAT ;
set X =  {  (NIC (I,f)) where f is Element of NAT : verum  }  ;
assume  not JUMP I is empty ; ::_thesis: contradiction
then consider x being set  such that
A2: x in meet  {  (NIC (I,f)) where f is Element of NAT : verum  }  by XBOOLE_0:def_1;
A3: NIC (I,p) = {(succ p)} by A1;
A4: NIC (I,q) = {(succ q)} by A1;
A5: {(succ p)} in  {  (NIC (I,f)) where f is Element of NAT : verum  }  by A3;
A6: {(succ q)} in  {  (NIC (I,f)) where f is Element of NAT : verum  }  by A4;
A7: x in {(succ p)} by A2, A5, SETFAM_1:def_1;
A8: x in {(succ q)} by A2, A6, SETFAM_1:def_1;
 x = succ p by A7, TARSKI:def_1;
hence  contradiction by A8, TARSKI:def_1; ::_thesis: verum
end;

registration
let N be with_zero set ;
let I be Instruction of (STC N);
cluster JUMP I ->  empty ;
coherence
 JUMP I is empty
proof
percases ( InsCode I = 0 or InsCode I = 1 ) by AMISTD_1:6;
suppose InsCode I = 0 ; ::_thesis: JUMP I is empty
then  for f being Element of NAT holds NIC (I,f) = {f} by AMISTD_1:2, AMISTD_1:4;
hence  JUMP I is empty by AMISTD_1:1; ::_thesis: verum
end;
suppose InsCode I = 1 ; ::_thesis: JUMP I is empty
then  for f being Element of NAT holds NIC (I,f) = {(succ f)} by AMISTD_1:10;
hence  JUMP I is empty by Th2; ::_thesis: verum
end;
end;
end;
end;

theorem :: AMISTD_2:3
for N being with_zero set
for T being InsType of the InstructionsF of (STC N) holds JumpParts T = {0}
proof
let N be with_zero set ; ::_thesis: for T being InsType of the InstructionsF of (STC N) holds JumpParts T = {0}
let T be InsType of the InstructionsF of (STC N); ::_thesis: JumpParts T = {0}
set A =  {  (JumpPart I) where I is Instruction of (STC N) : InsCode I = T  }  ;
 {0} =  {  (JumpPart I) where I is Instruction of (STC N) : InsCode I = T  }
proof
hereby  :: according to XBOOLE_0:def_10,TARSKI:def_3 ::_thesis:  {  (JumpPart I) where I is Instruction of (STC N) : InsCode I = T  }  c= {0}
let a be set ; ::_thesis: ( a in {0} implies b1 in  {  (JumpPart b2) where I is Instruction of (STC N) : InsCode b2 = T  }  )
assume  a in {0} ; ::_thesis: b1 in  {  (JumpPart b2) where I is Instruction of (STC N) : InsCode b2 = T  }
then A1: a = 0 by TARSKI:def_1;
A2: the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def_7;
then A3: InsCodes the InstructionsF of (STC N) = {0,1} by MCART_1:91;
percases ( T = 0 or T = 1 ) by A3, TARSKI:def_2;
supposeA4: T = 0 ; ::_thesis: b1 in  {  (JumpPart b2) where I is Instruction of (STC N) : InsCode b2 = T  }
reconsider I = [0,0,0] as Instruction of (STC N) by A2, TARSKI:def_2;
A5: JumpPart I = 0 ;
 InsCode I = 0 by RECDEF_2:def_1;
hence  a in  {  (JumpPart I) where I is Instruction of (STC N) : InsCode I = T  }  by A1, A4, A5; ::_thesis: verum
end;
supposeA6: T = 1 ; ::_thesis: b1 in  {  (JumpPart b2) where I is Instruction of (STC N) : InsCode b2 = T  }
reconsider I = [1,0,0] as Instruction of (STC N) by A2, TARSKI:def_2;
A7: JumpPart I = 0 ;
 InsCode I = 1 by RECDEF_2:def_1;
hence  a in  {  (JumpPart I) where I is Instruction of (STC N) : InsCode I = T  }  by A1, A6, A7; ::_thesis: verum
end;
end;
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (JumpPart I) where I is Instruction of (STC N) : InsCode I = T  }  or a in {0} )
assume  a in  {  (JumpPart I) where I is Instruction of (STC N) : InsCode I = T  }  ; ::_thesis: a in {0}
then  ex I being Instruction of (STC N) st
( a = JumpPart I & InsCode I = T ) ;
then  a = 0 ;
hence  a in {0} by TARSKI:def_1; ::_thesis: verum
end;
hence  JumpParts T = {0} ; ::_thesis: verum
end;

Lm1:  for N being with_zero set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0
proof
let N be with_zero set ; ::_thesis: for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0
let I be Instruction of (Trivial-AMI N); ::_thesis: JumpPart I = 0
 the InstructionsF of (Trivial-AMI N) = {[0,0,{}]} by EXTPRO_1:def_1;
then  I = [0,0,0] by TARSKI:def_1;
hence  JumpPart I = 0 by RECDEF_2:def_2; ::_thesis: verum
end;

Lm2:  for N being with_zero set
for T being InsType of the InstructionsF of (Trivial-AMI N) holds JumpParts T = {0}
proof
let N be with_zero set ; ::_thesis: for T being InsType of the InstructionsF of (Trivial-AMI N) holds JumpParts T = {0}
let T be InsType of the InstructionsF of (Trivial-AMI N); ::_thesis: JumpParts T = {0}
set A =  {  (JumpPart I) where I is Instruction of (Trivial-AMI N) : InsCode I = T  }  ;
 {0} =  {  (JumpPart I) where I is Instruction of (Trivial-AMI N) : InsCode I = T  }
proof
hereby  :: according to XBOOLE_0:def_10,TARSKI:def_3 ::_thesis:  {  (JumpPart I) where I is Instruction of (Trivial-AMI N) : InsCode I = T  }  c= {0}
let a be set ; ::_thesis: ( a in {0} implies a in  {  (JumpPart I) where I is Instruction of (Trivial-AMI N) : InsCode I = T  }  )
assume  a in {0} ; ::_thesis: a in  {  (JumpPart I) where I is Instruction of (Trivial-AMI N) : InsCode I = T  }
then A1: a = 0 by TARSKI:def_1;
A2: the InstructionsF of (Trivial-AMI N) = {[0,0,{}]} by EXTPRO_1:def_1;
then  InsCodes the InstructionsF of (Trivial-AMI N) = {0} by MCART_1:92;
then A3: T = 0 by TARSKI:def_1;
reconsider I = [0,0,0] as Instruction of (Trivial-AMI N) by A2, TARSKI:def_1;
A4: JumpPart I = 0 by Lm1;
 InsCode I = 0 by RECDEF_2:def_1;
hence  a in  {  (JumpPart I) where I is Instruction of (Trivial-AMI N) : InsCode I = T  }  by A1, A3, A4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (JumpPart I) where I is Instruction of (Trivial-AMI N) : InsCode I = T  }  or a in {0} )
assume  a in  {  (JumpPart I) where I is Instruction of (Trivial-AMI N) : InsCode I = T  }  ; ::_thesis: a in {0}
then  ex I being Instruction of (Trivial-AMI N) st
( a = JumpPart I & InsCode I = T ) ;
then  a = 0 by Lm1;
hence  a in {0} by TARSKI:def_1; ::_thesis: verum
end;
hence  JumpParts T = {0} ; ::_thesis: verum
end;

registration
let N be with_zero set ;
cluster STC N ->  with_explicit_jumps ;
coherence
 STC N is with_explicit_jumps
proof
let I be Instruction of (STC N); :: according to AMISTD_2:def_2 ::_thesis: I is with_explicit_jumps
thus  JUMP I = rng (JumpPart I) ; :: according to AMISTD_2:def_1 ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st
( b1 is standard & b1 is halting & b1 is with_explicit_jumps )
proof
take  STC N ; ::_thesis: ( STC N is standard & STC N is halting & STC N is with_explicit_jumps )
thus  ( STC N is standard & STC N is halting & STC N is with_explicit_jumps ) ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let I be Instruction of (Trivial-AMI N);
cluster JUMP I ->  empty ;
coherence
 JUMP I is empty
proof
 for f being Element of NAT holds NIC (I,f) = {f} by AMISTD_1:2, AMISTD_1:17;
hence  JUMP I is empty by AMISTD_1:1; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster Trivial-AMI N ->  with_explicit_jumps ;
coherence
 Trivial-AMI N is with_explicit_jumps
proof
thus  Trivial-AMI N is with_explicit_jumps ::_thesis: verum
proof
let I be Instruction of (Trivial-AMI N); :: according to AMISTD_2:def_2 ::_thesis: I is with_explicit_jumps
 the InstructionsF of (Trivial-AMI N) = {[0,0,{}]} by EXTPRO_1:def_1;
then  I = [0,0,0] by TARSKI:def_1;
hence  JUMP I = rng (JumpPart I) by RECDEF_2:def_2, RELAT_1:38; :: according to AMISTD_2:def_1 ::_thesis: verum
end;
end;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st
( b1 is with_explicit_jumps & b1 is halting )
proof
take  Trivial-AMI N ; ::_thesis: ( Trivial-AMI N is with_explicit_jumps & Trivial-AMI N is halting )
thus  ( Trivial-AMI N is with_explicit_jumps & Trivial-AMI N is halting ) ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated with_explicit_jumps AMI-Struct over N;
cluster  ->  with_explicit_jumps for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S holds b1 is with_explicit_jumps by Def2;
end;

theorem Th4: :: AMISTD_2:4
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 halting holds
JUMP I is empty
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 halting holds
JUMP I is empty
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 halting holds
JUMP I is empty
let I be Instruction of S; ::_thesis: ( I is halting implies JUMP I is empty )
assume  I is halting ; ::_thesis: JUMP I is empty
then  for l being Element of NAT holds NIC (I,l) = {l} by AMISTD_1:2;
hence  JUMP I is empty by AMISTD_1:1; ::_thesis: verum
end;

registration
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 halting Instruction of S;
cluster JUMP I ->  empty ;
coherence
 JUMP I is empty by Th4;
end;

theorem :: AMISTD_2:5
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N
for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N
for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty
let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N; ::_thesis: for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty
let I be Instruction of S; ::_thesis: ( I is ins-loc-free implies JUMP I is empty )
assume A1: JumpPart I is empty ; :: according to COMPOS_0:def_8 ::_thesis: JUMP I is empty
A2: rng (JumpPart I) = {} by A1;
 JUMP I c= rng (JumpPart I) by Def1;
hence  JUMP I is empty by A2; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated with_explicit_jumps AMI-Struct over N;
cluster halting  ->  ins-loc-free for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is halting holds
b1 is ins-loc-free
proof
let I be Instruction of S; ::_thesis: ( I is halting implies I is ins-loc-free )
assume  I is halting ; ::_thesis: I is ins-loc-free
then A1: JUMP I is empty by Th4;
 rng (JumpPart I) = JUMP I by Def1;
hence  JumpPart I is empty by A1; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated with_explicit_jumps AMI-Struct over N;
cluster sequential  ->  ins-loc-free for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is sequential holds
b1 is ins-loc-free
proof
let I be Instruction of S; ::_thesis: ( I is sequential implies I is ins-loc-free )
assume  I is sequential ; ::_thesis: I is ins-loc-free
then A1: JUMP I is empty by AMISTD_1:13;
 rng (JumpPart I) = JUMP I by Def1;
hence  JumpPart I is empty by A1; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N;
cluster Stop S ->  really-closed ;
coherence
 Stop S is really-closed by AMISTD_1:16;
end;

begin

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 halting Instruction of S;
let k be Nat;
cluster IncAddr (I,k) ->  halting ;
coherence
 IncAddr (I,k) is halting by COMPOS_0:4;
end;

theorem :: AMISTD_2:6
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps AMI-Struct over N
for I being Instruction of S st I is sequential holds
IncAddr (I,k) is sequential by COMPOS_0:4;

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 IC-relocable  means :Def3: :: AMISTD_2:def 3
 for j, k being Nat
for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))));
end;

:: deftheorem Def3 defines IC-relocable AMISTD_2: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
for I being Instruction of S holds
( I is IC-relocable iff for j, k being Nat
for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) );

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-relocable  means :Def4: :: AMISTD_2:def 4
 for I being Instruction of S holds I is IC-relocable ;
end;

:: deftheorem Def4 defines IC-relocable AMISTD_2: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 IC-relocable iff for I being Instruction of S holds I is IC-relocable );

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;
cluster sequential  ->  IC-relocable for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is sequential holds
b1 is IC-relocable
proof
let I be Instruction of S; ::_thesis: ( I is sequential implies I is IC-relocable )
assume A1: I is sequential ; ::_thesis: I is IC-relocable
let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))
let s1 be State of S; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
 dom ((IC ) .--> ((IC s1) + k)) = {(IC )} by FUNCOP_1:13;
then  IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1;
then A2: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13
.= (IC s1) + k by FUNCOP_1:72 ;
A3: IC (Exec (I,(IncIC (s1,k)))) = succ (IC (IncIC (s1,k))) by A1, AMISTD_1:def_8
.= ((IC s1) + 1) + k by A2 ;
A4: IncAddr (I,j) = I by A1, COMPOS_0:4;
IC (Exec (I,s1)) = succ (IC s1) by A1, AMISTD_1:def_8
.= (IC s1) + 1 ;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr ((IncAddr (I,j)),k)),(IncIC (s1,k)))) by A1, A3, A4, COMPOS_0:4
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by COMPOS_0:7 ;
::_thesis: verum
end;
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;
cluster halting  ->  IC-relocable for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is halting holds
b1 is IC-relocable
proof
let I be Instruction of S; ::_thesis: ( I is halting implies I is IC-relocable )
assume A1: I is halting ; ::_thesis: I is IC-relocable
let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))
let s1 be State of S; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
 dom ((IC ) .--> ((IC s1) + k)) = {(IC )} by FUNCOP_1:13;
then A2: IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1;
thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC s1) + k by A1, EXTPRO_1:def_3
.= ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCOP_1:72
.= IC (IncIC (s1,k)) by A2, FUNCT_4:13
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A1, EXTPRO_1:def_3 ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster STC N ->  IC-relocable ;
coherence
 STC N is IC-relocable
proof
thus  STC N is IC-relocable ::_thesis: verum
proof
let I be Instruction of (STC N); :: according to AMISTD_2:def_4 ::_thesis: I is IC-relocable
let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for s being State of (STC N) holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))))
let s1 be State of (STC N); ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
 {(IC )} = dom ((IC ) .--> ((IC s1) + k)) by FUNCOP_1:13;
then  IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1;
then A1: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13
.= (IC s1) + k by FUNCOP_1:72 ;
percases ( InsCode I = 1 or InsCode I = 0 ) by AMISTD_1:6;
supposeA2: InsCode I = 1 ; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
then A3: InsCode (IncAddr (I,k)) = 1 by COMPOS_0:def_9;
A4: IncAddr (I,j) = I by COMPOS_0:4;
IC (Exec (I,s1)) = succ (IC s1) by A2, AMISTD_1:9
.= (IC s1) + 1 ;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k = succ (IC (IncIC (s1,k))) by A1, A4
.= IC (Exec ((IncAddr ((IncAddr (I,j)),k)),(IncIC (s1,k)))) by A4, A3, AMISTD_1:9
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by COMPOS_0:7 ;
::_thesis: verum
end;
suppose InsCode I = 0 ; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
then A5: I is halting by AMISTD_1:4;
hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC s1) + k by EXTPRO_1:def_3
.= IC (Exec ((IncAddr ((IncAddr (I,j)),k)),(IncIC (s1,k)))) by A1, A5, EXTPRO_1:def_3
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by COMPOS_0:7 ;
::_thesis: verum
end;
end;
end;
end;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N st
( b1 is halting & b1 is with_explicit_jumps )
proof
take  STC N ; ::_thesis: ( STC N is halting & STC N is with_explicit_jumps )
thus  ( STC N is halting & STC N is with_explicit_jumps ) ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps IC-relocable for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps AMI-Struct over N st b1 is IC-relocable
proof
take  STC N ; ::_thesis: STC N is IC-relocable
thus  STC N is IC-relocable ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting IC-relocable AMI-Struct over N;
cluster  ->  IC-relocable for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S holds b1 is IC-relocable by Def4;
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;
cluster with_explicit_jumps IC-relocable for Element of the InstructionsF of S;
existence
 ex b1 being Instruction of S st b1 is IC-relocable
proof
take  the halting Instruction of S ; ::_thesis: the halting Instruction of S is IC-relocable
thus  the halting Instruction of S is IC-relocable ; ::_thesis: verum
end;
end;

theorem Th7: :: AMISTD_2:7
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N
for I being IC-relocable Instruction of S
for k being Nat
for s being State of S holds (IC (Exec (I,s))) + k = IC (Exec ((IncAddr (I,k)),(IncIC (s,k))))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N
for I being IC-relocable Instruction of S
for k being Nat
for s being State of S holds (IC (Exec (I,s))) + k = IC (Exec ((IncAddr (I,k)),(IncIC (s,k))))
let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N; ::_thesis: for I being IC-relocable Instruction of S
for k being Nat
for s being State of S holds (IC (Exec (I,s))) + k = IC (Exec ((IncAddr (I,k)),(IncIC (s,k))))
let I be IC-relocable Instruction of S; ::_thesis: for k being Nat
for s being State of S holds (IC (Exec (I,s))) + k = IC (Exec ((IncAddr (I,k)),(IncIC (s,k))))
let k be Nat; ::_thesis: for s being State of S holds (IC (Exec (I,s))) + k = IC (Exec ((IncAddr (I,k)),(IncIC (s,k))))
let s be State of S; ::_thesis: (IC (Exec (I,s))) + k = IC (Exec ((IncAddr (I,k)),(IncIC (s,k))))
A1: k + 0 = k ;
thus (IC (Exec (I,s))) + k = (IC (Exec ((IncAddr (I,0)),s))) + k by COMPOS_0:3
.= IC (Exec ((IncAddr (I,k)),(IncIC (s,k)))) by Def3, A1
.= IC (Exec ((IncAddr (I,k)),(IncIC (s,k)))) ; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps IC-relocable AMI-Struct over N;
let F, G be NAT -defined the InstructionsF of S -valued non empty finite initial really-closed Function;
clusterF ';' G ->  really-closed ;
coherence
 F ';' G is really-closed
proof
set P = F ';' G;
set k = (card F) -' 1;
let f be Element of NAT ; :: according to AMISTD_1:def_9 ::_thesis: ( not f in K485(NAT,(F ';' G)) or NIC (((F ';' G) /. f),f) c= K485(NAT,(F ';' G)) )
assume A1: f in dom (F ';' G) ; ::_thesis: NIC (((F ';' G) /. f),f) c= K485(NAT,(F ';' G))
A2: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def_1;
A3: dom (CutLastLoc F) c= dom F by GRFUNC_1:2;
A4: dom (Reloc (G,((card F) -' 1))) =  {  (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NIC (((F ';' G) /. f),f) or x in K485(NAT,(F ';' G)) )
assume  x in NIC (((F ';' G) /. f),f) ; ::_thesis: x in K485(NAT,(F ';' G))
then consider s2 being Element of product (the_Values_of S) such that
A5: x = IC (Exec (((F ';' G) /. f),s2)) and
A6: IC s2 = f ;
A7: (F ';' G) /. f = (F ';' G) . f by A1, PARTFUN1:def_6;
percases ( f in dom (CutLastLoc F) or f in dom (Reloc (G,((card F) -' 1))) ) by A1, A2, XBOOLE_0:def_3;
supposeA8: f in dom (CutLastLoc F) ; ::_thesis: x in K485(NAT,(F ';' G))
then A9: NIC ((F /. f),f) c= dom F by A3, AMISTD_1:def_9;
 dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by VALUED_1:36;
then A10: f in dom F by A8, XBOOLE_0:def_5;
 dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) by COMPOS_1:18;
then A11: not f in dom (Reloc (G,((card F) -' 1))) by A8, XBOOLE_0:3;
A12: (F ';' G) /. f = (F ';' G) . f by A1, PARTFUN1:def_6
.= (CutLastLoc F) . f by A11, FUNCT_4:11
.= F . f by A8, GRFUNC_1:2
.= F /. f by A10, PARTFUN1:def_6 ;
 IC (Exec ((F /. f),s2)) in NIC ((F /. f),f) by A6;
then A13: x in dom F by A5, A9, A12;
 dom F c= dom (F ';' G) by COMPOS_1:21;
hence  x in K485(NAT,(F ';' G)) by A13; ::_thesis: verum
end;
supposeA14: f in dom (Reloc (G,((card F) -' 1))) ; ::_thesis: x in K485(NAT,(F ';' G))
then consider m being Element of NAT  such that
A15: f = m + ((card F) -' 1) and
A16: m in dom (IncAddr (G,((card F) -' 1))) by A4;
A17: m in dom G by A16, COMPOS_1:def_21;
then A18: NIC ((G /. m),m) c= dom G by AMISTD_1:def_9;
A19: Values (IC ) = NAT by MEMSTR_0:def_6;
reconsider v = (IC ) .--> m as FinPartState of S by A19;
set s1 = s2 +* v;
A20: (F ';' G) /. f = (Reloc (G,((card F) -' 1))) . f by A7, A14, FUNCT_4:13
.= (IncAddr (G,((card F) -' 1))) . m by A15, A16, VALUED_1:def_12 ;
A21: ((IC ) .--> m) . (IC ) = m by FUNCOP_1:72;
A22: IC in {(IC )} by TARSKI:def_1;
A23: dom ((IC ) .--> m) = {(IC )} by FUNCOP_1:13;
reconsider w = (IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)) as FinPartState of S by A19;
A24: dom ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) = the carrier of S by PARTFUN1:def_2;
A25: dom s2 = the carrier of S by PARTFUN1:def_2;
 for a being set st a in dom s2 holds
s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a
proof
let a be set ; ::_thesis: ( a in dom s2 implies s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a )
assume  a in dom s2 ; ::_thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a
A26: dom ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1))) = {(IC )} by FUNCOP_1:13;
percases ( a = IC or a <> IC ) ;
supposeA27: a = IC ; ::_thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a
hence s2 . a = (IC (s2 +* v)) + ((card F) -' 1) by A6, A15, A23, A21, A22, FUNCT_4:13
.= ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1))) . a by A27, FUNCOP_1:72
.= ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a by A22, A26, A27, FUNCT_4:13 ;
::_thesis: verum
end;
supposeA28: a <> IC ; ::_thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a
then A29: not a in dom ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1))) by A26, TARSKI:def_1;
 not a in dom ((IC ) .--> m) by A23, A28, TARSKI:def_1;
then  (s2 +* v) . a = s2 . a by FUNCT_4:11;
hence  s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a by A29, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
then A30: s2 = IncIC ((s2 +* v),((card F) -' 1)) by A24, A25, FUNCT_1:2;
set s3 = s2 +* v;
A31: IC (s2 +* v) = (s2 +* v) . (IC )
.= m by A21, A22, A23, FUNCT_4:13 ;
reconsider s3 = s2 +* v as Element of product (the_Values_of S) by CARD_3:107;
reconsider k = (card F) -' 1, m = m as Element of NAT ;
A32: x = IC (Exec ((IncAddr ((G /. m),k)),s2)) by A5, A17, A20, COMPOS_1:def_21
.= (IC (Exec ((G /. m),(s2 +* v)))) + k by A30, Th7
.= (IC (Exec ((G /. m),s3))) + k ;
 IC (Exec ((G /. m),s3)) in NIC ((G /. m),m) by A31;
then  IC (Exec ((G /. m),s3)) in dom G by A18;
then  IC (Exec ((G /. m),s3)) in dom (IncAddr (G,k)) by COMPOS_1:def_21;
then  x in dom (Reloc (G,k)) by A4, A32;
hence  x in K485(NAT,(F ';' G)) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;

theorem :: AMISTD_2:8
for N being with_zero set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0 by Lm1;

theorem :: AMISTD_2:9
for N being with_zero set
for T being InsType of the InstructionsF of (Trivial-AMI N) holds JumpParts T = {0} by Lm2;


theorem :: AMISTD_2:10
for N being with_zero set
for n being Element of NAT
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for I being Program of
for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)
proof
let N be with_zero set ; ::_thesis: for n being Element of NAT
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for I being Program of
for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)
let n be Element of NAT ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for I being Program of
for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for s being State of S
for I being Program of
for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)
let s be State of S; ::_thesis: for I being Program of
for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)
let I be Program of ; ::_thesis: for P1, P2 being Instruction-Sequence of S st I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)
let P1, P2 be Instruction-Sequence of S; ::_thesis: ( I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ) implies for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m) )
assume A1: ( I c= P1 & I c= P2 ) ; ::_thesis: ( ex m being Element of NAT st
( m < n & not IC (Comput (P2,s,m)) in dom I ) or for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m) )
assume A2: for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ; ::_thesis: for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)
defpred S1[ Nat] means ( $1 <= n implies Comput (P1,s,$1) = Comput (P2,s,$1) );
A3: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A4: S1[m] ; ::_thesis: S1[m + 1]
A5: Comput (P2,s,(m + 1)) = Following (P2,(Comput (P2,s,m))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s,m)))),(Comput (P2,s,m))) ;
A6: Comput (P1,s,(m + 1)) = Following (P1,(Comput (P1,s,m))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s,m)))),(Comput (P1,s,m))) ;
assume A7: m + 1 <= n ; ::_thesis: Comput (P1,s,(m + 1)) = Comput (P2,s,(m + 1))
then  m < n by NAT_1:13;
then A8: IC (Comput (P1,s,m)) = IC (Comput (P2,s,m)) by A4;
 m < n by A7, NAT_1:13;
then A9: IC (Comput (P2,s,m)) in dom I by A2;
 dom P2 = NAT by PARTFUN1:def_2;
then A10: IC (Comput (P2,s,m)) in dom P2 ;
 dom P1 = NAT by PARTFUN1:def_2;
then  IC (Comput (P1,s,m)) in dom P1 ;
then  CurInstr (P1,(Comput (P1,s,m))) = P1 . (IC (Comput (P1,s,m))) by PARTFUN1:def_6
.= I . (IC (Comput (P1,s,m))) by A9, A8, A1, GRFUNC_1:2
.= P2 . (IC (Comput (P2,s,m))) by A9, A8, A1, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s,m))) by A10, PARTFUN1:def_6 ;
hence  Comput (P1,s,(m + 1)) = Comput (P2,s,(m + 1)) by A4, A6, A5, A7, NAT_1:13; ::_thesis: verum
end;
A11: S1[ 0 ] ;
thus  for m being Element of NAT holds S1[m] from NAT_1:sch_1(A11, A3); ::_thesis: verum
end;

theorem :: AMISTD_2:11
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
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
for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
let P be Instruction-Sequence of S; ::_thesis: for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
let s be State of S; ::_thesis: ( s = Following (P,s) implies for n being Element of NAT holds Comput (P,s,n) = s )
defpred S1[ Element of NAT ] means  Comput (P,s,$1) = s;
assume A1: s = Following (P,s) ; ::_thesis: for n being Element of NAT holds Comput (P,s,n) = s
A2: for n being Element of NAT st S1[n] holds
S1[n + 1] by A1, EXTPRO_1:3;
A3: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); ::_thesis: verum
end;