:: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz

::

:: Received April 22, 2010

:: Copyright (c) 2010-2018 Association of Mizar Users

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;

end;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;

let l1, l2 be Nat;

:: deftheorem 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 & 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) ) ) );

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 & 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

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 & l2 <= l3,S holds

l1 <= l3,S

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 & l2 <= l3,S holds

l1 <= l3,S

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;

end;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;

attr S is InsLoc-antisymmetric means :: AMI_WSTD:def 2

for l1, l2 being Element of NAT st l1 <= l2,S & l2 <= l1,S holds

l1 = l2;

for l1, l2 being Element of NAT st l1 <= l2,S & l2 <= l1,S holds

l1 = l2;

:: 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 & l2 <= l1,S holds

l1 = l2 );

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

end;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;

:: 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 sequence of NAT st

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) ) );

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 sequence of NAT st

( f is bijective & ( 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 sequence of 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

for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for f1, f2 being sequence of 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;

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

proof end;

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 sequence of 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 ) ) )

for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for f being sequence of 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 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 sequence of 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 ) ) ) ) )

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 sequence of 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]};

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)) = (IC s) + 1

proof end;

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 & InsCode i = 1 holds

NIC (i,l) = {(z + 1)}

proof end;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st

( b_{1} is weakly_standard & b_{1} is halting )

end;
cluster non empty with_non-empty_values IC-Ins-separated halting weakly_standard for AMI-Struct over N;

existence ex b

( b

proof 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 natural Number ;

ex b_{1} being Element of NAT ex f being sequence of NAT st

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & b_{1} = f . k )

for b_{1}, b_{2} being Element of NAT st ex f being sequence of NAT st

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & b_{1} = f . k ) & ex f being sequence of NAT st

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & b_{2} = f . k ) holds

b_{1} = b_{2}
by Th2;

end;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;

let k be natural Number ;

func il. (S,k) -> Element of NAT means :Def4: :: AMI_WSTD:def 4

ex f being sequence of 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 f being sequence of NAT st

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & it = f . k );

ex b

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & b

proof end;

uniqueness for b

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & b

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & b

b

:: 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 natural Number

for b_{4} being Element of NAT holds

( b_{4} = il. (S,k) iff ex f being sequence of NAT st

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & b_{4} = f . k ) );

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 natural Number

for b

( b

( f is bijective & ( for m, n being Element of NAT holds

( m <= n iff f . m <= f . n,S ) ) & b

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

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

proof end;

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)

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)

proof 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 l be Nat;

existence

ex b_{1} being Nat st il. (S,b_{1}) = l
by Th6;

uniqueness

for b_{1}, b_{2} being Nat st il. (S,b_{1}) = l & il. (S,b_{2}) = l holds

b_{1} = b_{2}
by Th5;

end;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;

let l be Nat;

existence

ex b

uniqueness

for b

b

:: 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, b_{4} being Nat holds

( b_{4} = locnum (l,S) iff il. (S,b_{4}) = l );

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, b

( b

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

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

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

proof end;

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 natural Number holds

( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 )

for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N

for k1, k2 being natural Number holds

( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 )

proof end;

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 )

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 )

proof end;

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

for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N holds T is InsLoc-antisymmetric

proof end;

registration

let N be with_zero set ;

for b_{1} being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b_{1} is weakly_standard holds

b_{1} is InsLoc-antisymmetric
by Th10;

end;
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 b

b

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;

coherence

il. (S,((locnum (f,S)) + k)) is Element of NAT ;

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

coherence

il. (S,((locnum (f,S)) + k)) is Element of NAT ;

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

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;

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

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

proof end;

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;

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 ;

coherence

f + (1,S) is Element of NAT ;

end;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;

let f be Element of NAT ;

coherence

f + (1,S) is Element of NAT ;

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

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

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)

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)

proof end;

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

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

proof end;

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))

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))

proof end;

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)))}

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)))}

proof end;

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)))}

for l being Element of NAT holds SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))}

proof 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 i be Instruction of S;

end;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;

let i be Instruction of S;

attr i is sequential means :: AMI_WSTD:def 8

for s being State of S holds (Exec (i,s)) . (IC ) = NextLoc ((IC s),S);

for s being State of S holds (Exec (i,s)) . (IC ) = NextLoc ((IC s),S);

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

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))}

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))}

proof end;

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

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

proof end;

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;

coherence

for b_{1} being Instruction of S st b_{1} is sequential holds

not b_{1} is halting
by Th22;

coherence

for b_{1} being Instruction of S st b_{1} is halting holds

not b_{1} is sequential
;

end;
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N;

coherence

for b

not b

coherence

for b

not b

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;

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

