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

::

:: Received April 14, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

registration

let N be with_zero set ;

let S be with_non-empty_values AMI-Struct over N;

let i be Element of the InstructionsF of S;

let s be State of S;

coherence

( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like )

end;
let S be with_non-empty_values AMI-Struct over N;

let i be Element of the InstructionsF of S;

let s be State of S;

coherence

( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like )

proof end;

registration

let N be with_zero set ;

existence

ex b_{1} being AMI-Struct over N st

( not b_{1} is empty & b_{1} is with_non-empty_values )

end;
existence

ex b

( not b

proof end;

definition

let N be with_zero set ;

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

let T be InsType of the InstructionsF of S;

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

let T be InsType of the InstructionsF of S;

attr T is jump-only means :: AMISTD_1:def 1

for s being State of S

for o being Object of S

for I being Instruction of S st InsCode I = T & o in Data-Locations holds

(Exec (I,s)) . o = s . o;

for s being State of S

for o being Object of S

for I being Instruction of S st InsCode I = T & o in Data-Locations holds

(Exec (I,s)) . o = s . o;

:: deftheorem defines jump-only AMISTD_1:def 1 :

for N being with_zero set

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

for T being InsType of the InstructionsF of S holds

( T is jump-only iff for s being State of S

for o being Object of S

for I being Instruction of S st InsCode I = T & o in Data-Locations holds

(Exec (I,s)) . o = s . o );

for N being with_zero set

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

for T being InsType of the InstructionsF of S holds

( T is jump-only iff for s being State of S

for o being Object of S

for I being Instruction of S st InsCode I = T & o in Data-Locations holds

(Exec (I,s)) . o = s . o );

definition

let N be with_zero set ;

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

let I be Instruction of S;

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

let I be Instruction of S;

:: deftheorem defines jump-only AMISTD_1:def 2 :

for N being with_zero set

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

for I being Instruction of S holds

( I is jump-only iff InsCode I is jump-only );

for N being with_zero set

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

for I being Instruction of S holds

( I is jump-only iff InsCode I is jump-only );

definition

let N be with_zero set ;

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

let l be Nat;

let i be Element of the InstructionsF of S;

{ (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } is Subset of NAT

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

let l be Nat;

let i be Element of the InstructionsF of S;

func NIC (i,l) -> Subset of NAT equals :: AMISTD_1:def 3

{ (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ;

coherence { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ;

{ (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } is Subset of NAT

proof end;

:: deftheorem defines NIC AMISTD_1:def 3 :

for N being with_zero set

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

for l being Nat

for i being Element of the InstructionsF of S holds NIC (i,l) = { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ;

for N being with_zero set

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

for l being Nat

for i being Element of the InstructionsF of S holds NIC (i,l) = { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ;

Lm1: now :: thesis: for N being with_zero set

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

for i being Element of the InstructionsF of S

for l being Element of NAT

for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

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

for i being Element of the InstructionsF of S

for l being Element of NAT

for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for i being Element of the InstructionsF of S

for l being Element of NAT

for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for i being Element of the InstructionsF of S

for l being Element of NAT

for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let i be Element of the InstructionsF of S; :: thesis: for l being Element of NAT

for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let l be Element of NAT ; :: thesis: for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let s be State of S; :: thesis: for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let P be Instruction-Sequence of S; :: thesis: IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

reconsider t = s +* ((IC ),l) as Element of product (the_Values_of S) by CARD_3:107;

l in NAT ;

then A1: l in dom P by PARTFUN1:def 2;

IC in dom s by MEMSTR_0:2;

then A2: IC t = l by FUNCT_7:31;

then CurInstr ((P +* (l,i)),t) = (P +* (l,i)) . l by PBOOLE:143

.= i by A1, FUNCT_7:31 ;

hence IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) by A2; :: thesis: verum

end;
for i being Element of the InstructionsF of S

for l being Element of NAT

for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for i being Element of the InstructionsF of S

for l being Element of NAT

for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let i be Element of the InstructionsF of S; :: thesis: for l being Element of NAT

for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let l be Element of NAT ; :: thesis: for s being State of S

for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let s be State of S; :: thesis: for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

let P be Instruction-Sequence of S; :: thesis: IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)

reconsider t = s +* ((IC ),l) as Element of product (the_Values_of S) by CARD_3:107;

l in NAT ;

then A1: l in dom P by PARTFUN1:def 2;

IC in dom s by MEMSTR_0:2;

then A2: IC t = l by FUNCT_7:31;

then CurInstr ((P +* (l,i)),t) = (P +* (l,i)) . l by PBOOLE:143

.= i by A1, FUNCT_7:31 ;

hence IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) by A2; :: thesis: verum

registration

let N be with_zero set ;

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

let i be Element of the InstructionsF of S;

let l be Element of NAT ;

coherence

not NIC (i,l) is empty by Lm1;

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

let i be Element of the InstructionsF of S;

let l be Element of NAT ;

coherence

not NIC (i,l) is empty by Lm1;

definition

let N be with_zero set ;

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

let i be Element of the InstructionsF of S;

meet { (NIC (i,l)) where l is Element of NAT : verum } is Subset of NAT

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

let i be Element of the InstructionsF of S;

func JUMP i -> Subset of NAT equals :: AMISTD_1:def 4

meet { (NIC (i,l)) where l is Element of NAT : verum } ;

coherence meet { (NIC (i,l)) where l is Element of NAT : verum } ;

meet { (NIC (i,l)) where l is Element of NAT : verum } is Subset of NAT

proof end;

:: deftheorem defines JUMP AMISTD_1:def 4 :

for N being with_zero set

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

for i being Element of the InstructionsF of S holds JUMP i = meet { (NIC (i,l)) where l is Element of NAT : verum } ;

for N being with_zero set

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

for i being Element of the InstructionsF of S holds JUMP i = meet { (NIC (i,l)) where l is Element of NAT : verum } ;

definition

let N be with_zero set ;

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

let l be Nat;

union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } is Subset of NAT

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

let l be Nat;

func SUCC (l,S) -> Subset of NAT equals :: AMISTD_1:def 5

union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ;

coherence union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ;

union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } is Subset of NAT

proof end;

:: deftheorem defines SUCC AMISTD_1:def 5 :

for N being with_zero set

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

for l being Nat holds SUCC (l,S) = union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ;

for N being with_zero set

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

for l being Nat holds SUCC (l,S) = union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ;

theorem Th1: :: AMISTD_1:1

for N being with_zero set

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

for i being Element of the InstructionsF of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds

JUMP i is empty

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

for i being Element of the InstructionsF of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds

JUMP i is empty

proof end;

theorem Th2: :: AMISTD_1:2

for N being with_zero set

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

for il being Element of NAT

for i being Instruction of S st i is halting holds

NIC (i,il) = {il}

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

for il being Element of NAT

for i being Instruction of S st i is halting holds

NIC (i,il) = {il}

proof end;

begin

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 Def6 defines standard AMISTD_1:def 6 :

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 standard iff for m, n being Element of NAT holds

( m <= n iff ex f being non empty FinSequence of NAT st

( f /. 1 = m & f /. (len f) = n & ( 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 holds

( S is standard iff for m, n being Element of NAT holds

( m <= n iff ex f being non empty FinSequence of NAT st

( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds

f /. (n + 1) in SUCC ((f /. n),S) ) ) ) );

Lm2: 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 ex f being non empty FinSequence of NAT st

( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds

f /. (n + 1) in SUCC ((f /. n),S) ) )

proof end;

theorem Th3: :: AMISTD_1: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 standard iff for k being Element of NAT holds

( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds

k <= j ) ) )

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

( S is standard iff for k being Element of NAT holds

( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds

k <= j ) ) )

proof end;

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

begin

definition

let N be with_zero set ;

ex b_{1} being strict AMI-Struct over N st

( the carrier of b_{1} = {0} & the ZeroF of b_{1} = 0 & the InstructionsF of b_{1} = {[0,0,0],[1,0,0]} & the Object-Kind of b_{1} = 0 .--> 0 & the ValuesF of b_{1} = N --> NAT & ex f being Function of (product (the_Values_of b_{1})),(product (the_Values_of b_{1})) st

( ( for s being Element of product (the_Values_of b_{1}) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of b_{1} = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b_{1})))) ) )

