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

::

:: Received April 14, 2000

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

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 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 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 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 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 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 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 by ORDINAL1:def 12;

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 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 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 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 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 by ORDINAL1:def 12;

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

coherence

meet { (NIC (i,l)) where l is 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;

coherence

meet { (NIC (i,l)) where l is 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 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 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 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 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 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 Nat

for i being Instruction of S st i is halting holds

NIC (i,il) = {il}

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;

:: deftheorem 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 Nat holds

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

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

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

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

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

Lm2: for k being 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 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 Nat holds

( k + 1 in SUCC (k,S) & ( for j being 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 Nat holds

( k + 1 in SUCC (k,S) & ( for j being Nat st j in SUCC (k,S) holds

k <= j ) ) )

proof end;

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

definition

let N be with_zero set ;

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

( the carrier of b_{1} = {0} & IC = 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 .--> ((In ((s . 0),NAT)) + 1)) ) & 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} & IC = 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 .--> ((In ((s . 0),NAT)) + 1)) ) & 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} & IC = 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 .--> ((In ((s . 0),NAT)) + 1)) ) & 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} & IC = 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 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it)))) ) );

existence ( the carrier of it = {0} & IC = 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 .--> ((In ((s . 0),NAT)) + 1)) ) & 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} & IC = 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 .--> ((In ((s . 0),NAT)) + 1)) ) & 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 ) = (IC s) + 1

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 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 Nat st l = z holds

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

for N being with_zero set

for l being 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 ) = (IC s) + 1;

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

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

for N being with_zero set

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

for i being Instruction of S holds

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

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 Nat

for i being Instruction of S st i is sequential holds

NIC (i,il) = {(il + 1)}

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

for il being Nat

for i being Instruction of S st i is sequential holds

NIC (i,il) = {(il + 1)}

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;

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;

attr F is really-closed means :: AMISTD_1:def 9

for l being Nat st l in dom F holds

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

for l being Nat st l in dom F holds

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

:: deftheorem 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 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 Nat st l in dom F holds

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

canceled;

::$CD

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 10

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

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 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 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 Nat holds IC (Comput (P,s,k)) in dom F )

proof end;

registration

let N be with_zero set ;

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

coherence

Stop S is really-closed

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

coherence

Stop S is really-closed

proof end;

::$CT 2

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 & b_{1} is trivial )

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 V10() non empty trivial Function-like finite initial non halt-free halt-ending unique-halt countable V150() really-closed for MacroInstruction of ;

existence ex b

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

:: 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 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 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 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 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 V150() parahalting for Function;

existence ex b

proof end;