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

begin

begin

definition

canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let l1, l2 be Nat;
pred l1 <= l2,S means :Def8: :: AMI_WSTD:def 8
ex f being non empty FinSequence of NAT st
( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n),S ) );

end;

:: deftheorem AMI_WSTD:def 1 :
canceled;

:: deftheorem AMI_WSTD:def 2 :
canceled;

:: deftheorem AMI_WSTD:def 3 :
canceled;

:: deftheorem AMI_WSTD:def 4 :
canceled;

:: deftheorem AMI_WSTD:def 5 :
canceled;

:: deftheorem AMI_WSTD:def 6 :
canceled;

:: deftheorem AMI_WSTD:def 7 :
canceled;

:: deftheorem Def8 defines <= AMI_WSTD:def 8 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for l1, l2 being Nat holds
( l1 <= l2,S iff ex f being non empty FinSequence of NAT st
( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n),S ) ) );

theorem :: AMI_WSTD:1

canceled;

theorem :: AMI_WSTD:2

canceled;

theorem :: AMI_WSTD:3

canceled;

theorem :: AMI_WSTD:4

canceled;

theorem :: AMI_WSTD:5

canceled;

theorem :: AMI_WSTD:6

canceled;

theorem :: AMI_WSTD:7

canceled;

theorem :: AMI_WSTD:8

canceled;

theorem :: AMI_WSTD:9

canceled;

theorem :: AMI_WSTD:10

canceled;

theorem :: AMI_WSTD:11

canceled;

theorem :: AMI_WSTD:12

canceled;

theorem :: AMI_WSTD:13

canceled;

theorem :: AMI_WSTD:14

canceled;

theorem :: AMI_WSTD:15

canceled;

theorem :: AMI_WSTD:16

for l3 being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds
l1 <= l3,S

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
attr S is InsLoc-antisymmetric means :: AMI_WSTD:def 9
for l1, l2 being Element of NAT st l1 <= l2,S & l2 <= l1,S holds
l1 = l2;

end;

:: deftheorem defines InsLoc-antisymmetric AMI_WSTD:def 9 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds
( S is InsLoc-antisymmetric iff for l1, l2 being Element of NAT st l1 <= l2,S & l2 <= l1,S holds
l1 = l2 );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
attr S is weakly_standard means :Def10: :: AMI_WSTD:def 10
ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) );

end;

:: deftheorem Def10 defines weakly_standard AMI_WSTD:def 10 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds
( S is weakly_standard iff ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) ) );

theorem Th17: :: AMI_WSTD:17

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for f1, f2 being Function of NAT ,NAT st f1 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n,S ) ) & f2 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n,S ) ) holds
f1 = f2

proof end;

LemRefle: for k being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds k <= k,S

proof end;

theorem Th18: :: AMI_WSTD:18

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of 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 & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) )

proof end;

theorem Th19: :: AMI_WSTD:19

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds
( S is weakly_standard iff ex f being Function of NAT ,NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) ) ) )

proof end;

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

begin

Lm4: for N being non empty with_non-empty_elements set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec i,s) . (IC (STC N)) = succ (IC s)

proof end;

Lm5: for z being natural number
for N being non empty with_non-empty_elements set
for l being Element of NAT
for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC i,l = {(z + 1)}

proof end;

theorem :: AMI_WSTD:20

canceled;

theorem :: AMI_WSTD:21

canceled;

theorem :: AMI_WSTD:22

canceled;

theorem :: AMI_WSTD:23

canceled;

theorem :: AMI_WSTD:24

canceled;

registration

let N be non empty with_non-empty_elements set ;
cluster STC N -> weakly_standard ;
coherence
STC N is weakly_standard

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed weakly_standard AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of N st
( b₁ is weakly_standard & b₁ is halting & b₁ is realistic & b₁ is steady-programmed & b₁ is standard-ins )

proof end;

end;

definition

canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
let k be natural number ;
func il. S,k -> Element of NAT means :Def12: :: AMI_WSTD:def 12
ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & it = f . k );
existence
ex b₁ being Element of NAT ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b₁ = f . k )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b₁ = f . k ) & ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b₂ = f . k ) holds
b₁ = b₂ by Th17;

end;

:: deftheorem AMI_WSTD:def 11 :
canceled;

:: deftheorem Def12 defines il. AMI_WSTD:def 12 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for k being natural number
for b₄ being Element of NAT holds
( b₄ = il. S,k iff ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b₄ = f . k ) );

theorem Th25: :: AMI_WSTD:25

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for k1, k2 being natural number st il. T,k1 = il. T,k2 holds
k1 = k2

proof end;

