Nuprl Lemma : name-case_wf
∀[T:Type]. ∀[A:i:Id ⟶ {k:Knd| ↑hasloc(k;i)}  ⟶ T]. ∀[B:Id ⟶ Id ⟶ T]. ∀[n:MaName].
  (name-case(n;i,k.A[i;k];j,x.B[j;x]) ∈ T)
Proof
Definitions occuring in Statement : 
name-case: name-case(n;i,k.A[i; k];j,x.B[j; x])
, 
MaName: MaName
, 
hasloc: hasloc(k;i)
, 
Knd: Knd
, 
Id: Id
, 
assert: ↑b
, 
uall: ∀[x:A]. B[x]
, 
so_apply: x[s1;s2]
, 
member: t ∈ T
, 
set: {x:A| B[x]} 
, 
function: x:A ⟶ B[x]
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
name-case: name-case(n;i,k.A[i; k];j,x.B[j; x])
, 
MaName: MaName
, 
so_lambda: λ2x y.t[x; y]
, 
so_apply: x[s1;s2]
, 
prop: ℙ
Latex:
\mforall{}[T:Type].  \mforall{}[A:i:Id  {}\mrightarrow{}  \{k:Knd|  \muparrow{}hasloc(k;i)\}    {}\mrightarrow{}  T].  \mforall{}[B:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  T].  \mforall{}[n:MaName].
    (name-case(n;i,k.A[i;k];j,x.B[j;x])  \mmember{}  T)
Date html generated:
2016_05_16-AM-11_01_39
Last ObjectModification:
2015_12_29-AM-09_10_58
Theory : event-ordering
Home
Index