:: Standard Ordering of Instruction Locations
:: 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;
cluster ( the Execution of S . i) . s -> Relation-like Function-like ;
coherence
( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like )
proof end;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values for AMI-Struct over N;
existence
ex b1 being AMI-Struct over N st
( not b1 is empty & b1 is with_non-empty_values )
proof end;
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;
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;
end;

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

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;
attr I is jump-only means :: AMISTD_1:def 2
InsCode I is jump-only ;
end;

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

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;
func NIC (i,l) -> Subset of NAT equals :: AMISTD_1:def 3
{ (IC (Exec (i,ss))) where ss is Element of product () : IC ss = l } ;
coherence
{ (IC (Exec (i,ss))) where ss is Element of product () : IC ss = l } is Subset of NAT
proof end;
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 () : 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 +* ((),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 +* ((),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 +* ((),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 +* ((),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 +* ((),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 +* ((),l)))) in NIC (i,l)
let P be Instruction-Sequence of S; :: thesis: IC (Following ((P +* (l,i)),(s +* ((),l)))) in NIC (i,l)
reconsider t = s +* ((),l) as Element of product () 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 ;
hence IC (Following ((P +* (l,i)),(s +* ((),l)))) in NIC (i,l) by A2; :: thesis: verum
end;

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;
cluster NIC (i,l) -> non empty ;
coherence
not NIC (i,l) is empty
by Lm1;
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 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 Nat : verum } ;
coherence
meet { (NIC (i,l)) where l is Nat : verum } is Subset of NAT
proof end;
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 } ;

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;
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 } is Subset of NAT
proof end;
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 } ;

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
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}
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;
attr S is standard means :: AMISTD_1:def 6
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) ) ) );
end;

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

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

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

definition
let N be with_zero set ;
func STC N -> strict AMI-Struct over N means :Def7: :: AMISTD_1:def 7
( the carrier of it = & 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 ()),(product ()) st
( ( for s being Element of product () holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ()))) ) );
existence
ex b1 being strict AMI-Struct over N st
( the carrier of b1 = & IC = 0 & the InstructionsF of b1 = {[0,0,0],[1,0,0]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & ex f being Function of (product ()),(product ()) st
( ( for s being Element of product () holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ()))) ) )
proof end;
uniqueness
for b1, b2 being strict AMI-Struct over N st the carrier of b1 = & IC = 0 & the InstructionsF of b1 = {[0,0,0],[1,0,0]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & ex f being Function of (product ()),(product ()) st
( ( for s being Element of product () holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ()))) ) & the carrier of b2 = & IC = 0 & the InstructionsF of b2 = {[0,0,0],[1,0,0]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & ex f being Function of (product ()),(product ()) st
( ( for s being Element of product () holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ()))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines STC AMISTD_1:def 7 :
for N being with_zero set
for b2 being strict AMI-Struct over N holds
( b2 = STC N iff ( the carrier of b2 = & IC = 0 & the InstructionsF of b2 = {[0,0,0],[1,0,0]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & ex f being Function of (product ()),(product ()) st
( ( for s being Element of product () holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ()))) ) ) );

registration
let N be with_zero set ;
cluster STC N -> non empty finite strict ;
coherence
( STC N is finite & not STC N is empty )
by Def7;
end;

registration
let N be with_zero set ;
coherence
proof end;
end;

registration
let N be with_zero set ;
coherence
proof end;
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 s) + 1

proof end;

theorem Th4: :: AMISTD_1:4
for N being with_zero set
for i being Instruction of (STC N) st InsCode i = 0 holds
i is halting
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
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 )
proof end;

theorem :: AMISTD_1:7
for N being with_zero set
for i being Instruction of (STC N) holds i is jump-only
proof end;

registration
let N be with_zero set ;
cluster -> ins-loc-free for Instruction of (STC N);
coherence
for b1 being Instruction of (STC N) holds b1 is ins-loc-free
proof end;
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)}
proof end;

registration
let N be with_zero set ;
coherence
STC N is standard
proof end;
end;

registration
let N be with_zero set ;
coherence
STC N is halting
proof end;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st
( b1 is standard & b1 is halting )
proof end;
end;

theorem :: AMISTD_1:9
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 s) + 1 by Lm3;

theorem :: AMISTD_1:10
for N being with_zero set
for l being Nat
for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(l + 1)} by Lm4;

theorem :: AMISTD_1:11
for N being with_zero set
for l being Nat holds SUCC (l,(STC N)) = {l,(l + 1)} by Th8;

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;
attr i is sequential means :: AMISTD_1:def 8
for s being State of S holds (Exec (i,s)) . () = (IC s) + 1;
end;

:: 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 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)}
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;
cluster sequential -> non halting for Instruction of S;
coherence
for b1 being Instruction of S st b1 is sequential holds
not b1 is halting
proof end;
cluster halting -> non sequential for Instruction of S;
coherence
for b1 being Instruction of S st b1 is halting holds
not b1 is sequential
;
end;

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

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

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; 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; end; :: 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 b2 -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 ); 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 ) 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 proof end; end; theorem :: AMISTD_1:15 canceled; theorem :: AMISTD_1:16 canceled; ::$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;
existence
ex b1 being MacroInstruction of S st
( b1 is really-closed & b1 is trivial )
proof end;
end;

theorem :: AMISTD_1:17
for N being with_zero set
for i being Instruction of () holds i is halting
proof end;

theorem :: AMISTD_1:18
for N being with_zero set
for i being Element of the InstructionsF of () 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)
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)
proof end;

registration
let N be with_zero set ;
let p be PartState of (STC N);
coherence
proof end;
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;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
existence
ex b1 being NAT -defined the InstructionsF of S -valued non empty finite non halt-free Function st b1 is parahalting
proof end;
end;