:: Weakly Standard Ordering of Instruction Locations
:: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 22, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

begin

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let l1, l2 be Nat;
predl1 <= l2,S means :Def1: :: AMI_WSTD:def 1
 ex f being non empty FinSequence of NAT st
( f /. 1 = l1 &amp; f /. (len f) = l2 &amp; ( for n being Element of NAT st 1 <= n &amp; n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) );
end;

:: deftheorem Def1 defines <= AMI_WSTD: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 l1, l2 being Nat holds
( l1 <= l2,S iff ex f being non empty FinSequence of NAT st
( f /. 1 = l1 &amp; f /. (len f) = l2 &amp; ( for n being Element of NAT st 1 <= n &amp; n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) );

theorem :: AMI_WSTD:1
for l3 being Element of NAT
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l1, l2 being Nat st l1 <= l2,S &amp; l2 <= l3,S holds
l1 <= l3,S
proofend;

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 InsLoc-antisymmetric  means :: AMI_WSTD:def 2
 for l1, l2 being Element of NAT st l1 <= l2,S &amp; l2 <= l1,S holds
l1 = l2;
end;

:: deftheorem  defines InsLoc-antisymmetric AMI_WSTD: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 InsLoc-antisymmetric iff for l1, l2 being Element of NAT st l1 <= l2,S &amp; l2 <= l1,S holds
l1 = l2 );

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 weakly_standard  means :Def3: :: AMI_WSTD:def 3
 ex f being Function of NAT,NAT st
( f is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) );
end;

:: deftheorem Def3 defines weakly_standard AMI_WSTD:def_3_:_
 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 weakly_standard iff ex f being Function of NAT,NAT st
( f is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) ) );

theorem Th2: :: AMI_WSTD:2
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for f1, f2 being Function of NAT,NAT st f1 is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n,S ) ) &amp; f2 is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n,S ) ) holds
f1 = f2
proofend;

Lm1:  for k being Element of NAT
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds k <= k,S
proofend;

theorem Th3: :: AMI_WSTD:3
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for f being Function of NAT,NAT st f is bijective holds
( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) &amp; ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) )
proofend;

theorem Th4: :: AMI_WSTD:4
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 weakly_standard iff ex f being Function of NAT,NAT st
( f is bijective &amp; ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) &amp; ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) ) )
proofend;

set III = {[1,0,0],[0,0,0]};

begin

Lm2:  for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
IC (Exec (i,s)) = succ (IC s)
proofend;

Lm3:  for z being Nat
for N being with_zero set
for l being Element of NAT
for i being Element of the InstructionsF of (STC N) st l = z &amp; InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
proofend;

registration
let N be with_zero set ;
cluster STC N ->  weakly_standard ;
coherence
 STC N is weakly_standard
proofend;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting weakly_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 weakly_standard &amp; b1 is halting )
proofend;
end;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let k be Nat;
func il. (S,k) ->  Element of NAT  means :Def4: :: AMI_WSTD:def 4
 ex f being Function of NAT,NAT st
( f is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) &amp; it = f . k );
existence
 ex b1 being Element of NAT ex f being Function of NAT,NAT st
( f is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) &amp; b1 = f . k )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex f being Function of NAT,NAT st
( f is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) &amp; b1 = f . k ) &amp; ex f being Function of NAT,NAT st
( f is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) &amp; b2 = f . k ) holds
b1 = b2 by Th2;
end;

:: deftheorem Def4 defines il. AMI_WSTD:def_4_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for k being Nat
for b4 being Element of NAT holds
( b4 = il. (S,k) iff ex f being Function of NAT,NAT st
( f is bijective &amp; ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) &amp; b4 = f . k ) );

theorem Th5: :: AMI_WSTD:5
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for k1, k2 being Nat st il. (T,k1) = il. (T,k2) holds
k1 = k2
proofend;

theorem Th6: :: AMI_WSTD:6
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l being Nat ex k being Nat st l = il. (T,k)
proofend;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let l be Nat;
func locnum (l,S) ->  Nat means :Def5: :: AMI_WSTD:def 5
 il. (S,it) = l;
existence
 ex b1 being Nat st il. (S,b1) = l by Th6;
uniqueness
 for b1, b2 being Nat st il. (S,b1) = l &amp; il. (S,b2) = l holds
b1 = b2 by Th5;
end;

:: deftheorem Def5 defines locnum AMI_WSTD:def_5_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l, b4 being Nat holds
( b4 = locnum (l,S) iff il. (S,b4) = l );

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let l be Nat;
:: original:locnum
redefine func locnum (l,S) ->  Element of NAT ;
coherence
 locnum (l,S) is Element of NAT by ORDINAL1:def_12;
