Nuprl Lemma : sq-stable-coW-game-legal1

[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])].  ∀p,q:Pos(coW-game(a.B[a];w;w')).  SqStable(Legal1(p;q))


Proof




Definitions occuring in Statement :  coW-game: coW-game(a.B[a];w;w') coW: coW(A;a.B[a]) sg-legal1: Legal1(x;y) sg-pos: Pos(g) sq_stable: SqStable(P) uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] sq_stable: SqStable(P) implies:  Q coW-game: coW-game(a.B[a];w;w') sg-legal1: Legal1(x;y) pi2: snd(t) pi1: fst(t) sg-pos: Pos(g) member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B nat: decidable: Dec(P) or: P ∨ Q squash: T and: P ∧ Q cand: c∧ B uiff: uiff(P;Q) uimplies: supposing a guard: {T} subtract: m top: Top le: A ≤ B not: ¬A less_than': less_than'(a;b) true: True false: False
Lemmas referenced :  squash_wf sg-legal1_wf coW-game_wf sg-pos_wf coW_wf decidable__int_equal copath-length_wf nat_wf sq_stable__copathAgree equal_wf le_antisymmetry_iff condition-implies-le minus-add minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero add-associates add-commutes le-add-cancel copathAgree_wf copath_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution sqequalRule productElimination thin cut introduction extract_by_obid isectElimination hypothesisEquality lambdaEquality applyEquality hypothesis instantiate cumulativity functionEquality universeEquality dependent_functionElimination setElimination rename addEquality because_Cache natural_numberEquality unionElimination imageElimination inlFormation independent_pairFormation independent_functionElimination promote_hyp equalitySymmetry hyp_replacement applyLambdaEquality intEquality independent_isectElimination isect_memberEquality voidElimination voidEquality minusEquality multiplyEquality imageMemberEquality baseClosed productEquality inrFormation

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w,w':coW(A;a.B[a])].
    \mforall{}p,q:Pos(coW-game(a.B[a];w;w')).    SqStable(Legal1(p;q))



Date html generated: 2019_06_20-PM-00_57_46
Last ObjectModification: 2019_01_02-PM-01_34_27

Theory : co-recursion-2


Home Index