Bug: Enter bug title here

I was able to deduce contradiction using the latest version of verifier.

Test case

Gmy_struct1 Gmy_struct2 Gmy_struct3 Gmy_struct4 Umy_selec1 Mmy_mode1 Omy_func1

environ

vocabularies MEMBERED, MY_VOC, ARYTM, INT_1, ARYTM_1, ARYTM_3, SUBSET_1, TARSKI ,SQUARE_1, MATRIX_2, ORDINAL2, FILTER_0, ABSVALUE, NAT_1, ORDINAL1, XREAL_0, BOOLE, SUPINF_1; notations XXREAL_0, ZFMISC_1, ORDINAL1, XCMPLX_0, SUBSET_1, XBOOLE_0, TARSKI, INT_1, INT_2, NAT_1, SQUARE_1, PEPIN, ABIAN, ABSVALUE, NUMBERS, XREAL_0,NAT_D, MEMBERED; constructors XXREAL_0, ZFMISC_1, ORDINAL1, XCMPLX_0, NAT_1, XBOOLE_0, TARSKI, INT_1, INT_2, SQUARE_1, PEPIN, ABIAN, ABSVALUE, NUMBERS, XREAL_0, NAT_D, MEMBERED; registrations XCMPLX_0, XREAL_0, SQUARE_1, PEPIN, NAT_1, INT_1, INT_2, ABIAN, ORDINAL1, XXREAL_0, REAL_1, ZFMISC_1, MEMBERED, XBOOLE_0; requirements SUBSET, NUMERALS, ARITHM, BOOLE; theorems XCMPLX_1, SQUARE_1, ABIAN, INT_1, INT_2, ABSVALUE, NAT_1, NAT_D, SUBSET_1, ZFMISC_1, XBOOLE_1, MEMBERED;

begin

definition let h be set; mode my_mode1 of h means :D0: it=h; existence; end;

definition let x be set; struct my_struct1 over x (# my_selec1 -> my_mode1 of x#); end;

definition let x,y be set; struct (my_struct1 over x\y) my_struct2 over x,y (#my_selec1 -> my_mode1 of x\y#); end;

definition let x,y be set; struct (my_struct1 over y\x) my_struct3 over x,y (#my_selec1 -> my_mode1 of y\x#); end;

definition let x,y be set; struct (my_struct3 over x,y, my_struct2 over x,y) my_struct4 over x,y (# my_selec1 -> my_mode1 of y\x#); end;

definition let x,y be set; let z be my_struct2 over x,y; func my_func1 z -> my_struct1 over x\y equals :d2: z; coherence; end;

L1: now let x,y be set; let k be my_mode1 of y\x; set h = my_struct4(#k#); L1: the my_selec1 of my_func1(h) is my_mode1 of x\y; L2: my_func1(h)=h by d2; L3: the my_selec1 of h = k; thus k is my_mode1 of x\y by L1,L2,L3; end;

L2: for x,y being set holds x\y=y\x proof let x,y be set; consider z being my_mode1 of x\y; z is my_mode1 of y\x by L1; then L2: z = y\x by D0; z = x\y by D0; hence thesis by L2; end;

L3: contradiction proof consider x being non empty set; x\{}={}\x by L2; then x={} by XBOOLE_1:32; hence thesis; end;

L4: 2+2=5 by L3;

Environment

-- SergeS - 2009-05-29

Follow up

Fix record

Thanks for the bug report. The relevant type checks have been restored to raise the error *92 in the analyzer in such cases. The fix created by Czesław Byliński is incorporated into:

-- AdamNaumowicz - 2009-06-18