Nuprl Definition : EquatePairs
EquatePairs(x;n;y;m) ==
pertype(λ2a b.(a = b ∈ Base)
∨ (((x = a ∈ Base) ∧ (n = b ∈ Base)) ∨ ((x = b ∈ Base) ∧ (n = a ∈ Base)))
∨ (((y = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((y = b ∈ Base) ∧ (m = a ∈ Base)))
∨ ((x = y ∈ Base) ∧ (((n = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((n = b ∈ Base) ∧ (m = a ∈ Base)))))
Definitions occuring in Statement :
pertype: pertype(R),
so_lambda: λ2x y.t[x; y],
or: P ∨ Q,
and: P ∧ Q,
base: Base,
equal: s = t ∈ T
Definitions occuring in definition :
pertype: pertype(R),
so_lambda: λ2x y.t[x; y],
or: P ∨ Q,
and: P ∧ Q,
equal: s = t ∈ T,
base: Base
FDL editor aliases :
EquatePairs
Latex:
EquatePairs(x;n;y;m) ==
pertype(\mlambda{}\msubtwo{}a b.(a = b)
\mvee{} (((x = a) \mwedge{} (n = b)) \mvee{} ((x = b) \mwedge{} (n = a)))
\mvee{} (((y = a) \mwedge{} (m = b)) \mvee{} ((y = b) \mwedge{} (m = a)))
\mvee{} ((x = y) \mwedge{} (((n = a) \mwedge{} (m = b)) \mvee{} ((n = b) \mwedge{} (m = a)))))
Date html generated:
2016_05_15-PM-03_15_39
Last ObjectModification:
2015_09_23-AM-07_42_51
Theory : general
Home
Index