for b_{1}, b_{2} being strict AMI-Struct over N st the carrier of b_{1} = {0} & the ZeroF of b_{1} = 0 & the InstructionsF of b_{1} = {[0,0,0],[1,0,0]} & the Object-Kind of b_{1} = 0 .--> 0 & the ValuesF of b_{1} = N --> NAT & ex f being Function of (product (the_Values_of b_{1})),(product (the_Values_of b_{1})) st

( ( for s being Element of product (the_Values_of b_{1}) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of b_{1} = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b_{1})))) ) & the carrier of b_{2} = {0} & the ZeroF of b_{2} = 0 & the InstructionsF of b_{2} = {[0,0,0],[1,0,0]} & the Object-Kind of b_{2} = 0 .--> 0 & the ValuesF of b_{2} = N --> NAT & ex f being Function of (product (the_Values_of b_{2})),(product (the_Values_of b_{2})) st

( ( for s being Element of product (the_Values_of b_{2}) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of b_{2} = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b_{2})))) ) holds

b_{1} = b_{2}

end;
func STC N -> strict AMI-Struct over N means :Def7: :: AMISTD_1:def 7

( the carrier of it = {0} & the ZeroF of it = 0 & the InstructionsF of it = {[0,0,0],[1,0,0]} & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & ex f being Function of (product (the_Values_of it)),(product (the_Values_of it)) st

( ( for s being Element of product (the_Values_of it) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it)))) ) );

