:: by Artur Korni{\l}owicz

::

:: Received April 14, 2000

:: Copyright (c) 2000-2018 Association of Mizar Users

definition

let R be Ring;

let la, lb be Data-Location of R;

let a, b be Element of R;

:: original: -->

redefine func (la,lb) --> (a,b) -> FinPartState of (SCM R);

coherence

(la,lb) --> (a,b) is FinPartState of (SCM R)

end;
let la, lb be Data-Location of R;

let a, b be Element of R;

:: original: -->

redefine func (la,lb) --> (a,b) -> FinPartState of (SCM R);

coherence

(la,lb) --> (a,b) is FinPartState of (SCM R)

proof end;

::$CT

theorem :: SCMRING3:5

theorem :: SCMRING3:6

theorem :: SCMRING3:7

theorem :: SCMRING3:8

theorem :: SCMRING3:9

theorem :: SCMRING3:11

theorem Th12: :: SCMRING3:13

for R being Ring

for I being Instruction of (SCM R) st InsCode I = 1 holds

ex a, b being Data-Location of R st I = a := b

for I being Instruction of (SCM R) st InsCode I = 1 holds

ex a, b being Data-Location of R st I = a := b

proof end;

theorem Th13: :: SCMRING3:14

for R being Ring

for I being Instruction of (SCM R) st InsCode I = 2 holds

ex a, b being Data-Location of R st I = AddTo (a,b)

for I being Instruction of (SCM R) st InsCode I = 2 holds

ex a, b being Data-Location of R st I = AddTo (a,b)

proof end;

theorem Th14: :: SCMRING3:15

for R being Ring

for I being Instruction of (SCM R) st InsCode I = 3 holds

ex a, b being Data-Location of R st I = SubFrom (a,b)

for I being Instruction of (SCM R) st InsCode I = 3 holds

ex a, b being Data-Location of R st I = SubFrom (a,b)

proof end;

theorem Th15: :: SCMRING3:16

for R being Ring

for I being Instruction of (SCM R) st InsCode I = 4 holds

ex a, b being Data-Location of R st I = MultBy (a,b)

for I being Instruction of (SCM R) st InsCode I = 4 holds

ex a, b being Data-Location of R st I = MultBy (a,b)

proof end;

theorem Th16: :: SCMRING3:17

for R being Ring

for I being Instruction of (SCM R) st InsCode I = 5 holds

ex a being Data-Location of R ex r being Element of R st I = a := r

for I being Instruction of (SCM R) st InsCode I = 5 holds

ex a being Data-Location of R ex r being Element of R st I = a := r

proof end;

theorem Th17: :: SCMRING3:18

for R being Ring

for I being Instruction of (SCM R) st InsCode I = 6 holds

ex i2 being Nat st I = goto (i2,R)

for I being Instruction of (SCM R) st InsCode I = 6 holds

ex i2 being Nat st I = goto (i2,R)

proof end;

theorem Th18: :: SCMRING3:19

for R being Ring

for I being Instruction of (SCM R) st InsCode I = 7 holds

ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1

for I being Instruction of (SCM R) st InsCode I = 7 holds

ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1

proof end;

Lm1: for x, y being set st x in dom <*y*> holds

x = 1

proof end;

Lm2: for R being Ring

for T being InsType of the InstructionsF of (SCM R) holds

( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )

proof end;

theorem :: SCMRING3:20

for R being Ring

for T being InsType of the InstructionsF of (SCM R) st T = 0 holds

JumpParts T = {0}

for T being InsType of the InstructionsF of (SCM R) st T = 0 holds

JumpParts T = {0}

proof end;

theorem :: SCMRING3:21

for R being Ring

for T being InsType of the InstructionsF of (SCM R) st T = 1 holds

JumpParts T = {{}}

for T being InsType of the InstructionsF of (SCM R) st T = 1 holds

JumpParts T = {{}}

proof end;

theorem :: SCMRING3:22

for R being Ring

for T being InsType of the InstructionsF of (SCM R) st T = 2 holds

JumpParts T = {{}}

for T being InsType of the InstructionsF of (SCM R) st T = 2 holds

JumpParts T = {{}}

