Nuprl Lemma : AF-induction

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  (∀[Q:T ⟶ ℙ]. TI(T;x,y.¬R[x;y];t.Q[t])) supposing `
`     (AFx,y:T.R[x;y] and `
`     (∀x,y,z:T.  ((¬R[x;y]) `` (¬R[y;z]) `` (¬R[x;z]))))`

Proof

Definitions occuring in Statement :  almost-full: `AFx,y:T.R[x; y]` TI: `TI(T;x,y.R[x; y];t.Q[t])` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` not: `¬A` false: `False` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` prop: `ℙ` almost-full: `AFx,y:T.R[x; y]` squash: `↓T` TI: `TI(T;x,y.R[x; y];t.Q[t])` so_lambda: `λ2x y.t[x; y]` consistent-seq: `R-consistent-seq(n)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` seq-add: `s.x@n` AF-spread-law: `AF-spread-law(x,y.R[x; y])` isl: `isl(x)` outl: `outl(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` and: `P ∧ Q` cand: `A c∧ B` true: `True` bfalse: `ff` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` lelt: `i ≤ j < k` le: `A ≤ B` decidable: `Dec(P)` less_than': `less_than'(a;b)` subtract: `n - m` sq_stable: `SqStable(P)` top: `Top` less_than: `a < b`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination applyEquality functionExtensionality cumulativity hypothesis universeEquality extract_by_obid isectElimination rename imageElimination imageMemberEquality baseClosed functionEquality lambdaFormation because_Cache unionEquality equalityTransitivity equalitySymmetry setEquality setElimination inlEquality independent_functionElimination dependent_set_memberEquality unionElimination equalityElimination productElimination independent_isectElimination int_eqReduceTrueSq natural_numberEquality independent_pairFormation dependent_pairFormation promote_hyp instantiate intEquality impliesFunctionality int_eqReduceFalseSq addEquality minusEquality isect_memberEquality voidEquality productEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(\mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  TI(T;x,y.\mneg{}R[x;y];t.Q[t]))  supposing
(AFx,y:T.R[x;y]  and
(\mforall{}x,y,z:T.    ((\mneg{}R[x;y])  {}\mRightarrow{}  (\mneg{}R[y;z])  {}\mRightarrow{}  (\mneg{}R[x;z]))))

Date html generated: 2017_04_14-AM-07_27_57
Last ObjectModification: 2017_02_27-PM-02_57_29

Theory : bar-induction

Home Index