### Nuprl Lemma : id-graph-edge_wf

`∀[S:Id List]. ∀[G:Graph(S)]. ∀[i:{i:Id| (i ∈ S)} ]. ∀[j:Id].  ((i⟶j)∈G ∈ ℙ)`

Proof

Definitions occuring in Statement :  id-graph-edge: `(i⟶j)∈G` id-graph: `Graph(S)` Id: `Id` l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` set: `{x:A| B[x]} `
Definitions unfolded in proof :  id-graph-edge: `(i⟶j)∈G` uall: `∀[x:A]. B[x]` member: `t ∈ T` id-graph: `Graph(S)` subtype_rel: `A ⊆r B` prop: `ℙ` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  l_member_wf Id_wf subtype_rel_list set_wf id-graph_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality applyEquality setEquality independent_isectElimination lambdaEquality setElimination rename because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[S:Id  List].  \mforall{}[G:Graph(S)].  \mforall{}[i:\{i:Id|  (i  \mmember{}  S)\}  ].  \mforall{}[j:Id].    ((i{}\mrightarrow{}j)\mmember{}G  \mmember{}  \mBbbP{})

Date html generated: 2016_05_14-PM-03_37_45
Last ObjectModification: 2015_12_26-PM-05_58_56

Theory : decidable!equality

Home Index