Nuprl Rule : parameterizedRecEquality

H  ⊢ pRec(C1;x1.B1;c1) = pRec(C2;x2.B2;c2) ∈ Type

  BY parameterizedRecEquality x y z c ()
     
     
  H x:(C1 ⟶ Type) ⊢ B1[x/x1] = B2[x/x2] ∈ (C1 ⟶ Type)
  H x:(C1 ⟶ Type), y:(C1 ⟶ Type), z:(∀c:C1. ((x c) ⊆r (y c))) ⊢ ∀c:C1. ((B1[x/x1] c) ⊆r (B2[y/x2] c))
  H  ⊢ C1 = C2 ∈ Type
  H  ⊢ c1 = c2 ∈ C1

Latex:
H    \mvdash{}  pRec(C1;x1.B1;c1)  =  pRec(C2;x2.B2;c2)

    BY  parameterizedRecEquality  x  y  z  c  ()
         
         
    H  x:(C1  {}\mrightarrow{}  Type)  \mvdash{}  B1[x/x1]  =  B2[x/x2]
    H  x:(C1  {}\mrightarrow{}  Type),  y:(C1  {}\mrightarrow{}  Type),  z:(\mforall{}c:C1.  ((x  c)  \msubseteq{}r  (y  c)))
          \mvdash{}  \mforall{}c:C1.  ((B1[x/x1]  c)  \msubseteq{}r  (B2[y/x2]  c))
    H    \mvdash{}  C1  =  C2
    H    \mvdash{}  c1  =  c2


Date html generated: 2019_06_20-PM-04_12_07
Last ObjectModification: 2013_10_31-PM-00_21_29

Theory : rules


Home Index