environ
vocabularies HIDDEN, NUMBERS, SCMPDS_2, AMI_1, INT_1, FUNCOP_1, SUBSET_1, FSM_1, FUNCT_1, AMISTD_1, FUNCT_4, XBOOLE_0, SETFAM_1, AMI_3, COMPLEX1, ARYTM_3, XXREAL_0, ARYTM_1, CARD_1, AMI_2, RELAT_1, GRAPHSP, TARSKI, FINSET_1, CARD_3, AMI_WSTD, NAT_1, GOBRD13, MEMSTR_0, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, INT_1, NAT_1, FINSET_1, COMPLEX1, INT_2, RELAT_1, FUNCT_4, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_2, SCMPDS_2, SCMPDS_3, AMISTD_1, AMI_WSTD;
definitions TARSKI, XBOOLE_0;
theorems AMI_WSTD, SETFAM_1, SCMPDS_2, ABSVALUE, INT_1, TARSKI, AMI_2, NAT_1, FUNCT_4, PRE_CIRC, WSIERP_1, PEPIN, COMPLEX1, XREAL_1, FUNCT_7, NAT_D, AMISTD_1, MEMSTR_0, CARD_3, SCMPDS_I, XTUPLE_0, ORDINAL1;
schemes ;
registrations XREAL_0, NAT_1, INT_1, CARD_3, SCMPDS_2, FUNCT_1, FUNCT_4, MEMSTR_0, AMI_3, ORDINAL1;
constructors HIDDEN, REAL_1, NAT_D, SCMPDS_1, SCMPDS_3, AMI_WSTD, PRE_POLY, AMISTD_1, FUNCT_4, FUNCT_7;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities XBOOLE_0, NAT_1, AMISTD_1, MEMSTR_0, SCMPDS_2;
expansions TARSKI, XBOOLE_0;
Lm1:
for k being Integer holds JUMP (goto k) = {}
Lm2:
for k being Nat st k > 1 holds
k - 2 is Element of NAT
registration
let a,
b be
Int_position;
let k1,
k2 be
Integer;
coherence
JUMP (AddTo (a,k1,b,k2)) is empty
coherence
JUMP (SubFrom (a,k1,b,k2)) is empty
coherence
JUMP (MultBy (a,k1,b,k2)) is empty
coherence
JUMP (Divide (a,k1,b,k2)) is empty
end;
Lm3:
not 5 / 3 is integer
Lm4:
for d being Real holds (((|.d.| + (((- d) + |.d.|) + 4)) + 2) - 2) + d <> - (((((|.d.| + (((- d) + |.d.|) + 4)) + (((- d) + |.d.|) + 4)) + 2) - 2) + d)
Lm5:
for b, d being Real holds b + 1 <> b + ((((- d) + |.d.|) + 4) + d)
Lm6:
for c, d being Real st c > 0 holds
(|.d.| + c) + 1 <> - (((|.d.| + c) + c) + d)
Lm7:
for b being Real
for d being Integer st d <> 5 holds
(b + (((- d) + |.d.|) + 4)) + 1 <> b + d
Lm8:
for c, d being Real st c > 0 holds
((|.d.| + c) + c) + 1 <> - ((|.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 k1, k2 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 k1, k2 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 k1, k2 being Integer st k2 <> 5 holds
JUMP ((a,k1) >=0_goto k2) = {}