Nuprl Lemma : fpf-union-compatible-property

    ∀[X:T ⟶ Type]
      ∀R:(V List) ⟶ V ⟶ 𝔹
        (∀A,B,C:t:T fp-> X[t] List.
            fpf-union-compatible(T;V;t.X[t];eq;R;C;fpf-union-join(eq;R;A;B)))) supposing 
           ((∀L1,L2:V List. ∀x:V.  (↑(R (L1 L2) x)) supposing ((↑(R L2 x)) and (↑(R L1 x)))) and 
           (∀L1,L2:V List. ∀x:V.  (L1 ⊆ L2  ↑(R L1 x) supposing ↑(R L2 x)))) 
      supposing ∀t:T. (X[t] ⊆V)


Definitions occuring in Statement :  fpf-union-join: fpf-union-join(eq;R;f;g) fpf-union-compatible: fpf-union-compatible(A;C;x.B[x];eq;R;f;g) fpf: a:A fp-> B[a] l_contains: A ⊆ B append: as bs list: List deq: EqDecider(T) assert: b bool: 𝔹 uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] implies:  Q apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] uimplies: supposing a member: t ∈ T subtype_rel: A ⊆B implies:  Q fpf-union-compatible: fpf-union-compatible(A;C;x.B[x];eq;R;f;g) so_lambda: λ2x.t[x] so_apply: x[s] top: Top iff: ⇐⇒ Q and: P ∧ Q or: P ∨ Q istype: istype(T) prop: not: ¬A false: False fpf-union: fpf-union(f;g;eq;R;x) fpf-cap: f(x)?z bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) band: p ∧b q ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b cand: c∧ B respects-equality: respects-equality(S;T) rev_implies:  Q true: True decidable: Dec(P) l_contains: A ⊆ B
Lemmas referenced :  assert_witness append_wf fpf-union-join-dom subtype-fpf2 list_wf top_wf istype-void l_member_wf fpf-ap_wf fpf-union-join_wf subtype_rel_dep_function bool_wf subtype_rel_list istype-assert fpf-dom_wf fpf-union-compatible_wf fpf_wf l_contains_wf subtype_rel_wf deq_wf istype-universe eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot fpf-union-join-ap member_append filter_wf5 member_filter subtype-respects-equality subtype_rel_transitivity assert_elim decidable__assert l_all_iff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction sqequalRule sqequalHypSubstitution lambdaEquality_alt dependent_functionElimination thin hypothesisEquality axiomEquality hypothesis functionIsTypeImplies inhabitedIsType rename isect_memberEquality_alt isectElimination extract_by_obid applyEquality independent_functionElimination isectIsTypeImplies independent_isectElimination voidElimination universeIsType because_Cache productElimination unionIsType productIsType functionEquality functionIsType isectIsType instantiate universeEquality unionElimination equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation_alt equalityIstype promote_hyp cumulativity setEquality setIsType setElimination inlFormation_alt inrFormation_alt independent_pairFormation dependent_set_memberEquality_alt applyLambdaEquality natural_numberEquality

        \mforall{}[X:T  {}\mrightarrow{}  Type]
            \mforall{}R:(V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}
                (\mforall{}A,B,C:t:T  fp->  X[t]  List.
                      {}\mRightarrow{}  fpf-union-compatible(T;V;t.X[t];eq;R;C;A)
                      {}\mRightarrow{}  fpf-union-compatible(T;V;t.X[t];eq;R;C;B)
                      {}\mRightarrow{}  fpf-union-compatible(T;V;t.X[t];eq;R;C;fpf-union-join(eq;R;A;B))))  supposing 
                      ((\mforall{}L1,L2:V  List.  \mforall{}x:V.    (\muparrow{}(R  (L1  @  L2)  x))  supposing  ((\muparrow{}(R  L2  x))  and  (\muparrow{}(R  L1  x))))  and 
                      (\mforall{}L1,L2:V  List.  \mforall{}x:V.    (L1  \msubseteq{}  L2  {}\mRightarrow{}  \muparrow{}(R  L1  x)  supposing  \muparrow{}(R  L2  x)))) 
            supposing  \mforall{}t:T.  (X[t]  \msubseteq{}r  V)

Date html generated: 2019_10_16-AM-11_25_47
Last ObjectModification: 2019_06_25-PM-01_23_02

Theory : finite!partial!functions

Home Index