:: SCMPDS Is Not Standard
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received September 27, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

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
proofend;
end;

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

registration
let k be Integer;
cluster JUMP (goto k) ->  empty ;
coherence
 JUMP (goto k) is empty by Lm1;
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 ) = succ (IC s) ) holds
NIC (i,l) = {(succ l)}
proofend;

theorem Th2: :: SCMPDS_9:2
for i being Instruction of SCMPDS st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds
JUMP i is empty
proofend;

theorem Th3: :: SCMPDS_9:3
for l being Element of NAT
for k being Integer holds NIC ((goto k),l) = {(abs (k + l))}
proofend;

Lm2:  for k being Nat st k > 1 holds
k - 2 is Element of NAT
proofend;

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 Element of NAT : k > 1  }
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l)}
proofend;

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) = {(succ l),(abs (k2 + l))}
proofend;

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) = {(succ l),(abs (k2 + l))}
proofend;

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) = {(succ l),(abs (k2 + l))}
proofend;

theorem Th17: :: SCMPDS_9:17
for a being Int_position holds JUMP (return a) =  {  k where k is Element of NAT : k > 1  }
proofend;

registration
let a be Int_position;
cluster JUMP (return a) ->  infinite ;
coherence
 not JUMP (return a) is finite
proofend;
end;

registration
let a be Int_position;
let k1 be Integer;
cluster JUMP (saveIC (a,k1)) ->  empty ;
coherence
 JUMP (saveIC (a,k1)) is empty
proofend;
end;

registration
let a be Int_position;
let k1 be Integer;
cluster JUMP (a := k1) ->  empty ;
coherence
 JUMP (a := k1) is empty
proofend;
end;

registration
let a be Int_position;
let k1, k2 be Integer;
cluster JUMP ((a,k1) := k2) ->  empty ;
coherence
 JUMP ((a,k1) := k2) is empty
proofend;
end;

registration
let a, b be Int_position;
let k1, k2 be Integer;
cluster JUMP ((a,k1) := (b,k2)) ->  empty ;
coherence
 JUMP ((a,k1) := (b,k2)) is empty
proofend;
end;

registration
let a be Int_position;
let k1, k2 be Integer;
cluster JUMP (AddTo (a,k1,k2)) ->  empty ;
coherence
 JUMP (AddTo (a,k1,k2)) is empty
proofend;
end;

registration
let a, b be Int_position;
let k1, k2 be Integer;
cluster JUMP (AddTo (a,k1,b,k2)) ->  empty ;
coherence
 JUMP (AddTo (a,k1,b,k2)) is empty
proofend;
cluster JUMP (SubFrom (a,k1,b,k2)) ->  empty ;
coherence
 JUMP (SubFrom (a,k1,b,k2)) is empty
proofend;
cluster JUMP (MultBy (a,k1,b,k2)) ->  empty ;
coherence
 JUMP (MultBy (a,k1,b,k2)) is empty
proofend;
cluster JUMP (Divide (a,k1,b,k2)) ->  empty ;
coherence
 JUMP (Divide (a,k1,b,k2)) is empty
proofend;
end;

Lm3:  not 5 / 3 is integer
proofend;

Lm4:  for d being real number holds ((((abs d) + (((- d) + (abs d)) + 4)) + 2) - 2) + d <> - ((((((abs d) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) + 2) - 2) + d)
proofend;

Lm5:  for b, d being real number holds b + 1 <> b + ((((- d) + (abs d)) + 4) + d)
proofend;

Lm6:  for c, d being real number st c > 0 holds
((abs d) + c) + 1 <> - ((((abs d) + c) + c) + d)
proofend;

Lm7:  for b being real number
for d being Integer st d <> 5 holds
(b + (((- d) + (abs d)) + 4)) + 1 <> b + d
proofend;

Lm8:  for c, d being real number st c > 0 holds
(((abs d) + c) + c) + 1 <> - (((abs d) + c) + d)
proofend;

Lm9:  for a being Int_position
for k1 being Integer holds JUMP ((a,k1) <>0_goto 5) = {}
proofend;

Lm10:  for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) <>0_goto k2) = {}
proofend;

Lm11:  for a being Int_position
for k1 being Integer holds JUMP ((a,k1) <=0_goto 5) = {}
proofend;

Lm12:  for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) <=0_goto k2) = {}
proofend;

Lm13:  for a being Int_position
for k1 being Integer holds JUMP ((a,k1) >=0_goto 5) = {}
proofend;

Lm14:  for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) >=0_goto k2) = {}
proofend;

registration
let a be Int_position;
let k1, k2 be Integer;
cluster JUMP ((a,k1) <>0_goto k2) ->  empty ;
coherence
 JUMP ((a,k1) <>0_goto k2) is empty
proofend;
cluster JUMP ((a,k1) <=0_goto k2) ->  empty ;
coherence
 JUMP ((a,k1) <=0_goto k2) is empty
proofend;
cluster JUMP ((a,k1) >=0_goto k2) ->  empty ;
coherence
 JUMP ((a,k1) >=0_goto k2) is empty
proofend;
end;

theorem Th18: :: SCMPDS_9:18
for l being Element of NAT holds SUCC (l,SCMPDS) = NAT
proofend;

registration
cluster SCMPDS  ->  non InsLoc-antisymmetric ;
coherence
 not SCMPDS is InsLoc-antisymmetric
proofend;
end;

registration
cluster SCMPDS  ->  non weakly_standard ;
coherence
 not SCMPDS is weakly_standard by AMI_WSTD:10;
end;