### Nuprl Lemma : cubical-interval-filler_wf

`cubical-interval-filler() ∈ I:(Cname List)`
`⟶ J:(nameset(I) List)`
`⟶ x:nameset(I)`
`⟶ i:ℕ2`
`⟶ open_box(cubical-interval();I;J;x;i)`
`⟶ cubical-interval()(I)`

Proof

Definitions occuring in Statement :  cubical-interval-filler: `cubical-interval-filler()` open_box: `open_box(X;I;J;x;i)` cubical-interval: `cubical-interval()` I-cube: `X(I)` nameset: `nameset(L)` coordinate_name: `Cname` list: `T List` int_seg: `{i..j-}` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  cubical-interval-filler: `cubical-interval-filler()` member: `t ∈ T` cubical-interval: `cubical-interval()` I-cube: `X(I)` all: `∀x:A. B[x]` top: `Top` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` nameset: `nameset(L)` open_box: `open_box(X;I;J;x;i)` cons: `[a / b]` l_exists: `(∃x∈L. P[x])` int_seg: `{i..j-}` coordinate_name: `Cname` int_upper: `{i...}` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` so_lambda: `λ2x.t[x]` sq_stable: `SqStable(P)` squash: `↓T` decidable: `Dec(P)` le: `A ≤ B` so_apply: `x[s]` cand: `A c∧ B` nat: `ℕ` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` subtract: `n - m` less_than': `less_than'(a;b)` true: `True` listp: `A List+` name-morph: `name-morph(I;J)`
Lemmas referenced :  ob_pair_lemma null_wf3 subtype_rel_list top_wf bool_wf eqtt_to_assert assert_of_null eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal-wf-T-base list_wf nameset_wf open_box_wf cubical-interval_wf coordinate_name_wf int_seg_wf I-face_wf list-cases product_subtype_list reduce_hd_cons_lemma length_of_nil_lemma int_seg_properties satisfiable-full-omega-tt intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf I-cube_wf list-diff_wf cname_deq_wf cons_wf nil_wf isect_subtype_rel_trivial name-morph_wf subtype_rel-equal cubical-set_wf decidable__le le_wf face-cube_wf subtype_rel_dep_function face-dimension_wf name-morph_subtype nameset_subtype list-diff-subset subtype_rel_self hd_wf l_member_wf list-subtype listp_properties length_of_cons_lemma length_wf_nat nat_wf decidable__lt false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel less_than_wf length_wf get_face_wf extd-nameset-nil face-name_wf cubical-interval-ap_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalRule cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis isectElimination hypothesisEquality applyEquality because_Cache independent_isectElimination lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination dependent_pairFormation promote_hyp instantiate cumulativity independent_functionElimination baseClosed setElimination rename natural_numberEquality hypothesis_subsumption int_eqEquality intEquality independent_pairFormation computeAll isectEquality universeEquality functionEquality imageMemberEquality imageElimination dependent_set_memberEquality setEquality addEquality minusEquality productEquality independent_pairEquality

Latex:
cubical-interval-filler()  \mmember{}  I:(Cname  List)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  open\_box(cubical-interval();I;J;x;i)
{}\mrightarrow{}  cubical-interval()(I)

Date html generated: 2017_10_05-AM-10_26_44
Last ObjectModification: 2017_07_28-AM-11_23_01

Theory : cubical!sets

Home Index