end;

theorem Th7: :: AMI_WSTD:7
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l1, l2 being Element of NAT st locnum (l1,T) = locnum (l2,T) holds
l1 = l2
proofend;

theorem Th8: :: AMI_WSTD:8
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for k1, k2 being Nat holds
( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 )
proofend;

theorem Th9: :: AMI_WSTD:9
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l1, l2 being Element of NAT holds
( locnum (l1,T) <= locnum (l2,T) iff l1 <= l2,T )
proofend;

theorem Th10: :: AMI_WSTD:10
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N holds T is InsLoc-antisymmetric
proofend;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated weakly_standard  ->  non empty with_non-empty_values IC-Ins-separated InsLoc-antisymmetric for AMI-Struct over N;
coherence
 for b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b1 is weakly_standard holds
b1 is InsLoc-antisymmetric by Th10;
end;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let f be Element of NAT ;
let k be Nat;
funcf + (k,S) ->  Element of NAT  equals :: AMI_WSTD:def 6
 il. (S,((locnum (f,S)) + k));
coherence
 il. (S,((locnum (f,S)) + k)) is Element of NAT ;
end;

:: deftheorem  defines + AMI_WSTD:def_6_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f being Element of NAT
for k being Nat holds f + (k,S) = il. (S,((locnum (f,S)) + k));

theorem :: AMI_WSTD:11
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f being Element of NAT holds f + (0,T) = f by Def5;

theorem :: AMI_WSTD:12
for z being Nat
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f, g being Element of NAT st f + (z,T) = g + (z,T) holds
f = g
proofend;

theorem :: AMI_WSTD:13
for z being Nat
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f being Element of NAT holds (locnum (f,T)) + z = locnum ((f + (z,T)),T) by Def5;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let f be Element of NAT ;
func NextLoc (f,S) ->  Element of NAT  equals :: AMI_WSTD:def 7
f + (1,S);
coherence
 f + (1,S) is Element of NAT ;
end;

:: deftheorem  defines NextLoc AMI_WSTD:def_7_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f being Element of NAT holds NextLoc (f,S) = f + (1,S);

theorem :: AMI_WSTD:14
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f being Element of NAT holds NextLoc (f,T) = il. (T,((locnum (f,T)) + 1)) ;

theorem Th15: :: AMI_WSTD:15
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f being Element of NAT holds f <> NextLoc (f,T)
proofend;

theorem :: AMI_WSTD:16
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f, g being Element of NAT st NextLoc (f,T) = NextLoc (g,T) holds
f = g
proofend;

theorem Th17: :: AMI_WSTD:17
for z being Nat
for N being with_zero set holds il. ((STC N),z) = z
proofend;

theorem :: AMI_WSTD:18
for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
IC (Exec (i,s)) = NextLoc ((IC s),(STC N))
proofend;

theorem :: AMI_WSTD:19
for N being with_zero set
for l being Element of NAT
for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(NextLoc (l,(STC N)))}
proofend;

theorem :: AMI_WSTD:20
for N being with_zero set
for l being Element of NAT holds SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))}
proofend;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let i be Instruction of S;
attri is sequential  means :: AMI_WSTD:def 8
 for s being State of S holds (Exec (i,s)) . (IC ) = NextLoc ((IC s),S);
end;

:: deftheorem  defines sequential AMI_WSTD:def_8_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for i being Instruction of S holds
( i is sequential iff for s being State of S holds (Exec (i,s)) . (IC ) = NextLoc ((IC s),S) );

theorem Th21: :: AMI_WSTD:21
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(NextLoc (il,S))}
proofend;

theorem Th22: :: AMI_WSTD:22
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for i being Instruction of S st i is sequential holds
not i is halting
proofend;

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

begin

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let F be NAT -defined the InstructionsF of S -valued Function;
attrF is para-closed  means :: AMI_WSTD:def 9
 for s being State of S st IC s = il. (S,0) holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F;
end;

:: deftheorem  defines para-closed AMI_WSTD:def_9_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued Function holds
( F is para-closed iff for s being State of S st IC s = il. (S,0) holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F );

theorem Th23: :: AMI_WSTD:23
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued finite Function st F is really-closed &amp; il. (S,0) in dom F holds
F is para-closed
proofend;

theorem Th24: :: AMI_WSTD:24
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds (il. (S,0)) .--> (halt S) is really-closed
proofend;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let F be NAT -defined the InstructionsF of S -valued finite Function;
attrF is lower  means :Def10: :: AMI_WSTD:def 10
 for l being Element of NAT st l in dom F holds
