Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Grzegorz Bancerek,
and
- Piotr Rudnicki
- Received October 8, 1993
- MML identifier: SCM_1
- [
Mizar article,
MML identifier index
]
environ
vocabulary AMI_3, INT_1, FINSEQ_1, AMI_1, AMI_2, FUNCT_1, RELAT_1, ARYTM_1,
NAT_1, MCART_1, SCM_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1,
MCART_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, AMI_1, AMI_2,
AMI_3;
constructors NAT_1, AMI_2, AMI_3, MEMBERED, XBOOLE_0;
clusters AMI_1, AMI_3, INT_1, XBOOLE_0, RELSET_1, FINSEQ_1, FRAENKEL, XREAL_0,
MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
definition
let i be Integer;
redefine func <*i*> -> FinSequence of INT;
end;
theorem :: SCM_1:1
for s being State of SCM
holds IC s = s.0 & CurInstr s = s.(s.0);
theorem :: SCM_1:2
for s being State of SCM, k being Nat
holds CurInstr (Computation s).k = s.(IC (Computation s).k) &
CurInstr (Computation s).k = s.((Computation s).k.0);
theorem :: SCM_1:3
for s being State of SCM
st ex k being Nat st s.(IC (Computation s).k) = halt SCM
holds s is halting;
theorem :: SCM_1:4
for s being State of SCM, k being Nat
st s.(IC (Computation s).k) = halt SCM
holds (Result s) = (Computation s).k;
canceled 2;
theorem :: SCM_1:7
for n, m being Nat holds
IC SCM <> il.n & IC SCM <> dl.n & il.n <> dl.m;
definition
let I be FinSequence of the Instructions of SCM,
D be FinSequence of INT,
il, ps, ds be Nat;
mode State-consisting of il, ps, ds, I, D -> State of SCM means
:: SCM_1:def 1
IC it = il.il &
(for k being Nat st k < len I holds it.il.(ps+k) = I.(k+1)) &
(for k being Nat st k < len D holds it.dl.(ds+k) = D.(k+1));
end;
theorem :: SCM_1:8
for x1, x2, x3, x4 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>
holds len p = 4 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4;
theorem :: SCM_1:9
for x1, x2, x3, x4, x5 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>
holds len p = 5 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5;
theorem :: SCM_1:10
for x1, x2, x3, x4, x5, x6 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>
holds len p = 6 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6;
theorem :: SCM_1:11
for x1, x2, x3, x4, x5, x6, x7 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>
holds len p = 7 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6 & p.7 = x7;
theorem :: SCM_1:12
for x1,x2,x3,x4, x5, x6, x7, x8 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>
holds len p = 8 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6 & p.7 = x7 & p.8 = x8;
theorem :: SCM_1:13
for x1,x2,x3,x4,x5,x6,x7, x8, x9 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>
holds len p = 9 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6 & p.7 = x7 & p.8 = x8 & p.9 = x9;
theorem :: SCM_1:14
for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM,
i1, i2, i3, i4 being Integer,
il being Nat,
s being State-consisting of il, 0, 0,
<*I1*>^<*I2*>^<*I3*>^<*I4*>^<*I5*>^<*I6*>^<*I7*>^<*I8*>^<*I9*>,
<*i1*>^<*i2*>^<*i3*>^<*i4*>
holds IC s = il.il &
s.il.0 = I1 & s.il.1 = I2 & s.il.2 = I3 & s.il.3 = I4 &
s.il.4 = I5 & s.il.5 = I6 & s.il.6 = I7 & s.il.7 = I8 & s.il.8 = I9 &
s.dl.0 = i1 & s.dl.1 = i2 & s.dl.2 = i3 & s.dl.3 = i4;
theorem :: SCM_1:15
for I1, I2 being Instruction of SCM,
i1, i2 being Integer,
il being Nat,
s being State-consisting of il, 0, 0, <*I1*>^<*I2*>, <*i1*>^<*i2*>
holds IC s = il.il &
s.il.0 = I1 & s.il.1 = I2 &
s.dl.0 = i1 & s.dl.1 = i2;
definition
let N be with_non-empty_elements set;
let S be halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let s be State of S such that
s is halting;
func Complexity s -> Nat means
:: SCM_1:def 2
CurInstr((Computation s).it) = halt S &
for k being Nat st CurInstr((Computation s).k) = halt S holds it <= k;
synonym LifeSpan s;
end;
theorem :: SCM_1:16
for s being State of SCM, k being Nat
holds s.(IC (Computation s).k) <> halt SCM &
s.(IC (Computation s).(k+1)) = halt SCM
iff Complexity s = k+1 & s is halting;
theorem :: SCM_1:17
for s being State of SCM, k being Nat
st IC (Computation s).k <> IC (Computation s).(k+1) &
s.(IC (Computation s).(k+1)) = halt SCM
holds Complexity s = k+1;
theorem :: SCM_1:18
for k, n being Nat, s being State of SCM, a, b being Data-Location
st IC (Computation s).k = il.n & s.il.n = a := b
holds IC (Computation s).(k+1) = il.(n+1) &
(Computation s).(k+1).a = (Computation s).k.b &
for d being Data-Location st d <> a holds
(Computation s).(k+1).d = (Computation s).k.d;
theorem :: SCM_1:19
for k, n being Nat, s being State of SCM, a, b being Data-Location
st IC (Computation s).k = il.n & s.il.n = AddTo(a,b)
holds IC (Computation s).(k+1) = il.(n+1) &
(Computation s).(k+1).a = (Computation s).k.a+(Computation s).k.b &
for d being Data-Location st d <> a holds
(Computation s).(k+1).d = (Computation s).k.d;
theorem :: SCM_1:20
for k, n being Nat, s being State of SCM, a, b being Data-Location
st IC (Computation s).k = il.n & s.il.n = SubFrom(a,b)
holds IC (Computation s).(k+1) = il.(n+1) &
(Computation s).(k+1).a = (Computation s).k.a-(Computation s).k.b &
for d being Data-Location st d <> a holds
(Computation s).(k+1).d = (Computation s).k.d;
theorem :: SCM_1:21
for k, n being Nat, s being State of SCM, a, b being Data-Location
st IC (Computation s).k = il.n & s.il.n = MultBy(a,b)
holds IC (Computation s).(k+1) = il.(n+1) &
(Computation s).(k+1).a = (Computation s).k.a*(Computation s).k.b &
for d being Data-Location st d <> a holds
(Computation s).(k+1).d = (Computation s).k.d;
theorem :: SCM_1:22
for k, n being Nat, s being State of SCM, a, b being Data-Location
st IC (Computation s).k = il.n & s.il.n = Divide(a,b) & a<>b
holds IC (Computation s).(k+1) = il.(n+1) &
(Computation s).(k+1).a = (Computation s).k.a div (Computation s).k.b &
(Computation s).(k+1).b = (Computation s).k.a mod (Computation s).k.b &
for d being Data-Location st d <> a & d <> b holds
(Computation s).(k+1).d = (Computation s).k.d;
theorem :: SCM_1:23
for k, n being Nat, s being State of SCM,
il being Instruction-Location of SCM
st IC (Computation s).k = il.n & s.il.n = goto il
holds IC (Computation s).(k+1) = il &
for d being Data-Location holds
(Computation s).(k+1).d = (Computation s).k.d;
theorem :: SCM_1:24
for k, n being Nat, s being State of SCM, a being Data-Location,
il being Instruction-Location of SCM
st IC (Computation s).k = il.n & s.il.n = a =0_goto il
holds ((Computation s).k.a = 0 implies IC (Computation s).(k+1) = il) &
((Computation s).k.a <>0 implies IC (Computation s).(k+1) = il.(n+1)) &
for d being Data-Location holds
(Computation s).(k+1).d = (Computation s).k.d;
theorem :: SCM_1:25
for k, n being Nat, s being State of SCM, a being Data-Location,
il being Instruction-Location of SCM
st IC (Computation s).k = il.n & s.il.n = a >0_goto il
holds ((Computation s).k.a > 0 implies IC (Computation s).(k+1) = il) &
((Computation s).k.a <= 0 implies IC (Computation s).(k+1) = il.(n+1)) &
for d being Data-Location holds
(Computation s).(k+1).d = (Computation s).k.d;
theorem :: SCM_1:26
(halt SCM)`1 = 0 &
(for a, b being Data-Location holds (a := b)`1 = 1) &
(for a, b being Data-Location holds (AddTo(a,b))`1 = 2) &
(for a, b being Data-Location holds (SubFrom(a,b))`1 = 3) &
(for a, b being Data-Location holds (MultBy(a,b))`1 = 4) &
(for a, b being Data-Location holds (Divide(a,b))`1 = 5) &
(for i being Instruction-Location of SCM holds (goto i)`1 = 6) &
(for a being Data-Location, i being Instruction-Location of SCM
holds (a =0_goto i)`1 = 7) &
(for a being Data-Location, i being Instruction-Location of SCM
holds (a >0_goto i)`1 = 8);
theorem :: SCM_1:27
for N being non empty with_non-empty_elements set,
S be IC-Ins-separated definite halting
(non empty non void AMI-Struct over N),
s being State of S, m being Nat
holds s is halting iff (Computation s).m is halting;
theorem :: SCM_1:28
for s1, s2 being State of SCM, k, c being Nat
st s2 = (Computation s1).k & Complexity s2 = c & s2 is halting & 0 < c
holds Complexity s1 = k+c;
theorem :: SCM_1:29
for s1, s2 being State of SCM, k being Nat
st s2 = (Computation s1).k & s2 is halting
holds Result s2 = Result s1;
theorem :: SCM_1:30
for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM,
i1, i2, i3, i4 being Integer,
il being Nat,
s being State of SCM
st IC s = il.il &
s.il.0 = I1 & s.il.1 = I2 & s.il.2 = I3 & s.il.3 = I4 &
s.il.4 = I5 & s.il.5 = I6 & s.il.6 = I7 & s.il.7 = I8 & s.il.8 = I9 &
s.dl.0 = i1 & s.dl.1 = i2 & s.dl.2 = i3 & s.dl.3 = i4
holds
s is State-consisting of il, 0, 0,
<*I1*>^<*I2*>^<*I3*>^<*I4*>^<*I5*>^<*I6*>^<*I7*>^<*I8*>^<*I9*>,
<*i1*>^<*i2*>^<*i3*>^<*i4*>;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Empty program
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:31
for s being State-consisting of 0, 0, 0, <*halt SCM*>, <*>INT
holds s is halting & Complexity s = 0 & Result s = s;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Assignment
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:32
for i1, i2 being Integer,
s being State-consisting of 0, 0, 0, <*dl.0 := dl.1*>^<*halt SCM*>,
<*i1*>^<*i2*>
holds s is halting &
Complexity s = 1 &
(Result s).dl.0 = i2 &
for d being Data-Location st d<>dl.0 holds (Result s).d = s.d;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Adding two integers
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:33
for i1, i2 being Integer,
s being State-consisting of 0, 0, 0, <*AddTo(dl.0,dl.1)*>^<*halt SCM*>,
<*i1*>^<*i2*>
holds s is halting &
Complexity s = 1 &
(Result s).dl.0 = i1 + i2 &
for d being Data-Location st d<>dl.0 holds (Result s).d = s.d;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Subtracting two integers
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:34
for i1, i2 being Integer,
s being State-consisting of 0, 0, 0, <*SubFrom(dl.0,dl.1)*>^<*halt SCM*>,
<*i1*>^<*i2*>
holds s is halting &
Complexity s = 1 &
(Result s).dl.0 = i1 - i2 &
for d being Data-Location st d<>dl.0 holds (Result s).d = s.d;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Multiplying two integers
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:35
for i1, i2 being Integer,
s being State-consisting of 0, 0, 0, <*MultBy(dl.0,dl.1)*>^<*halt SCM*>,
<*i1*>^<*i2*>
holds s is halting &
Complexity s = 1 &
(Result s).dl.0 = i1 * i2 &
for d being Data-Location st d<>dl.0 holds (Result s).d = s.d;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Dividing two integers
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:36
for i1, i2 being Integer,
s being State-consisting of 0, 0, 0, <*Divide(dl.0,dl.1)*>^<*halt SCM*>,
<*i1*>^<*i2*>
holds s is halting &
Complexity s = 1 &
(Result s).dl.0 = i1 div i2 & (Result s).dl.1 = i1 mod i2 &
:: (i2 <> 0 implies abs((Result s).dl.1) < abs i2
for d being Data-Location st d<>dl.0 & d<>dl.1
holds (Result s).d = s.d;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Unconditional jump
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:37
for i1, i2 being Integer,
s being State-consisting of 0, 0, 0, <*goto il.1*>^<*halt SCM*>,
<*i1*>^<*i2*>
holds s is halting &
Complexity s = 1 &
for d being Data-Location holds (Result s).d = s.d;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Jump at zero
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:38
for i1, i2 being Integer,
s being State-consisting of 0, 0, 0, <*dl.0 =0_goto il.1*>^<*halt SCM*>,
<*i1*>^<*i2*>
holds s is halting &
Complexity s = 1 &
for d being Data-Location holds (Result s).d = s.d;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Jump at greater than zero
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: SCM_1:39
for i1, i2 being Integer,
s being State-consisting of 0, 0, 0, <*dl.0 >0_goto il.1*>^<*halt SCM*>,
<*i1*>^<*i2*>
holds s is halting &
Complexity s = 1 &
for d being Data-Location holds (Result s).d = s.d;
Back to top