Nuprl Definition : equal def
s = t ∈ T == PRIMITIVE
Rules referencing :
imageEquality,
imageMemberEquality,
imageEqInduction,
universeEquality,
addCommutative,
addZero,
addInverse,
addAssociative,
multiplyCommutative,
multiplyOne,
multiplyAssociative,
multiplyDistributive,
addMonotonic,
lessDiscrete,
lessTrichotomy,
atomEquality,
tokenEquality,
atom_eqEquality,
voidEquality,
intEquality,
natural_numberEquality,
minusEquality,
addEquality,
multiplyEquality,
divideEquality,
remainderEquality,
divideRemainderSum,
intWeakElimination,
int_eqEquality,
unionEquality,
inlFormation,
inrFormation,
inlEquality,
inrEquality,
decideEquality,
functionEquality,
lambdaFormation,
lambdaEquality,
dependent_functionElimination,
functionUniverseElim,
applyEquality,
functionExtensionality,
productEquality,
dependent_pairFormation,
dependent_pairEquality,
productUniverseElim,
spreadEquality,
lessEquality,
independent_pairEquality,
setEquality,
dependent_set_memberFormation,
dependent_set_memberEquality,
equalityUniverse,
equalityEquality,
equalityEqualityBase,
baseEquality,
baseInt,
baseAtom,
axiomEquality,
equalityElimination,
hypothesisEquality,
levelHypothesis,
addLevel,
pointwiseFunctionalityForEquality,
introduction,
substitution,
hyp_replacement,
cumulativity,
extract_by_obid,
equalitySymmetry,
equalityTransitivity,
Continuity,
StrongContinuity2,
isintReduceTrue,
isatomReduceTrue,
isAtom2ReduceTrue,
isAtom1ReduceTrue,
isintReduceAtom,
isectEquality,
isect_memberFormation,
isect_memberEquality,
isect_member_caseEquality,
isectElimination,
classicalIntroduction,
pointwiseFunctionality,
pointwiseFunctionality wrename,
sqequalAxiom,
axiomSqleEquality,
axiomSqleNEquality,
sqequalnReflexivity,
sqntypeEquality,
sqntypeIntro,
sqntypeDef,
sqlenSubtypeRel,
sqequalBase,
sqequalExtensionalEquality,
sqequalIntensionalEquality,
sqleExtensionalEquality,
sqleIntensionalEquality,
sqlenIntensionalEquality,
sqequalnIntensionalEquality,
int_eqReduceTrueSq,
int_eqReduceFalseSq,
atomn_eqReduceTrueSq,
atom_eqReduceTrueSq,
atomn_eqReduceFalseSq,
atom_eqReduceFalseSq,
atomnEquality,
token1Equality,
token2Equality,
atomn_eqEquality,
baseAtomn,
freeFromAtomEquality,
freeFromAtomTriviality,
freeFromAtomBase,
freeFromAtomAxiom,
ispairExceptionCases,
isintExceptionCases,
isaxiomExceptionCases,
isatomExceptionCases,
isinlExceptionCases,
isinrExceptionCases,
islambdaExceptionCases,
isatom1ExceptionCases,
isatom2ExceptionCases,
decideExceptionCases,
spreadExceptionCases,
minusExceptionCases,
applyExceptionCases,
int_eqExceptionCases,
lessExceptionCases,
atom_eqExceptionCases,
atom1_eqExceptionCases,
atom2_eqExceptionCases,
addExceptionCases,
divideExceptionCases,
remainderExceptionCases,
multiplyExceptionCases,
callbyvalueExceptionCases,
pertypeEquality,
pertypeMemberEquality,
pertypeElimination,
perfunctionExtensionality,
dependentIntersectionEquality,
dependentIntersectionElimination,
dependentIntersectionEqElimination,
dependentIntersection_memberEquality
Latex:
s = t == PRIMITIVE
Date html generated:
2016_05_13-PM-03_03_30
Last ObjectModification:
2006_01_26-PM-03_41_54
Theory : core_1
Home
Index