:: 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 b_{2} -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 );

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 b

( 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 b_{2} -valued finite Function st F is really-closed & il. (S,0) in dom F holds

F is para-closed by AMISTD_1:14;

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 b

F is para-closed by AMISTD_1:14;

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

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

proof end;

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;

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

:: 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 b_{2} -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 );

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 b

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

for b_{1} being NAT -defined the InstructionsF of S -valued finite Function st b_{1} is empty holds

b_{1} is lower
;

end;
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 Function;

coherence for b

b

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

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

proof end;

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;

ex b_{1} being NAT -defined the InstructionsF of S -valued finite Function st

( b_{1} is lower & b_{1} is 1 -element )

end;
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 V105() lower for Function;

existence ex b

( b

proof 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 b_{2} -valued non empty finite lower Function holds il. (T,0) in dom F

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 b

proof end;

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 b_{3} -valued finite lower Function holds

( z < card P iff il. (T,z) in dom P )

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 b

( z < card P iff il. (T,z) in dom P )

proof 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 NAT -defined the InstructionsF of S -valued non empty finite Function;

ex b_{1} 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_{1} = il. (S,(max M)) )

for b_{1}, b_{2} 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_{1} = 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_{2} = il. (S,(max M)) ) holds

b_{1} = b_{2}
;

end;
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 } & it = il. (S,(max M)) );

existence 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)) );

ex b

( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b

proof end;

uniqueness for b

( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b

( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b

b

:: 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 b_{2} -valued non empty finite Function

for b_{4} being Element of NAT holds

( b_{4} = 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_{4} = il. (S,(max M)) ) );

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 b

for b

( b

( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b

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 b_{2} -valued non empty finite Function holds LastLoc F in dom F

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 b

proof end;

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 b_{2} -valued non empty finite Function st F c= G holds

LastLoc F <= LastLoc G,T

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 b

LastLoc F <= LastLoc G,T

proof end;

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 b_{2} -valued non empty finite Function

for l being Element of NAT st l in dom F holds

l <= LastLoc F,T

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 b

for l being Element of NAT st l in dom F holds

l <= LastLoc F,T

proof end;

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 b_{2} -valued non empty finite lower Function

for G being NAT -defined the InstructionsF of b_{2} -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds

F = G

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 b

for G being NAT -defined the InstructionsF of b

F = G

proof end;

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 b_{2} -valued non empty finite lower Function holds LastLoc F = il. (T,((card F) -' 1))

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 b

proof end;

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;

for b_{1} being NAT -defined the InstructionsF of S -valued finite Function st b_{1} is really-closed & b_{1} is lower & not b_{1} is empty holds

b_{1} is para-closed
by Th26, Th23;

end;
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 Function;

coherence for b

b

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 & ( 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)) ) )

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 & ( 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 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 & ( 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 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 & ( 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);

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 & 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 A2, TARSKI:def 1; :: thesis: verum

end;
( ((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 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 & ( 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);

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 & 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 A2, TARSKI:def 1; :: thesis: verum

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;

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

:: 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 b_{2} -valued non empty finite Function holds

( F is halt-ending iff F . (LastLoc F) = halt S );

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 b

( 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 b_{2} -valued non empty finite Function 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 );

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 b

( 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 with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N;

ex b_{1} being NAT -defined the InstructionsF of S -valued non empty finite lower Function st

( b_{1} is halt-ending & b_{1} is unique-halt & b_{1} is trivial )

end;
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 V105() lower halt-ending unique-halt for Function;

existence ex b

( b

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

ex b_{1} being NAT -defined the InstructionsF of S -valued finite Function st

( b_{1} is trivial & b_{1} is really-closed & b_{1} is lower & not b_{1} is empty )

end;
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 V105() really-closed lower for Function;

existence ex b

( b

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

ex b_{1} being NAT -defined the InstructionsF of S -valued non empty finite lower Function st

( b_{1} is halt-ending & b_{1} is unique-halt & b_{1} is trivial & b_{1} is really-closed )

end;
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 V105() really-closed lower halt-ending unique-halt for Function;

existence ex b

( b

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

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;

ex b_{1} being pre-Macro of S st b_{1} is really-closed

end;
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 V105() really-closed lower halt-ending unique-halt for pre-Macro of ;

existence ex b

proof 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

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

proof 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 loc be Element of NAT ;

let k be Nat;

coherence

il. (S,((locnum (loc,S)) -' k)) is Element of NAT ;

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

coherence

il. (S,((locnum (loc,S)) -' k)) is Element of NAT ;

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

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 by NAT_D:40, Def5;

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 by NAT_D:40, Def5;

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

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

proof end;