:: by Artur Korni{\l}owicz

::

:: Received May 8, 2001

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

definition

let la, lb be Int-Location;

let a, b be Integer;

:: original: -->

redefine func (la,lb) --> (a,b) -> PartState of SCM+FSA;

coherence

(la,lb) --> (a,b) is PartState of SCM+FSA

end;
let a, b be Integer;

:: original: -->

redefine func (la,lb) --> (a,b) -> PartState of SCM+FSA;

coherence

(la,lb) --> (a,b) is PartState of SCM+FSA

proof end;

theorem Th1: :: SCMFSA10:1

for o being Object of SCM+FSA holds

( not o in Data-Locations or o is Int-Location or o is FinSeq-Location )

( not o in Data-Locations or o is Int-Location or o is FinSeq-Location )

proof end;

theorem Th23: :: SCMFSA10:23

for T being InsType of the InstructionsF of SCM+FSA st T = 6 holds

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

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

proof end;

theorem Th24: :: SCMFSA10:24

for T being InsType of the InstructionsF of SCM+FSA st T = 7 holds

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

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

proof end;

theorem Th25: :: SCMFSA10:25

for T being InsType of the InstructionsF of SCM+FSA st T = 8 holds

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

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

proof end;

theorem :: SCMFSA10:31

for i1 being Nat

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

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

proof end;

theorem :: SCMFSA10:32

for i1 being Nat

for a being Int-Location holds (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 = NAT

for a being Int-Location holds (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 = NAT

proof end;

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

JUMP i is empty

proof end;

registration

let a, b be Int-Location;

coherence

a := b is sequential by SCMFSA_2:63;

coherence

AddTo (a,b) is sequential by SCMFSA_2:64;

coherence

SubFrom (a,b) is sequential by SCMFSA_2:65;

coherence

MultBy (a,b) is sequential by SCMFSA_2:66;

coherence

Divide (a,b) is sequential by SCMFSA_2:67;

end;
coherence

a := b is sequential by SCMFSA_2:63;

coherence

AddTo (a,b) is sequential by SCMFSA_2:64;

coherence

SubFrom (a,b) is sequential by SCMFSA_2:65;

coherence

MultBy (a,b) is sequential by SCMFSA_2:66;

coherence

Divide (a,b) is sequential by SCMFSA_2:67;

registration

let a, b be Int-Location;

coherence

JUMP (a := b) is empty

JUMP (AddTo (a,b)) is empty

JUMP (SubFrom (a,b)) is empty

JUMP (MultBy (a,b)) is empty

JUMP (Divide (a,b)) is empty

end;
coherence

JUMP (a := b) is empty

proof end;

coherence JUMP (AddTo (a,b)) is empty

proof end;

coherence JUMP (SubFrom (a,b)) is empty

proof end;

coherence JUMP (MultBy (a,b)) is empty

proof end;

coherence JUMP (Divide (a,b)) is empty

proof end;

registration
end;

registration
end;

registration

let a, b be Int-Location;

let f be FinSeq-Location ;

coherence

a := (f,b) is sequential by SCMFSA_2:72;

end;
let f be FinSeq-Location ;

coherence

a := (f,b) is sequential by SCMFSA_2:72;

registration
end;

registration

let a, b be Int-Location;

let f be FinSeq-Location ;

coherence

(f,b) := a is sequential by SCMFSA_2:73;

end;
let f be FinSeq-Location ;

coherence

(f,b) := a is sequential by SCMFSA_2:73;

registration
end;

registration
end;

registration
end;

registration

let a be Int-Location;

let f be FinSeq-Location ;

coherence

f :=<0,...,0> a is sequential by SCMFSA_2:75;

end;
let f be FinSeq-Location ;

coherence

f :=<0,...,0> a is sequential by SCMFSA_2:75;

registration

let a be Int-Location;

let f be FinSeq-Location ;

coherence

JUMP (f :=<0,...,0> a) is empty

end;
let f be FinSeq-Location ;

coherence

JUMP (f :=<0,...,0> a) is empty

proof end;

theorem Th40: :: SCMFSA10:40

for k being Nat holds

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

k <= j ) )

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

k <= j ) )

proof end;

registration

coherence

for b_{1} being InsType of the InstructionsF of SCM+FSA st b_{1} = InsCode (halt SCM+FSA) 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+FSA st b_{1} = InsCode (goto i1) holds

b_{1} is jump-only

end;
coherence

for b

b

proof end;

registration

let i1 be Nat;

coherence

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

end;
coherence

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

proof end;

registration

let a be Int-Location;

let i1 be Nat;

coherence

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

b_{1} is jump-only

for b_{1} being InsType of the InstructionsF of SCM+FSA 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 Int-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: intloc 0 <> intloc 1

by AMI_3:10;

registration

let a, b be Int-Location;

coherence

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

not b_{1} is jump-only

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

not b_{1} is jump-only

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

not b_{1} is jump-only

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

not b_{1} is jump-only

for b_{1} being InsType of the InstructionsF of SCM+FSA 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;

Lm3: fsloc 0 <> intloc 0

by SCMFSA_2:99;

Lm4: fsloc 0 <> intloc 1

by SCMFSA_2:99;

registration

let a, b be Int-Location;

let f be FinSeq-Location ;

coherence

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

not b_{1} is jump-only

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

not b_{1} is jump-only

end;
let f be FinSeq-Location ;

coherence

for b

not b

proof end;

coherence for b

not b

proof end;

registration

let a, b be Int-Location;

let f be FinSeq-Location ;

coherence

not b := (f,a) is jump-only ;

coherence

not (f,a) := b is jump-only ;

end;
let f be FinSeq-Location ;

coherence

not b := (f,a) is jump-only ;

coherence

not (f,a) := b is jump-only ;

registration

let a be Int-Location;

let f be FinSeq-Location ;

coherence

for b_{1} being InsType of the InstructionsF of SCM+FSA st b_{1} = InsCode (a :=len f) holds

not b_{1} is jump-only

for b_{1} being InsType of the InstructionsF of SCM+FSA st b_{1} = InsCode (f :=<0,...,0> a) holds

not b_{1} is jump-only

end;
let f be FinSeq-Location ;

coherence

for b

not b

proof end;

coherence for b

not b

proof end;

registration

let a be Int-Location;

let f be FinSeq-Location ;

coherence

not a :=len f is jump-only ;

coherence

not f :=<0,...,0> a is jump-only ;

end;
let f be FinSeq-Location ;

coherence

not a :=len f is jump-only ;

coherence

not f :=<0,...,0> a is jump-only ;

registration
end;