for m being Element of NAT st m <= l,S holds
m in dom F;
end;

:: deftheorem Def10 defines lower AMI_WSTD:def_10_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued finite Function holds
( F is lower iff for l being Element of NAT st l in dom F holds
for m being Element of NAT st m <= l,S holds
m in dom F );

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
cluster Relation-like NAT -defined the InstructionsF of S -valued empty Function-like finite  ->  NAT -defined the InstructionsF of S -valued finite lower for set ;
coherence
 for b1 being NAT -defined the InstructionsF of S -valued finite Function st b1 is empty holds
b1 is lower
proofend;
end;

theorem Th25: :: AMI_WSTD:25
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower
proofend;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
cluster Relation-like NAT -defined the InstructionsF of S -valued Function-like finite 1 -element countable V94() lower for set ;
existence
 ex b1 being NAT -defined the InstructionsF of S -valued finite Function st
( b1 is lower &amp; b1 is 1 -element )
proofend;
end;

theorem Th26: :: AMI_WSTD:26
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued non empty finite lower Function holds il. (T,0) in dom F
proofend;

theorem Th27: :: AMI_WSTD:27
for z being Nat
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for P being NAT -defined the InstructionsF of b3 -valued finite lower Function holds
( z < card P iff il. (T,z) in dom P )
proofend;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let F be NAT -defined the InstructionsF of S -valued non empty finite Function;
func LastLoc F ->  Element of NAT  means :Def11: :: AMI_WSTD:def 11
 ex M being non empty finite natural-membered set st
( M =  {  (locnum (l,S)) where l is Element of NAT : l in dom F  }  &amp; it = il. (S,(max M)) );
existence
 ex b1 being Element of NAT ex M being non empty finite natural-membered set st
( M =  {  (locnum (l,S)) where l is Element of NAT : l in dom F  }  &amp; b1 = il. (S,(max M)) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex M being non empty finite natural-membered set st
( M =  {  (locnum (l,S)) where l is Element of NAT : l in dom F  }  &amp; b1 = il. (S,(max M)) ) &amp; ex M being non empty finite natural-membered set st
( M =  {  (locnum (l,S)) where l is Element of NAT : l in dom F  }  &amp; b2 = il. (S,(max M)) ) holds
b1 = b2 ;
end;

:: deftheorem Def11 defines LastLoc AMI_WSTD:def_11_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function
for b4 being Element of NAT holds
( b4 = LastLoc F iff ex M being non empty finite natural-membered set st
( M =  {  (locnum (l,S)) where l is Element of NAT : l in dom F  }  &amp; b4 = il. (S,(max M)) ) );

theorem Th28: :: AMI_WSTD:28
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function holds LastLoc F in dom F
proofend;

theorem :: AMI_WSTD:29
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F, G being NAT -defined the InstructionsF of b2 -valued non empty finite Function st F c= G holds
LastLoc F <= LastLoc G,T
proofend;

theorem Th30: :: AMI_WSTD:30
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function
for l being Element of NAT st l in dom F holds
l <= LastLoc F,T
proofend;

theorem :: AMI_WSTD:31
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued non empty finite lower Function
for G being NAT -defined the InstructionsF of b2 -valued non empty finite Function st F c= G &amp; LastLoc F = LastLoc G holds
F = G
proofend;

theorem Th32: :: AMI_WSTD:32
for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued non empty finite lower Function holds LastLoc F = il. (T,((card F) -' 1))
proofend;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite really-closed lower  ->  NAT -defined the InstructionsF of S -valued finite para-closed for set ;
coherence
 for b1 being NAT -defined the InstructionsF of S -valued finite Function st b1 is really-closed &amp; b1 is lower &amp; not b1 is empty holds
b1 is para-closed
proofend;
end;

Lm4: now__::_thesis:_for_N_being_with_zero_set_
for_S_being_non_empty_with_non-empty_values_IC-Ins-separated_halting_weakly_standard_AMI-Struct_over_N_holds_
(_((il._(S,0))_.-->_(halt_S))_._(LastLoc_((il._(S,0))_.-->_(halt_S)))_=_halt_S_&amp;_(_for_l_being_Element_of_NAT_st_((il._(S,0))_.-->_(halt_S))_._l_=_halt_S_&amp;_l_in_dom_((il._(S,0))_.-->_(halt_S))_holds_
l_=_LastLoc_((il._(S,0))_.-->_(halt_S))_)_)
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds
( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S &amp; ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S &amp; l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S)) ) )
let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N; ::_thesis: ( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S &amp; ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S &amp; l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S)) ) )
set F = (il. (S,0)) .--> (halt S);
 dom ((il. (S,0)) .--> (halt S)) = {(il. (S,0))} by FUNCOP_1:13;