proof end;

theorem :: SCMRING3:23

for R being Ring

for T being InsType of the InstructionsF of (SCM R) st T = 3 holds

JumpParts T = {{}}

for T being InsType of the InstructionsF of (SCM R) st T = 3 holds

JumpParts T = {{}}

proof end;

theorem :: SCMRING3:24

for R being Ring

for T being InsType of the InstructionsF of (SCM R) st T = 4 holds

JumpParts T = {{}}

for T being InsType of the InstructionsF of (SCM R) st T = 4 holds

JumpParts T = {{}}

proof end;

theorem :: SCMRING3:25

for R being Ring

for T being InsType of the InstructionsF of (SCM R) st T = 5 holds

JumpParts T = {{}}

for T being InsType of the InstructionsF of (SCM R) st T = 5 holds

JumpParts T = {{}}

proof end;

theorem Th25: :: SCMRING3:26

for R being Ring

for T being InsType of the InstructionsF of (SCM R) st T = 6 holds

dom (product" (JumpParts T)) = {1}

for T being InsType of the InstructionsF of (SCM R) st T = 6 holds

dom (product" (JumpParts T)) = {1}

proof end;

theorem Th26: :: SCMRING3:27

for R being Ring

for T being InsType of the InstructionsF of (SCM R) st T = 7 holds

dom (product" (JumpParts T)) = {1}

for T being InsType of the InstructionsF of (SCM R) st T = 7 holds

dom (product" (JumpParts T)) = {1}

proof end;

theorem :: SCMRING3:29

for R being Ring

for a being Data-Location of R

for i1 being Nat holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT

for a being Data-Location of R

for i1 being Nat holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT

proof end;

Lm3: for R being Ring

for i being Instruction of (SCM R) st ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) holds

JUMP i is empty

proof end;

registration
end;

registration

let R be Ring;

let a, b be Data-Location of R;

coherence

a := b is sequential by SCMRING2:11;

coherence

AddTo (a,b) is sequential by SCMRING2:12;

coherence

SubFrom (a,b) is sequential by SCMRING2:13;

coherence

MultBy (a,b) is sequential by SCMRING2:14;

end;
let a, b be Data-Location of R;

coherence

a := b is sequential by SCMRING2:11;

coherence

AddTo (a,b) is sequential by SCMRING2:12;

coherence

SubFrom (a,b) is sequential by SCMRING2:13;

coherence

MultBy (a,b) is sequential by SCMRING2:14;

registration

let R be Ring;

let a be Data-Location of R;

let r be Element of R;

coherence

a := r is sequential by SCMRING2:17;

end;
let a be Data-Location of R;

let r be Element of R;

coherence

a := r is sequential by SCMRING2:17;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let R be Ring;

let a be Data-Location of R;

let r be Element of R;

coherence

JUMP (a := r) is empty

end;
let a be Data-Location of R;

let r be Element of R;

coherence

JUMP (a := r) is empty

proof end;

registration
end;

theorem Th31: :: SCMRING3:32

for R being Ring

for a being Data-Location of R

for il, i1 being Nat holds

( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )

for a being Data-Location of R

for il, i1 being Nat holds

( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )

proof end;

theorem :: SCMRING3:33

for R being non trivial Ring

for a being Data-Location of R

for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}

for a being Data-Location of R

for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}

proof end;

registration

let R be Ring;

let a be Data-Location of R;

let i1 be Nat;

coherence

JUMP (a =0_goto i1) is 1 -element

end;
let a be Data-Location of R;

let i1 be Nat;

coherence

JUMP (a =0_goto i1) is 1 -element

proof end;

theorem Th35: :: SCMRING3:36

for R being Ring

for k being Nat holds

( k + 1 in SUCC (k,(SCM R)) & ( for j being Nat st j in SUCC (k,(SCM R)) holds

k <= j ) )

for k being Nat holds

( k + 1 in SUCC (k,(SCM R)) & ( for j being Nat st j in SUCC (k,(SCM R)) holds

k <= j ) )

proof end;

definition

let R be Ring;

let k be Nat;

coherence

dl. k is Data-Location of R by AMI_2:def 16, AMI_3:27, SCMRING2:1;

end;
let k be Nat;

coherence

dl. k is Data-Location of R by AMI_2:def 16, AMI_3:27, SCMRING2:1;

:: deftheorem defines dl. SCMRING3:def 1 :

for R being Ring

for k being Nat holds dl. (R,k) = dl. k;

for R being Ring

for k being Nat holds dl. (R,k) = dl. k;

registration

let R be Ring;

coherence

for b_{1} being InsType of the InstructionsF of (SCM R) st b_{1} = InsCode (halt (SCM R)) holds

b_{1} is jump-only

end;
coherence

for b

b

proof end;

registration
end;

registration

let R be Ring;

let i1 be Nat;

coherence

for b_{1} being InsType of the InstructionsF of (SCM R) st b_{1} = InsCode (goto (i1,R)) holds

b_{1} is jump-only

end;
let i1 be Nat;

coherence

for b

b

proof end;

registration

let R be Ring;

let a be Data-Location of R;

let i1 be Nat;

coherence

for b_{1} being InsType of the InstructionsF of (SCM R) st b_{1} = InsCode (a =0_goto i1) holds

b_{1} is jump-only

end;
let a be Data-Location of R;

let i1 be Nat;

coherence

for b

b

proof end;

registration
end;

registration

let S be non trivial Ring;

let p, q be Data-Location of S;

coherence

for b_{1} being InsType of the InstructionsF of (SCM S) st b_{1} = InsCode (p := q) holds

not b_{1} is jump-only

end;
let p, q be Data-Location of S;

coherence

for b

not b

proof end;

registration
end;

registration

let S be non trivial Ring;

let p, q be Data-Location of S;

coherence

for b_{1} being InsType of the InstructionsF of (SCM S) st b_{1} = InsCode (AddTo (p,q)) holds

not b_{1} is jump-only

end;
let p, q be Data-Location of S;

coherence

for b

not b

proof end;

registration
end;

registration

let S be non trivial Ring;

let p, q be Data-Location of S;

coherence

for b_{1} being InsType of the InstructionsF of (SCM S) st b_{1} = InsCode (SubFrom (p,q)) holds

not b_{1} is jump-only

end;
let p, q be Data-Location of S;

coherence

for b

not b

proof end;

registration

let S be non trivial Ring;

let p, q be Data-Location of S;

coherence

not SubFrom (p,q) is jump-only ;

end;
let p, q be Data-Location of S;

coherence

not SubFrom (p,q) is jump-only ;

registration

let S be non trivial Ring;

let p, q be Data-Location of S;

coherence

for b_{1} being InsType of the InstructionsF of (SCM S) st b_{1} = InsCode (MultBy (p,q)) holds

not b_{1} is jump-only

end;
let p, q be Data-Location of S;

coherence

for b

not b

proof end;

registration
end;

registration

let S be non trivial Ring;

let p be Data-Location of S;

let w be Element of S;

coherence

for b_{1} being InsType of the InstructionsF of (SCM S) st b_{1} = InsCode (p := w) holds

not b_{1} is jump-only

end;
let p be Data-Location of S;

let w be Element of S;

coherence

for b

not b

proof end;

registration

let S be non trivial Ring;

let p be Data-Location of S;

let w be Element of S;

coherence

not p := w is jump-only ;

end;
let p be Data-Location of S;

let w be Element of S;

coherence

not p := w is jump-only ;

registration

let R be Ring;

let a be Data-Location of R;

let i1 be Nat;

coherence

not a =0_goto i1 is sequential

end;
let a be Data-Location of R;

let i1 be Nat;

coherence

not a =0_goto i1 is sequential

proof end;

registration

let R be Ring;

let a be Data-Location of R;

let i1 be Nat;

coherence

not a =0_goto i1 is ins-loc-free ;

end;
let a be Data-Location of R;

let i1 be Nat;

coherence

not a =0_goto i1 is ins-loc-free ;

theorem Th37: :: SCMRING3:38

for R being Ring

for a being Data-Location of R

for i1, k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)

for a being Data-Location of R

for i1, k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)

proof end;

registration
end;