:: by Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received September 27, 2003

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

definition

let la, lb be Int_position;

let a, b be Integer;

:: original: -->

redefine func (la,lb) --> (a,b) -> PartState of SCMPDS;

coherence

(la,lb) --> (a,b) is PartState of SCMPDS

end;
let a, b be Integer;

:: original: -->

redefine func (la,lb) --> (a,b) -> PartState of SCMPDS;

coherence

(la,lb) --> (a,b) is PartState of SCMPDS

proof end;

Lm1: for k being Integer holds JUMP (goto k) = {}

proof end;

registration
end;

theorem Th1: :: SCMPDS_9:1

for i being Instruction of SCMPDS

for l being Element of NAT st ( for s being State of SCMPDS st IC s = l holds

(Exec (i,s)) . (IC ) = (IC s) + 1 ) holds

NIC (i,l) = {(l + 1)}

for l being Element of NAT st ( for s being State of SCMPDS st IC s = l holds

(Exec (i,s)) . (IC ) = (IC s) + 1 ) holds

NIC (i,l) = {(l + 1)}

proof end;

theorem Th2: :: SCMPDS_9:2

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

JUMP i is empty

JUMP i is empty

proof end;

Lm2: for k being Nat st k > 1 holds

k - 2 is Element of NAT

proof end;

theorem Th4: :: SCMPDS_9:4

for a being Int_position

for l being Element of NAT holds NIC ((return a),l) = { k where k is Nat : k > 1 }

for l being Element of NAT holds NIC ((return a),l) = { k where k is Nat : k > 1 }

proof end;

theorem Th5: :: SCMPDS_9:5

for a being Int_position

for l being Element of NAT

for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(l + 1)}

for l being Element of NAT

for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(l + 1)}

proof end;

theorem Th6: :: SCMPDS_9:6

for a being Int_position

for l being Element of NAT

for k1 being Integer holds NIC ((a := k1),l) = {(l + 1)}

for l being Element of NAT

for k1 being Integer holds NIC ((a := k1),l) = {(l + 1)}

proof end;

theorem Th7: :: SCMPDS_9:7

for a being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) := k2),l) = {(l + 1)}

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) := k2),l) = {(l + 1)}

proof end;

theorem Th8: :: SCMPDS_9:8

for a, b being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) := (b,k2)),l) = {(l + 1)}

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) := (b,k2)),l) = {(l + 1)}

proof end;

theorem Th9: :: SCMPDS_9:9

for a being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC ((AddTo (a,k1,k2)),l) = {(l + 1)}

for l being Element of NAT

for k1, k2 being Integer holds NIC ((AddTo (a,k1,k2)),l) = {(l + 1)}

proof end;

theorem Th10: :: SCMPDS_9:10

for a, b being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC ((AddTo (a,k1,b,k2)),l) = {(l + 1)}

for l being Element of NAT

for k1, k2 being Integer holds NIC ((AddTo (a,k1,b,k2)),l) = {(l + 1)}

proof end;

theorem Th11: :: SCMPDS_9:11

for a, b being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC ((SubFrom (a,k1,b,k2)),l) = {(l + 1)}

for l being Element of NAT

for k1, k2 being Integer holds NIC ((SubFrom (a,k1,b,k2)),l) = {(l + 1)}

proof end;

theorem Th12: :: SCMPDS_9:12

for a, b being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC ((MultBy (a,k1,b,k2)),l) = {(l + 1)}

for l being Element of NAT

for k1, k2 being Integer holds NIC ((MultBy (a,k1,b,k2)),l) = {(l + 1)}

proof end;

theorem Th13: :: SCMPDS_9:13

for a, b being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC ((Divide (a,k1,b,k2)),l) = {(l + 1)}

for l being Element of NAT

for k1, k2 being Integer holds NIC ((Divide (a,k1,b,k2)),l) = {(l + 1)}

proof end;