then A1: card (dom ((il. (S,0)) .--> (halt S))) = 1 by CARD_1:30;
 (il. (S,0)) .--> (halt S) is NAT -defined the InstructionsF of S -valued finite lower Function by Th25;
then A2: LastLoc ((il. (S,0)) .--> (halt S)) = il. (S,((card ((il. (S,0)) .--> (halt S))) -' 1)) by Th32
.= il. (S,((card (dom ((il. (S,0)) .--> (halt S)))) -' 1)) by CARD_1:62
.= il. (S,0) by A1, XREAL_1:232 ;
hence  ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S by FUNCOP_1:72; ::_thesis: for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S &amp; l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S))
let l be Element of NAT ; ::_thesis: ( ((il. (S,0)) .--> (halt S)) . l = halt S &amp; l in dom ((il. (S,0)) .--> (halt S)) implies l = LastLoc ((il. (S,0)) .--> (halt S)) )
assume  ((il. (S,0)) .--> (halt S)) . l = halt S ; ::_thesis: ( l in dom ((il. (S,0)) .--> (halt S)) implies l = LastLoc ((il. (S,0)) .--> (halt S)) )
assume  l in dom ((il. (S,0)) .--> (halt S)) ; ::_thesis: l = LastLoc ((il. (S,0)) .--> (halt S))
hence  l = LastLoc ((il. (S,0)) .--> (halt S)) by A2, TARSKI:def_1; ::_thesis: verum
end;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N;
let F be NAT -defined the InstructionsF of S -valued non empty finite Function;
attrF is halt-ending  means :Def12: :: AMI_WSTD:def 12
F . (LastLoc F) = halt S;
attrF is unique-halt  means :Def13: :: AMI_WSTD:def 13
 for f being Element of NAT st F . f = halt S &amp; f in dom F holds
f = LastLoc F;
end;

:: deftheorem Def12 defines halt-ending AMI_WSTD:def_12_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function holds
( F is halt-ending iff F . (LastLoc F) = halt S );

:: deftheorem Def13 defines unique-halt AMI_WSTD:def_13_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued non empty finite Function holds
( F is unique-halt iff for f being Element of NAT st F . f = halt S &amp; f in dom F holds
f = LastLoc F );

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N;
cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite countable V94() lower halt-ending unique-halt for set ;
existence
 ex b1 being NAT -defined the InstructionsF of S -valued non empty finite lower Function st
( b1 is halt-ending &amp; b1 is unique-halt &amp; b1 is trivial )
proofend;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N;
cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite countable V94() really-closed lower for set ;
existence
 ex b1 being NAT -defined the InstructionsF of S -valued finite Function st
( b1 is trivial &amp; b1 is really-closed &amp; b1 is lower &amp; not b1 is empty )
proofend;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N;
cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite countable V94() really-closed lower halt-ending unique-halt for set ;
existence
 ex b1 being NAT -defined the InstructionsF of S -valued non empty finite lower Function st
( b1 is halt-ending &amp; b1 is unique-halt &amp; b1 is trivial &amp; b1 is really-closed )
proofend;
end;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N;
mode pre-Macro of S is NAT -defined the InstructionsF of S -valued non empty finite lower halt-ending unique-halt Function;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N;
cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite countable V94() really-closed lower halt-ending unique-halt for set ;
existence
 ex b1 being pre-Macro of S st b1 is really-closed
proofend;
end;

theorem :: AMI_WSTD:33
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l1, l2 being Element of NAT st SUCC (l1,S) = NAT holds
l1 <= l2,S
proofend;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;
let loc be Element of NAT ;
let k be Nat;
funcloc -' (k,S) ->  Element of NAT  equals :: AMI_WSTD:def 14
 il. (S,((locnum (loc,S)) -' k));
coherence
 il. (S,((locnum (loc,S)) -' k)) is Element of NAT ;
end;

:: deftheorem  defines -' AMI_WSTD:def_14_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for loc being Element of NAT
for k being Nat holds loc -' (k,S) = il. (S,((locnum (loc,S)) -' k));

theorem :: AMI_WSTD:34
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l being Element of NAT holds l -' (0,S) = l
proofend;

theorem :: AMI_WSTD:35
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l being Element of NAT holds (l + (k,S)) -' (k,S) = l
proofend;