Nuprl Definition : axiom def

Ax ==  PRIMITIVE


Rules referencing :  imageEquality,  imageMemberEquality,  imageEqInduction,  universeEquality,  addCommutative,  addZero,  addInverse,  addAssociative,  multiplyCommutative,  multiplyOne,  multiplyAssociative,  multiplyDistributive,  addMonotonic,  lessDiscrete,  lessTrichotomy,  multiplyPositive,  atomEquality,  tokenEquality,  atom_eqEquality,  voidEquality,  intEquality,  natural_numberEquality,  minusEquality,  addEquality,  multiplyEquality,  divideEquality,  remainderEquality,  remainderBounds1,  remainderBounds2,  remainderBounds3,  remainderBounds4,  divideRemainderSum,  intWeakElimination,  int_eqEquality,  unionEquality,  inlFormation,  inrFormation,  inlEquality,  inrEquality,  decideEquality,  functionEquality,  lambdaFormation,  lambdaEquality,  dependent_functionElimination,  applyEquality,  functionExtensionality,  productEquality,  dependent_pairFormation,  dependent_pairEquality,  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,  computationStep,  computeAll,  extract_by_obid,  equalitySymmetry,  equalityTransitivity,  exceptionNotBottom,  exceptionNotAxiom,  because_Cache,  because_SupInf,  barInduction,  bar_Induction,  strong_bar_Induction,  Continuity,  StrongContinuity2,  divergentSqle,  divergentSqlen,  compactness,  isintReduceTrue,  isatomReduceTrue,  isAtom2ReduceTrue,  isAtom1ReduceTrue,  isintReduceAtom,  isectEquality,  isect_memberFormation,  isect_memberEquality,  isect_member_caseEquality,  isectElimination,  independent_isectElimination,  classicalIntroduction,  pointwiseFunctionality,  pointwiseFunctionality wrename,  hypothesis_subsumption,  sqequalAxiom,  axiomSqleEquality,  axiomSqleNEquality,  sqequalElimination,  sqequalnReflexivity,  sqequal_n rule,  sqle_n rule,  sqntypeEquality,  sqntypeIntro,  sqntypeDef,  sqlenSubtypeRel,  sqequalZero,  sqleZero,  sqequalDefinition,  sqequalSqle,  sqequalnSqlen,  sqlenSqequaln,  sqequalnSymm,  sqleDefinition,  sqequalReflexivity,  sqequalTransitivity,  sqleReflexivity,  sqleTransitivity,  sqequalBase,  sqequalSubstitution,  sqequalHypSubstitution,  sqequalExtensionalEquality,  sqequalIntensionalEquality,  sqleExtensionalEquality,  sqleIntensionalEquality,  sqlenIntensionalEquality,  sqequalnIntensionalEquality,  int_eqReduceTrueSq,  int_eqReduceFalseSq,  atomn_eqReduceTrueSq,  atom_eqReduceTrueSq,  atomn_eqReduceFalseSq,  atom_eqReduceFalseSq,  fixpointLeast,  atomnEquality,  token1Equality,  token2Equality,  atomn_eqEquality,  baseAtomn,  freeFromAtomEquality,  freeFromAtomTriviality,  freeFromAtomBase,  freeFromAtom1Atom2,  freeFromAtomApplication,  freeFromAtomSet,  freeFromAtomAxiom,  callbyvalueReduce,  cutEval,  callbyvalueInt,  callbyvalueAtom1,  callbyvalueAtom2,  callbyvalueAtom,  callbyvalueType,  callbyvalueAdd,  callbyvalueMultiply,  callbyvalueDivide,  callbyvalueRemainder,  callbyvalueMinus,  callbyvalueLess,  callbyvalueIntEq,  callbyvalueAtomEq,  callbyvalueAtomnEq,  callbyvalueApply,  tryReduceValue,  sqleLambda,  applyPair,  applyInl,  applyInr,  applyInt,  callbyvalueCallbyvalue,  callbyvalueSpread,  callbyvalueDecide,  callbyvalueIspair,  callbyvalueIsaxiom,  callbyvalueIsinl,  callbyvalueIsinr,  callbyvalueIslambda,  callbyvalueIsint,  callbyvalueIsatom,  callbyvalueIsatom1,  callbyvalueIsatom2,  exceptionSqequal,  exceptionLess,  exceptionInteq,  exceptionAtomeq,  exceptionAtomeq1,  exceptionAtomeq2,  exceptionAdd,  exceptionMultiply,  exceptionDivide,  exceptionRemainder,  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,  ispairCases,  isintCases,  isatomCases,  isaxiomCases,  islambdaCases,  isinlCases,  isinrCases,  isatom1Cases,  isatom2Cases,  lessCases,  bottomDivergent,  pertypeEquality,  pertypeMemberEquality,  pertypeElimination,  perfunctionExtensionality,  dependentIntersectionEquality,  dependentIntersectionElimination,  dependentIntersectionEqElimination,  dependentIntersection_memberEquality,  existsFunctionality,  allLevelFunctionality,  uallLevelFunctionality,  existsLevelFunctionality,  andLevelFunctionality,  orLevelFunctionality,  orFunctionality,  impliesFunctionality,  impliesLevelFunctionality
Latex:
Ax  ==    PRIMITIVE


Date html generated: 2016_05_13-PM-03_03_30
Last ObjectModification: 2006_01_26-PM-03_39_41

Theory : core_1


Home Index