:: Normal Computers
:: by Andrzej Trybulec
::
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users


begin

definition
let l be Element of NAT ;
:: original: succ
redefine func succ l -> Element of NAT ;
coherence
succ l is Element of NAT ;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite AMI-Struct of N;
let p be PartState of S;
let k be Element of NAT ;
:: original: Shift
redefine func Shift p,k -> PartState of S;
coherence
Shift p,k is PartState of S
proof end;
end;

registration
let N be set ;
let S be AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let k be Element of NAT ;
cluster Shift p,k -> the Instructions of S -valued ;
coherence
Shift p,k is the Instructions of S -valued
proof end;
end;

definition
let N be set ;
let S be AMI-Struct of N;
mode preProgram of S is NAT -defined FinPartState of ;
end;

definition
let F be Function;
attr F is initial means :Def1: :: SCMNORM:def 1
for m, n being Nat st n in dom F & m < n holds
m in dom F;
end;

:: deftheorem Def1 defines initial SCMNORM:def 1 :
for F being Function holds
( F is initial iff for m, n being Nat st n in dom F & m < n holds
m in dom F );

registration
cluster Relation-like Function-like empty -> initial set ;
coherence
for b1 being Function st b1 is empty holds
b1 is initial
proof end;
end;

registration
let N be with_non-empty_elements set ;
let S be AMI-Struct of N;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible empty finite countable set ;
existence
ex b1 being FinPartState of S st b1 is empty
proof end;
end;

registration
let N be set ;
let S be AMI-Struct of N;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible empty finite -> NAT -defined set ;
coherence
for b1 being FinPartState of S st b1 is empty holds
b1 is NAT -defined
proof end;
end;

registration
let N be set ;
let S be AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable initial set ;
existence
ex b1 being preProgram of S st b1 is initial
proof end;
end;

definition
let N be set ;
let S be AMI-Struct of N;
mode Program of S is initial preProgram of S;
end;

registration
cluster Relation-like Function-like T-Sequence-like finite -> initial set ;
coherence
for b1 being XFinSequence holds b1 is initial
proof end;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting definite AMI-Struct of N;
func Stop S -> Program of S equals :: SCMNORM:def 2
<%(halt S)%>;
coherence
<%(halt S)%> is Program of S
proof end;
end;

:: deftheorem defines Stop SCMNORM:def 2 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting definite AMI-Struct of N holds Stop S = <%(halt S)%>;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting definite AMI-Struct of N;
cluster Stop S -> non empty ;
coherence
not Stop S is empty ;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting definite AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible non empty finite countable initial set ;
existence
ex b1 being FinPartState of S st
( b1 is initial & b1 is NAT -defined & not b1 is empty )
proof end;
end;

theorem :: SCMNORM:1
canceled;

theorem :: SCMNORM:2
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting definite AMI-Struct of N holds 0 in dom (Stop S)
proof end;

theorem :: SCMNORM:3
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting definite AMI-Struct of N holds card (Stop S) = 1
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite AMI-Struct of N;
let p be FinPartState of S;
cluster ProgramPart p -> NAT -defined the Instructions of S -valued finite Function;
coherence
for b1 being Function st b1 = ProgramPart p holds
( b1 is finite & b1 is NAT -defined & b1 is the Instructions of S -valued )
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let I be initial FinPartState of S;
cluster ProgramPart I -> initial Function;
coherence
for b1 being Function st b1 = ProgramPart I holds
b1 is initial
proof end;
end;

definition
canceled;
canceled;
canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued finite Function;
mode Autonomy of p -> FinPartState of S means :Def7: :: SCMNORM:def 7
for s1, s2 being State of S st it c= s1 & it c= s2 holds
for q being NAT -defined the Instructions of S -valued finite Function st p c= q holds
for i being Nat holds (Comput p,s1,i) | (dom it) = (Comput q,s2,i) | (dom it);
existence
ex b1 being FinPartState of S st
for s1, s2 being State of S st b1 c= s1 & b1 c= s2 holds
for q being NAT -defined the Instructions of S -valued finite Function st p c= q holds
for i being Nat holds (Comput p,s1,i) | (dom b1) = (Comput q,s2,i) | (dom b1)
proof end;
end;

