Nuprl Lemma : causal_order_wf

[T:Type]. ∀[L:T List]. ∀[P,Q:ℕ||L|| ⟶ ℙ]. ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ].  (causal_order(L;R;P;Q) ∈ ℙ)


Proof




Definitions occuring in Statement :  causal_order: causal_order(L;R;P;Q) length: ||as|| list: List int_seg: {i..j-} uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T causal_order: causal_order(L;R;P;Q) so_lambda: λ2x.t[x] implies:  Q prop: and: P ∧ Q int_seg: {i..j-} subtype_rel: A ⊆B so_apply: x[s]
Lemmas referenced :  all_wf int_seg_wf length_wf exists_wf le_wf subtype_rel_self list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesisEquality hypothesis lambdaEquality functionEquality applyEquality productEquality setElimination rename instantiate universeEquality because_Cache axiomEquality equalityTransitivity equalitySymmetry functionIsType universeIsType inhabitedIsType isect_memberEquality cumulativity

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P,Q:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}].    (causal\_order(L;R;P;Q)  \mmember{}  \mBbbP{})



Date html generated: 2019_10_15-AM-10_57_31
Last ObjectModification: 2018_09_27-AM-09_37_30

Theory : list!


Home Index