theorem :: SCMPDS_9:14

for a being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) <>0_goto k2),l) = {(l + 1),|.(k2 + l).|}

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) <>0_goto k2),l) = {(l + 1),|.(k2 + l).|}

proof end;

theorem :: SCMPDS_9:15

for a being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) <=0_goto k2),l) = {(l + 1),|.(k2 + l).|}

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) <=0_goto k2),l) = {(l + 1),|.(k2 + l).|}

proof end;

theorem :: SCMPDS_9:16

for a being Int_position

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) >=0_goto k2),l) = {(l + 1),|.(k2 + l).|}

for l being Element of NAT

for k1, k2 being Integer holds NIC (((a,k1) >=0_goto k2),l) = {(l + 1),|.(k2 + l).|}

proof end;

registration
end;

registration
end;

registration
end;

registration

let a, b be Int_position;

let k1, k2 be Integer;

coherence

JUMP ((a,k1) := (b,k2)) is empty

end;
let k1, k2 be Integer;

coherence

JUMP ((a,k1) := (b,k2)) is empty

proof end;

registration
end;

registration

let a, b be Int_position;

let k1, k2 be Integer;

coherence

JUMP (AddTo (a,k1,b,k2)) is empty

JUMP (SubFrom (a,k1,b,k2)) is empty

JUMP (MultBy (a,k1,b,k2)) is empty

JUMP (Divide (a,k1,b,k2)) is empty

end;
let k1, k2 be Integer;

coherence

JUMP (AddTo (a,k1,b,k2)) is empty

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm3: not 5 / 3 is integer

proof end;

Lm4: for d being Real holds (((|.d.| + (((- d) + |.d.|) + 4)) + 2) - 2) + d <> - (((((|.d.| + (((- d) + |.d.|) + 4)) + (((- d) + |.d.|) + 4)) + 2) - 2) + d)

proof end;

Lm5: for b, d being Real holds b + 1 <> b + ((((- d) + |.d.|) + 4) + d)

proof end;

Lm6: for c, d being Real st c > 0 holds

(|.d.| + c) + 1 <> - (((|.d.| + c) + c) + d)

proof end;

Lm7: for b being Real

for d being Integer st d <> 5 holds

(b + (((- d) + |.d.|) + 4)) + 1 <> b + d

proof end;

Lm8: for c, d being Real st c > 0 holds

((|.d.| + c) + c) + 1 <> - ((|.d.| + c) + d)

proof end;

Lm9: for a being Int_position

for k1 being Integer holds JUMP ((a,k1) <>0_goto 5) = {}

proof end;

Lm10: for a being Int_position

for k1, k2 being Integer st k2 <> 5 holds

JUMP ((a,k1) <>0_goto k2) = {}

proof end;

Lm11: for a being Int_position

for k1 being Integer holds JUMP ((a,k1) <=0_goto 5) = {}

proof end;

Lm12: for a being Int_position

for k1, k2 being Integer st k2 <> 5 holds

JUMP ((a,k1) <=0_goto k2) = {}

proof end;

Lm13: for a being Int_position

for k1 being Integer holds JUMP ((a,k1) >=0_goto 5) = {}

proof end;

Lm14: for a being Int_position

for k1, k2 being Integer st k2 <> 5 holds

JUMP ((a,k1) >=0_goto k2) = {}

proof end;

registration

let a be Int_position;

let k1, k2 be Integer;

coherence

JUMP ((a,k1) <>0_goto k2) is empty

JUMP ((a,k1) <=0_goto k2) is empty

JUMP ((a,k1) >=0_goto k2) is empty

end;
let k1, k2 be Integer;

coherence

JUMP ((a,k1) <>0_goto k2) is empty

proof end;

coherence JUMP ((a,k1) <=0_goto k2) is empty

proof end;

coherence JUMP ((a,k1) >=0_goto k2) is empty

proof end;

registration
end;