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

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 the Instructions of S -valued FinPartState of ;
end;

registration
let N be with_non-empty_elements set ;
let S be AMI-Struct of N;
cluster empty 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 empty -> NAT -defined set ;
coherence
for b1 being FinPartState of S st b1 is empty holds
b1 is NAT -defined ;
end;

registration
let N be set ;
let S be AMI-Struct of N;
cluster 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;

definition
canceled;
canceled;
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 3
<%(halt S)%>;
coherence
<%(halt S)%> is Program of S
proof end;
end;

:: deftheorem SCMNORM:def 1 :
canceled;

:: deftheorem SCMNORM:def 2 :
canceled;

:: deftheorem defines Stop SCMNORM:def 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 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 non empty set ;
existence
not for b1 being Program of S holds 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 by AFINSQ_1:36;

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;

theorem :: SCMNORM:4
canceled;

theorem :: SCMNORM:5
canceled;

theorem :: SCMNORM:6
canceled;

theorem :: SCMNORM:7
canceled;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
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 SCMNORM:def 4 :
canceled;

:: deftheorem SCMNORM:def 5 :
canceled;

:: deftheorem SCMNORM:def 6 :
canceled;

:: deftheorem SCMNORM:def 7 :
canceled;

:: deftheorem SCMNORM:def 8 :
canceled;

:: deftheorem SCMNORM:def 9 :
canceled;

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

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
canceled;
canceled;
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 PartState of S;
let k be Element of NAT ;
func IncrIC p,k -> PartState of S equals :: SCMNORM:def 13
p +* (Start-At ((IC p) + k),S);
correctness
coherence
p +* (Start-At ((IC p) + k),S) is PartState of S;
;
end;

:: deftheorem SCMNORM:def 11 :
canceled;

:: deftheorem SCMNORM:def 12 :
canceled;

:: 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 PartState of S
for k being Element of NAT holds IncrIC p,k = p +* (Start-At ((IC p) + k),S);

theorem :: SCMNORM:11
canceled;

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;

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 Th18: :: 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 p being FinPartState of S
for k being Element of NAT holds IC (IncrIC p,k) = (IC p) + k
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 PartState of S holds ProgramPart (IncrIC d,k) = {}
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;

theorem :: SCMNORM:29
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 Start-At ((IC p) + k),S c= IncrIC p,k
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 Element of 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, 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, 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 Element of 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 Element of 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 Element of 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;

theorem :: SCMNORM:39
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 by FUNCOP_1:87;