st1 
st2 == 
sub:Atom 
SimpleType. (
st-similar(st1;st-subst(sub;st2)))
Definitions occuring in Statement :
st-similar: st-similar(st1;st2),
st-subst: st-subst(subst;st),
simple_type: SimpleType,
assert: b,
exists: x:A. B[x],
function: x:A B[x],
atom: Atom
Definitions :
exists: x:A. B[x],
function: x:A B[x],
atom: Atom,
simple_type: SimpleType,
assert: b,
st-similar: st-similar(st1;st2),
st-subst: st-subst(subst;st)
FDL editor aliases :
st-instance
st1 \mleq{} st2 == \mexists{}sub:Atom {}\mrightarrow{} SimpleType. (\muparrow{}st-similar(st1;st-subst(sub;st2)))
Date html generated:
2011_08_17-PM-04_56_35
Last ObjectModification:
2011_02_07-PM-03_55_54
Home
Index