:: deftheorem SCMNORM:def 3 :
canceled;

:: deftheorem SCMNORM:def 4 :
canceled;

:: deftheorem SCMNORM:def 5 :
canceled;

:: deftheorem SCMNORM:def 6 :
canceled;

:: deftheorem Def7 defines Autonomy SCMNORM:def 7 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for b4 being FinPartState of S holds
( b4 is Autonomy of p iff for s1, s2 being State of S st b4 c= s1 & b4 c= s2 holds
for q being NAT -defined the Instructions of b2 -valued finite Function st p c= q holds
for i being Nat holds (Comput p,s1,i) | (dom b4) = (Comput q,s2,i) | (dom b4) );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite AMI-Struct of N;
let f be NAT -defined the Instructions of S -valued finite Function;
let s be State of S;
pred f halts_on s means :Def8: :: SCMNORM:def 8
 ex n being Nat st
( IC (Comput f,s,n) in dom f & CurInstr f,(Comput f,s,n) = halt S );
end;

:: deftheorem Def8 defines halts_on SCMNORM:def 8 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for f being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S holds
( f halts_on s iff ex n being Nat st
( IC (Comput f,s,n) in dom f & CurInstr f,(Comput f,s,n) = halt S ) );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite AMI-Struct of N;
let f be NAT -defined the Instructions of S -valued finite Function;
let p be Autonomy of f;
attr p is halting means :Def9: :: SCMNORM:def 9
for s being State of S st p c= s holds
f halts_on s;
end;

:: deftheorem Def9 defines halting SCMNORM:def 9 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for f being NAT -defined the Instructions of b2 -valued finite Function
for p being Autonomy of f holds
( p is halting iff for s being State of S st p c= s holds
f halts_on s );

theorem :: SCMNORM:4
canceled;

theorem :: SCMNORM:5
canceled;

theorem :: SCMNORM:6
canceled;

theorem Th7: :: SCMNORM:7
for i, j being Nat st i <= j holds
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for f being NAT -defined the Instructions of b4 -valued finite Function
for s being State of S st CurInstr f,(Comput f,s,i) = halt S holds
Comput f,s,j = Comput f,s,i
proof end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite AMI-Struct of N;
let f be NAT -defined the Instructions of S -valued finite Function;
let s be State of S;
assume A1: f halts_on s ;
func Result f,s -> State of S means :Def10: :: SCMNORM:def 10
 ex k being Nat st
( it = Comput f,s,k & CurInstr f,it = halt S );
uniqueness
for b1, b2 being State of S st ex k being Nat st
( b1 = Comput f,s,k & CurInstr f,b1 = halt S ) & ex k being Nat st
( b2 = Comput f,s,k & CurInstr f,b2 = halt S ) holds
b1 = b2
proof end;
correctness
existence
ex b1 being State of S ex k being Nat st
( b1 = Comput f,s,k & CurInstr f,b1 = halt S );
proof end;
end;

:: deftheorem Def10 defines Result SCMNORM:def 10 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for f being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S st f halts_on s holds
for b5 being State of S holds
( b5 = Result f,s iff ex k being Nat st
( b5 = Comput f,s,k & CurInstr f,b5 = halt S ) );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N;
let f be NAT -defined the Instructions of S -valued finite Function;
let p be Autonomy of f;
assume A1: p is halting ;
consider h being State of S such that
A2: p c= h by PBOOLE:156;
func Result f,p -> FinPartState of S means :: SCMNORM:def 11
for p9 being State of S st p c= p9 holds
it = (Result f,p9) | (dom p);
existence
ex b1 being FinPartState of S st
for p9 being State of S st p c= p9 holds
b1 = (Result f,p9) | (dom p)
proof end;
correctness
uniqueness
for b1, b2 being FinPartState of S st ( for p9 being State of S st p c= p9 holds
b1 = (Result f,p9) | (dom p) ) & ( for p9 being State of S st p c= p9 holds
b2 = (Result f,p9) | (dom p) ) holds
b1 = b2;
proof end;
end;

:: deftheorem defines Result SCMNORM:def 11 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for f being NAT -defined the Instructions of b2 -valued finite Function
for p being Autonomy of f st p is halting holds
for b5 being FinPartState of S holds
( b5 = Result f,p iff for p9 being State of S st p c= p9 holds
b5 = (Result f,p9) | (dom p) );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N;
let f be NAT -defined the Instructions of S -valued finite Function;
let p be FinPartState of S;
let F be Function;
pred f,p computes F means :: SCMNORM:def 12
for s being FinPartState of S st s in dom F holds
ex q being Autonomy of f st
( q = p +* s & q is halting & F . s c= Result f,q );
end;

:: deftheorem defines computes SCMNORM:def 12 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for f being NAT -defined the Instructions of b2 -valued finite Function
for p being FinPartState of S
for F being Function holds
( f,p computes F iff for s being FinPartState of S st s in dom F holds
ex q being Autonomy of f st
( q = p +* s & q is halting & F . s c= Result f,q ) );

theorem :: SCMNORM:8
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for s being State of S
for f being NAT -defined the Instructions of b2 -valued finite Function
for k being Element of NAT st IC (Comput f,s,k) in dom f & f /. (IC (Comput f,s,k)) = halt S holds
Result f,s = Comput f,s,k
proof end;

theorem :: SCMNORM:9
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for l1, l2, k being Element of NAT holds
( Start-At (l1 + k),S = Start-At (l2 + k),S iff Start-At l1,S = Start-At l2,S )
proof end;

theorem :: SCMNORM:10
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for l1, l2 being Element of NAT
for k being Nat st Start-At l1,S = Start-At l2,S holds
Start-At (l1 -' k),S = Start-At (l2 -' k),S
proof end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let p be FinPartState of S;
let k be Element of NAT ;
func IncrIC p,k -> FinPartState of S equals :: SCMNORM:def 13
p +* (Start-At ((IC p) + k),S);
correctness
coherence
p +* (Start-At ((IC p) + k),S) is FinPartState of S;
;
end;

:: deftheorem defines IncrIC SCMNORM:def 13 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for p being FinPartState of S
for k being Element of NAT holds IncrIC p,k = p +* (Start-At ((IC p) + k),S);

theorem :: SCMNORM:11
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for l being Element of NAT holds DataPart (Start-At l,S) = {} by AMI_1:138;

theorem :: SCMNORM:12
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for p being FinPartState of S
for k being Element of NAT holds DataPart (IncrIC p,k) = DataPart p
proof end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let s be State of S;
func DataPart s -> PartState of S equals :: SCMNORM:def 14
s | (Data-Locations S);
coherence
s | (Data-Locations S) is PartState of S ;
end;

:: deftheorem defines DataPart SCMNORM:def 14 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for s being State of S holds DataPart s = s | (Data-Locations S);

theorem Th13: :: SCMNORM:13
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for s being State of S holds Data-Locations S c= dom s
proof end;

theorem :: SCMNORM:14
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for s being State of S holds dom (DataPart s) = Data-Locations S
proof end;

theorem Th15: :: SCMNORM:15
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N holds NAT misses Data-Locations S
proof end;

theorem :: SCMNORM:16
canceled;

theorem Th17: :: SCMNORM:17
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for l being Element of NAT holds IC S in dom (Start-At l,S)
proof end;

theorem :: SCMNORM:18
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S
for k being Element of NAT holds IC S in dom (IncrIC p,k)
proof end;

theorem Th19: :: SCMNORM:19
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for l being Element of NAT holds IC (Start-At l,S) = l
proof end;

