[mizar] Proving inequality of structs ?

[Greg Frascadore <gfrascadore@qwest.net>]

    Hello,  I could use a little help with my understanding of
    Mizar structs and strict. 
    
    My current understanding is based on "Some Features of the Mizar
    Language" by Trybulec. I've also seen the long email thread 
    for Jesse Alama <http://www.nabble.com/strict-to8243464.html>
    concerning strict.
    
    Here is my question:
    
    reserve x for set;
    reserve t for Subset-Family of x;
    reserve o for 1-sorted;
    reserve s for TopStruct;
    
    s = TopStruct(# x, t #) & o = 1-sorted(# x #) implies
        the 1-sorted of s = o;                          :: I understand
        
    s is TopStruct & o is strict 1-sorted implies
        s <> o;                                        
             *4
     
    :: If o is strict, it lacks the 'topology' selector. How to
    :: test that? maybe:
    
    s = TopStruct(# x, t #) & o = 1-sorted(# x #) implies
        s <> o;                                         
             *4                                         :: now what?
    
    TopStruct(# x, t #) <> 1-sorted(# x #);
                                         *4             :: confused
                                         
    Also, what is 'forgetful' about the 'forgetful constructor' ?
    
    Thanks for any insight.
    
    -Greg Frascadore


-- 
View this message in context: http://www.nabble.com/Proving-inequality-of-structs---tp21459576p21459576.html
Sent from the Mizar mailing list archive at Nabble.com.