theorem Th26: :: AMI_WSTD:26

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for l being Nat ex k being natural number st l = il. T,k

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
let l be Nat;
func locnum l,S -> natural number means :Def13: :: AMI_WSTD:def 13
il. S,it = l;
existence
ex b₁ being natural number st il. S,b₁ = l by Th26;
uniqueness
for b₁, b₂ being natural number st il. S,b₁ = l & il. S,b₂ = l holds
b₁ = b₂ by Th25;

end;

:: deftheorem Def13 defines locnum AMI_WSTD:def 13 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for l being Nat
for b₄ being natural number holds
( b₄ = locnum l,S iff il. S,b₄ = l );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of 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 13;

end;

theorem Th27: :: AMI_WSTD:27

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for l1, l2 being Element of NAT st locnum l1,T = locnum l2,T holds
l1 = l2

proof end;

theorem Th28: :: AMI_WSTD:28

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for k1, k2 being natural number holds
( il. T,k1 <= il. T,k2,T iff k1 <= k2 )

proof end;

theorem Th29: :: AMI_WSTD:29

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for l1, l2 being Element of NAT holds
( locnum l1,T <= locnum l2,T iff l1 <= l2,T )

proof end;

theorem Th30: :: AMI_WSTD:30

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N holds T is InsLoc-antisymmetric

proof end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite weakly_standard -> non empty stored-program IC-Ins-separated definite InsLoc-antisymmetric AMI-Struct of N;
coherence
for b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of N st b₁ is weakly_standard holds
b₁ is InsLoc-antisymmetric by Th30;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
let f be Element of NAT ;
let k be natural number ;
func f + k,S -> Element of NAT equals :: AMI_WSTD:def 14
il. S,((locnum f,S) + k);
coherence
il. S,((locnum f,S) + k) is Element of NAT ;

end;

:: deftheorem defines + AMI_WSTD:def 14 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f being Element of NAT
for k being natural number holds f + k,S = il. S,((locnum f,S) + k);

theorem :: AMI_WSTD:31

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f being Element of NAT holds f + 0 ,T = f by Def13;

theorem :: AMI_WSTD:32

for z being natural number
for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f, g being Element of NAT st f + z,T = g + z,T holds
f = g

proof end;

theorem :: AMI_WSTD:33

for z being natural number
for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f being Element of NAT holds (locnum f,T) + z = locnum (f + z,T),T by Def13;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
let f be Element of NAT ;
func NextLoc f,S -> Element of NAT equals :: AMI_WSTD:def 15
f + 1,S;
coherence
f + 1,S is Element of NAT ;

end;

:: deftheorem defines NextLoc AMI_WSTD:def 15 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f being Element of NAT holds NextLoc f,S = f + 1,S;

theorem :: AMI_WSTD:34

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f being Element of NAT holds NextLoc f,T = il. T,((locnum f,T) + 1) ;

theorem Th35: :: AMI_WSTD:35

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f being Element of NAT holds f <> NextLoc f,T

proof end;

theorem :: AMI_WSTD:36

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f, g being Element of NAT st NextLoc f,T = NextLoc g,T holds
f = g

proof end;

theorem Th37: :: AMI_WSTD:37

for z being natural number
for N being non empty with_non-empty_elements set holds il. (STC N),z = z

proof end;

theorem :: AMI_WSTD:38

for N being non empty with_non-empty_elements set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec i,s) . (IC (STC N)) = NextLoc (IC s),(STC N)

proof end;

theorem :: AMI_WSTD:39

for N being non empty with_non-empty_elements set
for l being Element of NAT
for i being Element of the Instructions of (STC N) st InsCode i = 1 holds
NIC i,l = {(NextLoc l,(STC N))}

proof end;

theorem :: AMI_WSTD:40

for N being non empty with_non-empty_elements set
for l being Element of NAT holds SUCC l,(STC N) = {l,(NextLoc l,(STC N))}

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
let i be Instruction of S;
attr i is sequential means :: AMI_WSTD:def 16
for s being State of S holds (Exec i,s) . (IC S) = NextLoc (IC s),S;

end;

:: deftheorem defines sequential AMI_WSTD:def 16 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for i being Instruction of S holds
( i is sequential iff for s being State of S holds (Exec i,s) . (IC S) = NextLoc (IC s),S );

theorem Th41: :: AMI_WSTD:41

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic steady-programmed weakly_standard AMI-Struct of N
for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC i,il = {(NextLoc il,S)}

proof end;

theorem Th42: :: AMI_WSTD:42

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic steady-programmed weakly_standard AMI-Struct of N
for i being Instruction of S st i is sequential holds
not i is halting

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic steady-programmed weakly_standard AMI-Struct of N;
cluster sequential -> non halting Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is sequential holds
not b₁ is halting by Th42;
cluster halting -> non sequential Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is halting holds
not b₁ is sequential ;

