### Nuprl Lemma : fun-path-before

`∀[T:Type]. ∀f:T ⟶ T. ∀L:T List. ∀x,y,a,b:T.  a before b ∈ L `` a is f*(b) supposing x=f*(y) via L`

Proof

Definitions occuring in Statement :  fun-connected: `y is f*(x)` fun-path: `y=f*(x) via L` l_before: `x before y ∈ l` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` prop: `ℙ` implies: `P `` Q` so_apply: `x[s]` fun-path: `y=f*(x) via L` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` subtract: `n - m` and: `P ∧ Q` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` false: `False` not: `¬A` int_seg: `{i..j-}` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` uiff: `uiff(P;Q)` iff: `P `⇐⇒` Q` cons: `[a / b]` nat_plus: `ℕ+` true: `True` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` cand: `A c∧ B` nat: `ℕ` le: `A ≤ B`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity because_Cache functionExtensionality applyEquality hypothesis functionEquality independent_functionElimination rename dependent_functionElimination universeEquality baseClosed independent_isectElimination isect_memberEquality voidElimination voidEquality productElimination independent_pairEquality imageElimination axiomEquality productEquality natural_numberEquality minusEquality equalityTransitivity equalitySymmetry addEquality setElimination unionElimination dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll pointwiseFunctionality promote_hyp baseApply closedConclusion hypothesis_subsumption dependent_set_memberEquality imageMemberEquality applyLambdaEquality inrFormation inlFormation

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}L:T  List.  \mforall{}x,y,a,b:T.    a  before  b  \mmember{}  L  {}\mRightarrow{}  a  is  f*(b)  supposing  x=f*(y)  via  L

Date html generated: 2018_05_21-PM-07_46_23
Last ObjectModification: 2017_07_26-PM-05_23_51

Theory : general

Home Index