Nuprl Definition : psub
a ⊆ b ==
formula_ind(b;
pvar(v)⇒ a = pvar(v) ∈ formula();
pnot(c)⇒ r.(a = pnot(c) ∈ formula()) ∨ r;
pand(c,d)⇒ r1,r2.(a = pand(c;d) ∈ formula()) ∨ r1 ∨ r2;
por(c,d)⇒ r1,r2.(a = por(c;d) ∈ formula()) ∨ r1 ∨ r2;
pimp(c,d)⇒ r1,r2.(a = pimp(c;d) ∈ formula()) ∨ r1 ∨ r2)
Definitions occuring in Statement :
formula_ind: formula_ind,
pimp: pimp(left;right),
por: por(left;right),
pand: pand(left;right),
pnot: pnot(sub),
pvar: pvar(name),
formula: formula(),
or: P ∨ Q,
equal: s = t ∈ T
Definitions occuring in definition :
formula_ind: formula_ind,
pvar: pvar(name),
pnot: pnot(sub),
pand: pand(left;right),
por: por(left;right),
equal: s = t ∈ T,
formula: formula(),
pimp: pimp(left;right),
or: P ∨ Q
FDL editor aliases :
psub
Latex:
a \msubseteq{} b ==
formula\_ind(b;
pvar(v){}\mRightarrow{} a = pvar(v);
pnot(c){}\mRightarrow{} r.(a = pnot(c)) \mvee{} r;
pand(c,d){}\mRightarrow{} r1,r2.(a = pand(c;d)) \mvee{} r1 \mvee{} r2;
por(c,d){}\mRightarrow{} r1,r2.(a = por(c;d)) \mvee{} r1 \mvee{} r2;
pimp(c,d){}\mRightarrow{} r1,r2.(a = pimp(c;d)) \mvee{} r1 \mvee{} r2)
Date html generated:
2016_05_15-PM-07_13_03
Last ObjectModification:
2015_09_23-AM-08_13_16
Theory : general
Home
Index