end;

theorem :: AMI_WSTD:43

canceled;

begin

definition

canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
let F be FinPartState of S;
attr F is para-closed means :: AMI_WSTD:def 19
for s being State of S st F c= s & IC s = il. S,0 holds
for k being Element of NAT holds IC (Comput (ProgramPart s),s,k) in dom F;

end;

:: deftheorem AMI_WSTD:def 17 :
canceled;

:: deftheorem AMI_WSTD:def 18 :
canceled;

:: deftheorem defines para-closed AMI_WSTD:def 19 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being FinPartState of S holds
( F is para-closed iff for s being State of S st F c= s & IC s = il. S,0 holds
for k being Element of NAT holds IC (Comput (ProgramPart s),s,k) in dom F );

theorem Th44: :: AMI_WSTD:44

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed weakly_standard AMI-Struct of N
for F being NAT -defined the Instructions of b₂ -valued FinPartState of st F is really-closed & il. S,0 in dom F holds
F is para-closed

proof end;

theorem :: AMI_WSTD:45

canceled;

theorem Th46: :: AMI_WSTD:46

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed weakly_standard AMI-Struct of N holds (il. S,0 ) .--> (halt S) is closed

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let F be FinPartState of S;
attr F is lower means :Def20: :: AMI_WSTD:def 20
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 Def20 defines lower AMI_WSTD:def 20 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for F being FinPartState of S 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 );

theorem Th47: :: AMI_WSTD:47

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for F being empty FinPartState of S holds F is lower

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
cluster Relation-like the U1 of S -defined empty Function-like the Object-Kind of S -compatible finite -> lower set ;
coherence
for b₁ being FinPartState of S st b₁ is empty holds
b₁ is lower by Th47;

end;

theorem Th48: :: AMI_WSTD:48

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for i being Element of the Instructions of T holds (il. T,0 ) .--> i is lower

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
cluster Relation-like NAT -defined the U1 of S -defined the Instructions of S -valued non empty trivial Function-like the Object-Kind of S -compatible finite countable lower set ;
existence
ex b₁ being FinPartState of S st
( b₁ is lower & not b₁ is empty & b₁ is trivial & b₁ is NAT -defined & b₁ is the Instructions of S -valued )

proof end;

end;

theorem Th49: :: AMI_WSTD:49

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being NAT -defined non empty lower FinPartState of holds il. T,0 in dom F

proof end;

theorem Th50: :: AMI_WSTD:50

for z being natural number
for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for P being NAT -defined lower FinPartState of holds
( z < card P iff il. T,z in dom P )

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
let F be NAT -defined non empty FinPartState of ;
func LastLoc F -> Element of NAT means :Def21: :: AMI_WSTD:def 21
ex M being non empty finite natural-membered set st
( M = { (locnum l,S) where l is Element of NAT : l in dom F } & it = il. S,(max M) );
existence
ex b₁ 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 } & b₁ = il. S,(max M) )

proof end;

uniqueness
for b₁, b₂ 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 } & b₁ = il. S,(max M) ) & ex M being non empty finite natural-membered set st
( M = { (locnum l,S) where l is Element of NAT : l in dom F } & b₂ = il. S,(max M) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def21 defines LastLoc AMI_WSTD:def 21 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of
for b₄ being Element of NAT holds
( b₄ = 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 } & b₄ = il. S,(max M) ) );

theorem Th51: :: AMI_WSTD:51

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of holds LastLoc F in dom F

proof end;

theorem :: AMI_WSTD:52

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F, G being NAT -defined non empty FinPartState of st F c= G holds
LastLoc F <= LastLoc G,T

proof end;

theorem Th53: :: AMI_WSTD:53

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of
for l being Element of NAT st l in dom F holds
l <= LastLoc F,T

proof end;

theorem :: AMI_WSTD:54

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being NAT -defined non empty lower FinPartState of
for G being NAT -defined non empty FinPartState of st F c= G & LastLoc F = LastLoc G holds
F = G

proof end;

theorem Th55: :: AMI_WSTD:55

