:: SCMPDS Is Not Standard
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received September 27, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem Def1 defines locnum SCMPDS_9:def 1 :
theorem :: SCMPDS_9:1
canceled;
theorem :: SCMPDS_9:2
canceled;
theorem Th3: :: SCMPDS_9:3
theorem :: SCMPDS_9:4
theorem :: SCMPDS_9:5
canceled;
theorem :: SCMPDS_9:6
canceled;
theorem Th7: :: SCMPDS_9:7
theorem Th8: :: SCMPDS_9:8
theorem Th9: :: SCMPDS_9:9
Lm1:
for k being natural number st k > 1 holds
k - 2 is Element of NAT
theorem Th10: :: SCMPDS_9:10
theorem Th11: :: SCMPDS_9:11
theorem Th12: :: SCMPDS_9:12
theorem Th13: :: SCMPDS_9:13
theorem Th14: :: SCMPDS_9:14
theorem Th15: :: SCMPDS_9:15
theorem Th16: :: SCMPDS_9:16
theorem Th17: :: SCMPDS_9:17
theorem Th18: :: SCMPDS_9:18
theorem Th19: :: SCMPDS_9:19
theorem :: SCMPDS_9:20
theorem :: SCMPDS_9:21
theorem :: SCMPDS_9:22
Lm2:
for k being Integer holds JUMP (goto k) = {}
theorem Th23: :: SCMPDS_9:23
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
cluster JUMP (SubFrom a,k1,b,k2) -> empty ;
coherence
JUMP (SubFrom a,k1,b,k2) is empty
cluster JUMP (MultBy a,k1,b,k2) -> empty ;
coherence
JUMP (MultBy a,k1,b,k2) is empty
cluster JUMP (Divide a,k1,b,k2) -> empty ;
coherence
JUMP (Divide a,k1,b,k2) is empty
end;
Lm3:
not 5 / 3 is integer
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)
Lm5:
for b, d being real number holds b + 1 <> b + ((((- d) + (abs d)) + 4) + d)
Lm6:
for c, d being real number st c > 0 holds
((abs d) + c) + 1 <> - ((((abs d) + c) + c) + d)
Lm7:
for b being real number
for d being Integer st d <> 5 holds
(b + (((- d) + (abs d)) + 4)) + 1 <> b + d
Lm8:
for c, d being real number st c > 0 holds
(((abs d) + c) + c) + 1 <> - (((abs d) + c) + d)
Lm9:
for a being Int_position
for k1 being Integer holds JUMP (a,k1 <>0_goto 5) = {}
Lm10:
for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP (a,k1 <>0_goto k2) = {}
Lm11:
for a being Int_position
for k1 being Integer holds JUMP (a,k1 <=0_goto 5) = {}
Lm12:
for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP (a,k1 <=0_goto k2) = {}
Lm13:
for a being Int_position
for k1 being Integer holds JUMP (a,k1 >=0_goto 5) = {}
Lm14:
for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP (a,k1 >=0_goto k2) = {}
theorem Th24: :: SCMPDS_9:24