Nuprl Lemma : decide-spread-sq1

[x:Top × Top]. ∀[f,g,h:Top].  (case let a,b in inl f[a;b] of inl(z) => g[z] inr(z) => h[z] g[f[fst(x);snd(x)]])


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] pi1: fst(t) pi2: snd(t) spread: spread def product: x:A × B[x] decide: case of inl(x) => s[x] inr(y) => t[y] inl: inl x sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T pi1: fst(t) pi2: snd(t)
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut productElimination thin sqequalRule sqequalAxiom lemma_by_obid hypothesis sqequalHypSubstitution isect_memberEquality isectElimination hypothesisEquality because_Cache productEquality

Latex:
\mforall{}[x:Top  \mtimes{}  Top].  \mforall{}[f,g,h:Top].
    (case  let  a,b  =  x  in  inl  f[a;b]  of  inl(z)  =>  g[z]  |  inr(z)  =>  h[z]  \msim{}  g[f[fst(x);snd(x)]])



Date html generated: 2016_05_15-PM-03_25_02
Last ObjectModification: 2015_12_27-PM-01_06_23

Theory : general


Home Index