for N being non empty with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being NAT -defined non empty lower FinPartState of holds LastLoc F = il. T,((card F) -' 1)

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite steady-programmed weakly_standard AMI-Struct of N;
cluster Relation-like NAT -defined the U1 of S -defined the Instructions of S -valued non empty Function-like the Object-Kind of S -compatible finite really-closed lower -> NAT -defined the Instructions of S -valued para-closed set ;
coherence
for b₁ being NAT -defined the Instructions of S -valued FinPartState of st b₁ is really-closed & b₁ is lower & not b₁ is empty holds
b₁ is para-closed

proof end;

end;

Lm7: now

let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting weakly_standard AMI-Struct of N holds
( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S)) ) )
let S be non empty stored-program IC-Ins-separated definite halting weakly_standard AMI-Struct of N; :: thesis: ( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S)) ) )
set F = (il. S,0 ) .--> (halt S);
A1: dom ((il. S,0 ) .--> (halt S)) = {(il. S,0 )} by FUNCOP_1:19;
then A2: card (dom ((il. S,0 ) .--> (halt S))) = 1 by CARD_1:50;
(il. S,0 ) .--> (halt S) is lower FinPartState of S by Th48;
then A3: LastLoc ((il. S,0 ) .--> (halt S)) = il. S,((card ((il. S,0 ) .--> (halt S))) -' 1) by Th55
.= il. S,((card (dom ((il. S,0 ) .--> (halt S)))) -' 1) by CARD_1:104
.= il. S,0 by A2, XREAL_1:234 ;
hence ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S by FUNCOP_1:87; :: thesis: for l being Element of NAT st ((il. S,0 ) .--> (halt S)) . l = halt S & 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 & 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 A1, A3, TARSKI:def 1; :: thesis: verum

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting weakly_standard AMI-Struct of N;
let F be NAT -defined non empty FinPartState of ;
attr F is halt-ending means :Def22: :: AMI_WSTD:def 22
F . (LastLoc F) = halt S;
attr F is unique-halt means :Def23: :: AMI_WSTD:def 23
for f being Element of NAT st F . f = halt S & f in dom F holds
f = LastLoc F;

end;

:: deftheorem Def22 defines halt-ending AMI_WSTD:def 22 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting weakly_standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of holds
( F is halt-ending iff F . (LastLoc F) = halt S );

:: deftheorem Def23 defines unique-halt AMI_WSTD:def 23 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting weakly_standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of holds
( F is unique-halt iff for f being Element of NAT st F . f = halt S & f in dom F holds
f = LastLoc F );

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting weakly_standard AMI-Struct of N;
cluster Relation-like NAT -defined the U1 of S -defined the Instructions of S -valued non empty trivial Function-like the Object-Kind of S -compatible finite countable lower halt-ending unique-halt set ;
existence
ex b₁ being NAT -defined the Instructions of S -valued non empty lower FinPartState of st
( b₁ is halt-ending & b₁ is unique-halt & b₁ is trivial )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed weakly_standard AMI-Struct of N;
cluster Relation-like NAT -defined the U1 of S -defined the Instructions of S -valued non empty trivial Function-like the Object-Kind of S -compatible finite countable closed lower set ;
existence
ex b₁ being NAT -defined the Instructions of S -valued FinPartState of st
( b₁ is trivial & b₁ is closed & b₁ is lower & not b₁ is empty )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed weakly_standard AMI-Struct of N;
cluster Relation-like NAT -defined the U1 of S -defined the Instructions of S -valued non empty trivial Function-like the Object-Kind of S -compatible finite countable closed lower halt-ending unique-halt set ;
existence
ex b₁ being NAT -defined the Instructions of S -valued non empty lower FinPartState of st
( b₁ is halt-ending & b₁ is unique-halt & b₁ is trivial & b₁ is closed )

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting weakly_standard AMI-Struct of N;
mode pre-Macro of S is NAT -defined the Instructions of S -valued non empty lower halt-ending unique-halt FinPartState of ;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed weakly_standard AMI-Struct of N;
cluster Relation-like NAT -defined the U1 of S -defined the Instructions of S -valued non empty Function-like the Object-Kind of S -compatible finite countable closed lower halt-ending unique-halt set ;
existence
ex b₁ being pre-Macro of S st b₁ is closed

proof end;

end;

theorem :: AMI_WSTD:56

canceled;

theorem :: AMI_WSTD:57

canceled;

theorem :: AMI_WSTD:58

canceled;

theorem :: AMI_WSTD:59

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for l1, l2 being Element of NAT st SUCC l1,S = NAT holds
l1 <= l2,S

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N;
let loc be Element of NAT ;
let k be natural number ;
func loc -' k,S -> Element of NAT equals :: AMI_WSTD:def 24
il. S,((locnum loc,S) -' k);
coherence
il. S,((locnum loc,S) -' k) is Element of NAT ;

end;

:: deftheorem defines -' AMI_WSTD:def 24 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for loc being Element of NAT
for k being natural number holds loc -' k,S = il. S,((locnum loc,S) -' k);

theorem :: AMI_WSTD:60

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for l being Element of NAT holds l -' 0 ,S = l

proof end;

theorem :: AMI_WSTD:61

for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for l being Element of NAT holds (l + k,S) -' k,S = l

proof end;