environ
vocabularies HIDDEN, NUMBERS, NAT_1, FINSEQ_2, MARGREL1, SUBSET_1, FINSEQ_1, PARTFUN1, RELAT_1, FUNCT_1, FUNCOP_1, XBOOLEAN, ARYTM_3, INT_1, BINARITH, ARYTM_1, POWER, ORDINAL4, CARD_1, TARSKI, BINOP_2, SETWISEO, BINARI_2, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, NUMBERS, FUNCT_1, NAT_1, NAT_D, INT_1, PARTFUN1, BINOP_1, SETWOP_2, SERIES_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, BINOP_2, XBOOLEAN, MARGREL1, BINARITH;
definitions ;
theorems BINARITH, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCOP_1, POWER, NAT_1, FINSOP_1, BINOP_2, XBOOLEAN, PARTFUN1, XREAL_0, CARD_1;
schemes FINSEQ_2, NAT_1;
registrations ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, BINOP_2, XBOOLEAN, MARGREL1, FINSEQ_2, CARD_1;
constructors HIDDEN, PARTFUN1, BINOP_1, SETWISEO, XXREAL_0, NAT_1, INT_1, FINSEQ_4, FINSOP_1, SERIES_1, BINARITH, BINOP_2, NAT_D, RELSET_1, TREES_3, FUNCOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLEAN;
expansions ;
Lm1:
for n being Nat
for p, q being Tuple of n, BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) holds
p = q
definition
let n be
Nat;
existence
ex b1 being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ (i,1,TRUE,FALSE)
uniqueness
for b1, b2 being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ (i,1,TRUE,FALSE) ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ (i,1,TRUE,FALSE) ) holds
b1 = b2
end;
theorem Th11:
for
m being non
zero Nat for
z1,
z2 being
Tuple of
m,
BOOLEAN for
d1,
d2 being
Element of
BOOLEAN holds
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ ((Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1))))) - (IFEQ ((Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1)))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
theorem Th12:
for
m being non
zero Nat for
z1,
z2 being
Tuple of
m,
BOOLEAN for
d1,
d2 being
Element of
BOOLEAN holds
Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = (((Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))) - (IFEQ ((Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1))))
theorem
for
m being non
zero Nat for
z1,
z2 being
Tuple of
m,
BOOLEAN for
d1,
d2 being
Element of
BOOLEAN holds
(((Intval ((z1 ^ <*d1*>) - (z2 ^ <*d2*>))) + (IFEQ ((Int_add_ovfl ((z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>)))),FALSE,0,(2 to_power (m + 1))))) - (IFEQ ((Int_add_udfl ((z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>)))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_ovfl (('not' (z2 ^ <*d2*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = (Intval (z1 ^ <*d1*>)) - (Intval (z2 ^ <*d2*>))