### Nuprl Lemma : complete_nat_measure_ind

`∀[T:Type]. ∀[measure:T ⟶ ℕ]. ∀[P:T ⟶ ℙ].`
`  ((∀i:T. ((∀j:{j:T| measure[j] < measure[i]} . P[j]) `` P[i])) `` (∀i:T. P[i]))`

Proof

Definitions occuring in Statement :  nat: `ℕ` less_than: `a < b` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` genrec: genrec nat: `ℕ` false: `False` ge: `i ≥ j ` guard: `{T}` uimplies: `b supposing a` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` not: `¬A` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` exists: `∃x:A. B[x]` sq_type: `SQType(T)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction lambdaEquality cut extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality sqequalRule functionEquality setEquality because_Cache applyEquality functionExtensionality hypothesis lambdaFormation setElimination rename universeEquality intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination dependent_functionElimination axiomEquality unionElimination independent_pairFormation productElimination addEquality isect_memberEquality voidEquality intEquality minusEquality equalityTransitivity equalitySymmetry dependent_pairFormation sqequalIntensionalEquality promote_hyp applyLambdaEquality instantiate

Latex:
\mforall{}[T:Type].  \mforall{}[measure:T  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}i:T.  ((\mforall{}j:\{j:T|  measure[j]  <  measure[i]\}  .  P[j])  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:T.  P[i]))

Date html generated: 2017_04_14-AM-07_32_42
Last ObjectModification: 2017_02_27-PM-03_07_25

Theory : int_1

Home Index