theorem :: SCMNORM:20
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S
for k being Element of NAT holds (IncrIC p,k) . (IC S) = (IC p) + k
proof end;

theorem Th21: :: SCMNORM:21
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N holds not IC S in Data-Locations S
proof end;

theorem Th22: :: SCMNORM:22
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for d being data-only FinPartState of S holds not IC S in dom d
proof end;

theorem Th23: :: SCMNORM:23
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S
for d being data-only FinPartState of S holds IC (p +* d) = IC p
proof end;

theorem Th24: :: SCMNORM:24
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for l being Element of NAT
for d being data-only FinPartState of S holds d tolerates Start-At l,S
proof end;

theorem :: SCMNORM:25
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S
for k being Element of NAT
for d being data-only FinPartState of S holds IncrIC (p +* d),k = (IncrIC p,k) +* d
proof end;

theorem :: SCMNORM:26
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for d being data-only FinPartState of S
for f being NAT -defined the Instructions of b2 -valued finite Function holds d tolerates f
proof end;

theorem :: SCMNORM:27
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for k being Element of NAT
for d being data-only FinPartState of S holds (IncrIC d,k) | NAT = {}
proof end;

theorem :: SCMNORM:28
for N being non empty with_non-empty_elements set
for k being Element of NAT
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b3 -valued finite Function
for s being State of S holds Comput p,s,(k + 1) = Exec (p /. (IC (Comput p,s,k))),(Comput p,s,k)
proof end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty halting IC-Ins-separated AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued finite Function;
let l be set ;
pred p halts_at l means :Def15: :: SCMNORM:def 15
( l in dom p & p . l = halt S );
end;

:: deftheorem Def15 defines halts_at SCMNORM:def 15 :
for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for l being set holds
( p halts_at l iff ( l in dom p & p . l = halt S ) );

theorem Th83: :: SCMNORM:29
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S holds
( p halts_on s iff ex i being Nat st p halts_at IC (Comput p,s,i) )
proof end;

theorem Th85: :: SCMNORM:30
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S
for k being Nat st p halts_on s holds
( Result p,s = Comput p,s,k iff p halts_at IC (Comput p,s,k) )
proof end;

theorem Th87: :: SCMNORM:31
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S
for i being Nat st p halts_at IC (Comput p,s,i) holds
Result p,s = Comput p,s,i
proof end;

theorem Th88: :: SCMNORM:32
for i being Nat
for j being Element of NAT st i <= j holds
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b4 -valued finite Function
for s being State of S st p halts_at IC (Comput p,s,i) holds
p halts_at IC (Comput p,s,j)
proof end;

theorem :: SCMNORM:33
for i being Nat
for j being Element of NAT st i <= j holds
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b4 -valued finite Function
for s being State of S st p halts_at IC (Comput p,s,i) holds
Comput p,s,j = Comput p,s,i
proof end;

theorem Th51: :: SCMNORM:34
for i being Nat
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b3 -valued finite Function
for s being State of S
for k being Element of NAT holds Comput p,s,(i + k) = Comput p,(Comput p,s,i),k
proof end;

theorem Th56: :: SCMNORM:35
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S
for k being Element of NAT st IC (Comput p,s,k) in dom p & p . (IC (Comput p,s,k)) = halt S holds
Result p,s = Comput p,s,k
proof end;

theorem Th57: :: SCMNORM:36
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S st ex k being Element of NAT st
( IC (Comput p,s,k) in dom p & p . (IC (Comput p,s,k)) = halt S ) holds
for i being Nat holds Result p,s = Result p,(Comput p,s,i)
proof end;

theorem :: SCMNORM:37
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S st ex k being Element of NAT st p halts_at IC (Comput p,s,k) holds
for i being Nat holds Result p,s = Result p,(Comput p,s,i)
proof end;

theorem :: SCMNORM:38
for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued finite Function
for s being State of S holds
( p halts_on s iff ex k being Nat st p halts_at IC (Comput p,s,k) )
proof end;