existence ( the carrier of it = {0} & the ZeroF of it = 0 & the InstructionsF of it = {[0,0,0],[1,0,0]} & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & ex f being Function of (product (the_Values_of it)),(product (the_Values_of it)) st

( ( for s being Element of product (the_Values_of it) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it)))) ) );

ex b

( the carrier of b

( ( for s being Element of product (the_Values_of b

proof end;

uniqueness for b

( ( for s being Element of product (the_Values_of b

( ( for s being Element of product (the_Values_of b

b

proof end;

:: deftheorem Def7 defines STC AMISTD_1:def 7 :

for N being with_zero set

for b_{2} being strict AMI-Struct over N holds

( b_{2} = STC N iff ( the carrier of b_{2} = {0} & the ZeroF of b_{2} = 0 & the InstructionsF of b_{2} = {[0,0,0],[1,0,0]} & the Object-Kind of b_{2} = 0 .--> 0 & the ValuesF of b_{2} = N --> NAT & ex f being Function of (product (the_Values_of b_{2})),(product (the_Values_of b_{2})) st

( ( for s being Element of product (the_Values_of b_{2}) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of b_{2} = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b_{2})))) ) ) );

for N being with_zero set

for b

( b

( ( for s being Element of product (the_Values_of b

registration
end;

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

(Exec (i,s)) . (IC ) = succ (IC s)

proof end;

theorem :: AMISTD_1:5

for N being with_zero set

for i being Instruction of (STC N) st InsCode i = 1 holds

not i is halting

for i being Instruction of (STC N) st InsCode i = 1 holds

not i is halting

proof end;

theorem Th6: :: AMISTD_1:6

for N being with_zero set

for i being Element of the InstructionsF of (STC N) holds

( InsCode i = 1 or InsCode i = 0 )

for i being Element of the InstructionsF of (STC N) holds

( InsCode i = 1 or InsCode i = 0 )

proof end;

registration

let N be with_zero set ;

coherence

for b_{1} being Instruction of (STC N) holds b_{1} is ins-loc-free

end;
coherence

for b

proof end;

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

Lm5: for N being with_zero set

for i being Element of the InstructionsF of (STC N) holds JUMP i is empty

proof end;

theorem Th8: :: AMISTD_1:8

for z being Nat

for N being with_zero set

for l being Element of NAT st l = z holds

SUCC (l,(STC N)) = {z,(z + 1)}

for N being with_zero set

for l being Element of NAT st l = z holds

SUCC (l,(STC N)) = {z,(z + 1)}

proof end;

registration
end;

registration
end;

registration

let N be with_zero set ;

existence

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

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

end;
existence

ex b

( b

proof end;

theorem :: AMISTD_1:9

theorem :: AMISTD_1:10

theorem :: AMISTD_1:11

definition

let N be with_zero set ;

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

let i be Instruction of S;

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

let i be Instruction of S;

attr i is sequential means :: AMISTD_1:def 8

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

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

:: deftheorem defines sequential AMISTD_1:def 8 :

for N being with_zero set

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

for i being Instruction of S holds

( i is sequential iff for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s) );

for N being with_zero set

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

for i being Instruction of S holds

( i is sequential iff for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s) );

theorem Th12: :: AMISTD_1:12

for N being with_zero set

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

for il being Element of NAT

for i being Instruction of S st i is sequential holds

NIC (i,il) = {(succ il)}

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

for il being Element of NAT

for i being Instruction of S st i is sequential holds

NIC (i,il) = {(succ il)}

proof end;

registration

let N be with_zero set ;

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

coherence

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

not b_{1} is halting

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 AMI-Struct over N;

coherence

for b

not b

proof end;

coherence for b

not b

theorem :: AMISTD_1:13

for N being with_zero set

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

for i being Instruction of T st not JUMP i is empty holds

not i is sequential

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

for i being Instruction of T st not JUMP i is empty holds

not i is sequential

proof end;

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 F be preProgram of S;

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

let F be preProgram of S;

:: deftheorem Def9 defines really-closed AMISTD_1:def 9 :

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 preProgram of S holds

( F is really-closed iff for l being Element of NAT st l in dom F holds

NIC ((F /. l),l) c= 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 preProgram of S holds

( F is really-closed iff for l being Element of NAT st l in dom F holds

NIC ((F /. l),l) c= dom F );

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

attr F is paraclosed means :: AMISTD_1:def 10

for s being 0 -started State of S

for P being Instruction-Sequence of S st F c= P holds

for k being Element of NAT holds IC (Comput (P,s,k)) in dom F;

for s being 0 -started State of S

for P being Instruction-Sequence of S st F c= P holds

for k being Element of NAT holds IC (Comput (P,s,k)) in dom F;

:: deftheorem defines paraclosed AMISTD_1: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 Function holds

( F is paraclosed iff for s being 0 -started State of S

for P being Instruction-Sequence of S st F c= P holds

for k being Element of NAT holds IC (Comput (P,s,k)) 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 paraclosed iff for s being 0 -started State of S

for P being Instruction-Sequence of S st F c= P holds

for k being Element of NAT holds IC (Comput (P,s,k)) in dom F );

definition

let N be with_zero set ;

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

let F be NAT -defined the InstructionsF of S -valued Function;

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

let F be NAT -defined the InstructionsF of S -valued Function;

attr F is parahalting means :: AMISTD_1:def 11

for s being 0 -started State of S

for P being Instruction-Sequence of S st F c= P holds

P halts_on s;

for s being 0 -started State of S

for P being Instruction-Sequence of S st F c= P holds

P halts_on s;

:: deftheorem defines parahalting AMISTD_1:def 11 :

for N being with_zero set

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

for F being NAT -defined the InstructionsF of b_{2} -valued Function holds

( F is parahalting iff for s being 0 -started State of S

for P being Instruction-Sequence of S st F c= P holds

P halts_on s );

for N being with_zero set

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

for F being NAT -defined the InstructionsF of b

( F is parahalting iff for s being 0 -started State of S

for P being Instruction-Sequence of S st F c= P holds

P halts_on s );

theorem Th14: :: AMISTD_1:14

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 preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for k being Element of NAT holds IC (Comput (F,s,k)) in dom F )

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

for F being preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for k being Element of NAT holds IC (Comput (F,s,k)) in dom F )

proof end;

Lm6: 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 preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for P being Instruction-Sequence of S st F c= P holds

for k being Element of NAT holds IC (Comput (P,s,k)) in dom F )

proof end;

theorem Th15: :: AMISTD_1:15

for N being with_zero set

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

for F being NAT -defined the InstructionsF of b_{2} -valued finite Function st F is really-closed & 0 in dom F holds

F is paraclosed

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

for F being NAT -defined the InstructionsF of b

F is paraclosed

proof end;

theorem Th16: :: AMISTD_1:16

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds 0 .--> (halt S) is really-closed

for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds 0 .--> (halt S) is really-closed

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated 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 initial & not b_{1} is empty holds

b_{1} is paraclosed

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

cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite initial really-closed -> NAT -defined the InstructionsF of S -valued finite paraclosed for set ;

coherence for b

b

proof end;

Lm7: now :: thesis: for N being with_zero set

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

( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds

l = LastLoc <%(halt S)%> ) )

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

( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds

l = LastLoc <%(halt S)%> ) )

let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds

( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds

l = LastLoc <%(halt S)%> ) )

let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; :: thesis: ( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds

l = LastLoc <%(halt S)%> ) )

set F = <%(halt S)%>;

A1: dom <%(halt S)%> = {0} by FUNCOP_1:13;

then A2: card (dom <%(halt S)%>) = 1 by CARD_1:30;

A3: LastLoc <%(halt S)%> = (card <%(halt S)%>) -' 1 by AFINSQ_1:70

.= 0 by A2, XREAL_1:232 ;

hence <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S by FUNCOP_1:72; :: thesis: for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds

l = LastLoc <%(halt S)%>

let l be Nat; :: thesis: ( <%(halt S)%> . l = halt S & l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )

assume <%(halt S)%> . l = halt S ; :: thesis: ( l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )

assume l in dom <%(halt S)%> ; :: thesis: l = LastLoc <%(halt S)%>

hence l = LastLoc <%(halt S)%> by A1, A3, TARSKI:def 1; :: thesis: verum

end;
( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds

l = LastLoc <%(halt S)%> ) )

let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; :: thesis: ( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds

l = LastLoc <%(halt S)%> ) )

set F = <%(halt S)%>;

A1: dom <%(halt S)%> = {0} by FUNCOP_1:13;

then A2: card (dom <%(halt S)%>) = 1 by CARD_1:30;

A3: LastLoc <%(halt S)%> = (card <%(halt S)%>) -' 1 by AFINSQ_1:70

.= 0 by A2, XREAL_1:232 ;

hence <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S by FUNCOP_1:72; :: thesis: for l being Nat st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds

l = LastLoc <%(halt S)%>

let l be Nat; :: thesis: ( <%(halt S)%> . l = halt S & l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )

assume <%(halt S)%> . l = halt S ; :: thesis: ( l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )

assume l in dom <%(halt S)%> ; :: thesis: l = LastLoc <%(halt S)%>

hence l = LastLoc <%(halt S)%> by A1, A3, TARSKI:def 1; :: thesis: verum

registration

let N be with_zero set ;

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

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 initial & not b_{1} is empty )

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

cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite initial countable V139() really-closed for set ;

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 standard AMI-Struct over N;

ex b_{1} being NAT -defined the InstructionsF of S -valued non empty finite initial 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 standard AMI-Struct over N;

cluster Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like finite initial halt-ending unique-halt countable V139() really-closed for set ;

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 standard AMI-Struct over N;

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

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

cluster Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty Function-like finite initial halt-ending unique-halt countable V139() really-closed for set ;

existence ex b

proof end;

theorem :: AMISTD_1:18

for N being with_zero set

for i being Element of the InstructionsF of (Trivial-AMI N) holds InsCode i = 0

for i being Element of the InstructionsF of (Trivial-AMI N) holds InsCode i = 0

proof end;

begin

:: from SCMPDS_9, 2008.03.10, A.T.

theorem :: AMISTD_1:19

for N being with_zero set

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

for i being Instruction of S

for l being Element of NAT holds JUMP i c= NIC (i,l)

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

for i being Instruction of S

for l being Element of NAT holds JUMP i c= NIC (i,l)

proof end;

theorem :: AMISTD_1:20

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

Exec (i,s) = IncIC (s,1)

for i being Instruction of (STC N)

for s being State of (STC N) st InsCode i = 1 holds

Exec (i,s) = IncIC (s,1)

proof end;

registration
end;

theorem :: AMISTD_1:21

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 preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for P being Instruction-Sequence of S st F c= P holds

for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) by Lm6;

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

for F being preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for P being Instruction-Sequence of S st F c= P holds

for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) by Lm6;

registration

let N be with_zero set ;

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

ex b_{1} being NAT -defined the InstructionsF of S -valued non empty finite non halt-free Function st b_{1} is parahalting

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

cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite non halt-free countable V139() parahalting for set ;

existence ex b

proof end;