[mizar] Was it meant to be that way?

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

While playing with Patrick's incons, I have run into the following:

	:: Verifier, Mizar Ver. 6.4.02 (Linux/FPC)

     environ
     
      vocabulary CQC_LANG, ZF_MODEL, VALUAT_1;
      notation XBOOLE_0, SUBSET_1, CQC_LANG, VALUAT_1;
      constructors VALUAT_1;
      clusters RELAT_1;
     
     begin
     
     reserve X for Subset of CQC-WFF;
     reserve p for Element of CQC-WFF;
     reserve A for non empty set;
     reserve v for Element of Valuations_in A;
     reserve J for interpretation of A;
     
     definition let A,J,v,X;
       pred J,v |= X means :Def1: p in X implies J,v |= p;
     end;
     
     definition let X,p; 
       pred X |= p means :Def2:
        for A, J, v holds J,v |= X implies J,v |= p;
     end;
     
     consider X being Subset of CQC-WFF;
     consider p being Element of CQC-WFF;
     
     X |= p iff (for A, J, v holds J,v |= X implies J,v |= p) by Def2;
     
     definition let X,p; 
       pred X |= p means :Def3:
       for J, v holds J,v |= X implies J,v |= p;
     end;
     
     X |= p iff (for A, J, v holds J,v |= X implies J,v |= p) by Def3;
     
     definition let X,p; 
       pred X |= p means :Def4:
       for v holds J,v |= X implies J,v |= p;
     end;
     
     X |= p iff (for A, J, v holds J,v |= X implies J,v |= p) by Def4;
     
     definition let X,p; 
       pred X |= p means :Def5:
       J,v |= X implies J,v |= p;
     end;
     
     X |= p iff (for A, J, v holds J,v |= X implies J,v |= p) by Def5;
     ::>                                                       *4
     
     ::> 4: This inference is not accepted


Was it meant to be this way?

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr