begin
:: deftheorem Def1 defines initial SCMNORM:def 1 :
theorem
:: deftheorem defines Stop SCMNORM:def 2 :
theorem
theorem
:: deftheorem defines [ SCMNORM:def 3 :
:: deftheorem defines CurInstr SCMNORM:def 4 :
:: deftheorem defines Following SCMNORM:def 5 :
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
NAT -defined the
Instructions of
S -valued finite Function;
deffunc H1(
set ,
State of )
-> State of =
Following p,$2;
let s be
State of ;
let k be
Nat;
func Comput p,
s,
k -> State of
means :
Def6:
ex
f being
Function of
NAT ,
product the
Object-Kind of
S st
(
it = f . k &
f . 0 = s & ( for
i being
Nat holds
f . (i + 1) = Following p,
(f . i) ) );
existence
ex b1 being State of ex f being Function of NAT , product the Object-Kind of S st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) )
uniqueness
for b1, b2 being State of st ex f being Function of NAT , product the Object-Kind of S st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) & ex f being Function of NAT , product the Object-Kind of S st
( b2 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines Comput SCMNORM:def 6 :
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
NAT -defined the
Instructions of
S -valued finite Function;
mode Autonomy of
p -> FinPartState of
means :
Def7:
for
s1,
s2 being
State of 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 st
for s1, s2 being State of 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)
end;
:: deftheorem Def7 defines Autonomy SCMNORM:def 7 :
theorem Th4:
theorem Th5:
theorem
:: deftheorem Def8 defines halts_on SCMNORM:def 8 :
:: deftheorem Def9 defines halting SCMNORM:def 9 :
theorem Th7:
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 f be
NAT -defined the
Instructions of
S -valued finite Function;
let s be
State of ;
assume A1:
f halts_on s
;
func Result f,
s -> State of
means :
Def10:
ex
k being
Nat st
(
it = Comput f,
s,
k &
CurInstr f,
it = halt S );
uniqueness
for b1, b2 being State of 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
correctness
existence
ex b1 being State of ex k being Nat st
( b1 = Comput f,s,k & CurInstr f,b1 = halt S );
end;
:: deftheorem Def10 defines Result SCMNORM:def 10 :
:: deftheorem defines Result SCMNORM:def 11 :
:: deftheorem defines computes SCMNORM:def 12 :
theorem
theorem
theorem
:: deftheorem defines IncrIC SCMNORM:def 13 :
theorem
theorem
:: deftheorem defines DataPart SCMNORM:def 14 :
theorem Th13:
theorem
theorem Th15:
theorem
canceled;
theorem Th17:
theorem
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
theorem
theorem
:: deftheorem Def15 defines halts_at SCMNORM:def 15 :
theorem Th83:
theorem Th85:
theorem Th87:
theorem Th88:
theorem
theorem Th51:
theorem Th56:
theorem Th57:
theorem Th90:
theorem Th83: