:: by Artur Korni{\l}owicz

::

:: Received May 8, 2001

:: Copyright (c) 2001-2019 Association of Mizar Users

theorem :: AMI_6:13

for a being Data-Location

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

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

proof end;

theorem :: AMI_6:14

for a being Data-Location

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

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

proof end;

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

JUMP i is empty

proof end;

registration

let a, b be Data-Location;

coherence

a := b is sequential by AMI_3:2;

coherence

AddTo (a,b) is sequential by AMI_3:3;

coherence

SubFrom (a,b) is sequential by AMI_3:4;

coherence

MultBy (a,b) is sequential by AMI_3:5;

coherence

Divide (a,b) is sequential by AMI_3:6;

end;
coherence

a := b is sequential by AMI_3:2;

coherence

AddTo (a,b) is sequential by AMI_3:3;

coherence

SubFrom (a,b) is sequential by AMI_3:4;

coherence

MultBy (a,b) is sequential by AMI_3:5;

coherence

Divide (a,b) is sequential by AMI_3:6;

registration
end;

registration
end;

theorem Th22: :: AMI_6:22

for k being Nat holds

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

k <= j ) )

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

k <= j ) )

proof end;

registration

coherence

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

b_{1} is jump-only

end;
for b

b

proof end;

registration

let i1 be Nat;

coherence

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

b_{1} is jump-only

end;
coherence

for b

b

proof end;

registration

let i1 be Nat;

coherence

( SCM-goto i1 is jump-only & not SCM-goto i1 is sequential & not SCM-goto i1 is ins-loc-free )

end;
coherence

( SCM-goto i1 is jump-only & not SCM-goto i1 is sequential & not SCM-goto i1 is ins-loc-free )

proof end;

registration

let a be Data-Location;

let i1 be Nat;

coherence

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

b_{1} is jump-only

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

b_{1} is jump-only

end;
let i1 be Nat;

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let a be Data-Location;

let i1 be Nat;

coherence

( a =0_goto i1 is jump-only & not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free )

( a >0_goto i1 is jump-only & not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free )

end;
let i1 be Nat;

coherence

( a =0_goto i1 is jump-only & not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free )

proof end;

coherence ( a >0_goto i1 is jump-only & not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free )

proof end;

Lm2: dl. 0 <> dl. 1

by AMI_3:10;

registration

let a, b be Data-Location;

coherence

for b_{1} being InsType of the InstructionsF of SCM st b_{1} = InsCode (a := b) holds

not b_{1} is jump-only

for b_{1} being InsType of the InstructionsF of SCM st b_{1} = InsCode (AddTo (a,b)) holds

not b_{1} is jump-only

for b_{1} being InsType of the InstructionsF of SCM st b_{1} = InsCode (SubFrom (a,b)) holds

not b_{1} is jump-only

for b_{1} being InsType of the InstructionsF of SCM st b_{1} = InsCode (MultBy (a,b)) holds

not b_{1} is jump-only

for b_{1} being InsType of the InstructionsF of SCM st b_{1} = InsCode (Divide (a,b)) holds

not b_{1} is jump-only

end;
coherence

for b

not b

proof end;

coherence for b

not b

proof end;

coherence for b

not b

proof end;

coherence for b

not b

proof end;

coherence for b

not b

proof end;

registration

let a, b be Data-Location;

coherence

not a := b is jump-only ;

coherence

not AddTo (a,b) is jump-only ;

coherence

not SubFrom (a,b) is jump-only ;

coherence

not MultBy (a,b) is jump-only ;

coherence

not Divide (a,b) is jump-only ;

end;
coherence

not a := b is jump-only ;

coherence

not AddTo (a,b) is jump-only ;

coherence

not SubFrom (a,b) is jump-only ;

coherence

not MultBy (a,b) is jump-only ;

coherence

not Divide (a,b) is jump-only ;

registration
end;