<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
// A proof of strong normalization for System F based on Girard's
// notion of reducibility candidates.

// Kevin Donnelly and Hongwei Xi (May 2006)

// This is a proof based on Girard's method of reducibility candidates

// definition of sort 'tm' of HOAS terms
datasort tm =
  | TMcst
  | TMlam of (tm -> tm)
  | TMapp of (tm, tm)

// neutral terms
dataprop NEU (tm) =
  | NEUcst (TMcst)
  | {t1:tm, t2:tm} NEUapp (TMapp (t1, t2))

// small-step reduction
dataprop RED (tm, tm, int) =
  | {f:tm->tm, f':tm->tm, n:nat}
      REDlam (TMlam f, TMlam f', n+1) of {x:tm} RED (f x, f' x, n)

  | {t1:tm,t2:tm,t1':tm, s:nat}
      REDapp1 (TMapp (t1, t2), TMapp (t1', t2), s+1) of RED (t1, t1', s)

  | {t1:tm,t2:tm,t2':tm, s:nat}
      REDapp2 (TMapp (t1, t2), TMapp (t1, t2'), s+1) of (RED (t2, t2', s))

  | {f:tm->tm,t:tm} REDapp3 (TMapp (TMlam f, t), f t, 0)

propdef RED0 (t:tm, t':tm) = [s:nat] RED (t, t', s)

(* Strong Normalization *)
dataprop SN(tm, int) =
  | {t:tm, n:nat} SN(t,n) of 
      {t':tm} (RED0(t, t') -> [n':nat | n' < n] SN(t',n'))

propdef SN0 (t:tm) = [n:nat] SN(t, n)

// SN is closed under reduction
prfun forwardSN {t:tm, t':tm, n:nat} .< >.
  (sn:SN(t, n), red:RED0(t, t')) : [n':nat | n' < n] SN(t', n') =
  let prval SN fsn = sn in fsn red end

// sort for predicates on terms
sortdef rc = tm -> prop

(* Reducibility Candidates *)
propdef CR1 (R: rc) = {t:tm} R t -> SN0 t

propdef CR2 (R: rc) = {t:tm, t':tm} (R t, RED0 (t, t')) -> R t'

propdef CR3 (R: rc) = {t:tm} (NEU t, {t':tm} RED0 (t, t') -> R t') -> R t

propdef RC (R: rc) = '(CR1 R, CR2 R, CR3 R)

prfn sn_is_cr1 (): CR1 (SN0) = lam sn => sn

prfn sn_is_cr2 (): CR2 (SN0) = lam (sn, rd) => let prval SN fsn = sn in fsn rd end

// this follows from the fact that any term has a finite number of reductions
// easy to see this is true, but complicated to formally prove
dynprf backwardSN: {t:tm} ({t':tm} RED0 (t, t') -> SN0 t') -> SN0 t

prfn sn_is_cr3 (): CR3 (SN0) = lam (_, fsn) => backwardSN fsn

prval sn_is_rc: RC (SN0) = '(sn_is_cr1 (), sn_is_cr2 (), sn_is_cr3 ())

//

prfn cr_cst {R:tm->prop} (rc:RC(R)) : R(TMcst) =
  let 
     prval '(_, _, cr3) = rc
     prfn redsR {t':tm} (red:RED0(TMcst, t')) : R(t') =
       (case* red of REDapp3() => '())
  in
     cr3(NEUcst, redsR)
  end

//

// lifting of -> to candidates
dataprop RCFUN (rc, rc, tm) =
  {R1:rc, R2:rc, t:tm} 
    RCFUN (R1, R2, t) of {t1: tm} R1 t1 -> R2 (TMapp (t, t1))

propdef RCFUN0 (R1: rc, R2: rc) (t:tm) = RCFUN (R1, R2, t)

prfun appSNlemma {t:tm, t1:tm, n:nat} .<n>. 
      (sn:SN(TMapp(t, t1), n)) : [n':nat | n' <= n] SN(t, n') =
  let
     prval SN(redsSNapp) = sn
     prfn redsSNt {t':tm} (red:RED0(t, t')) : [n':nat | n' < n] SN(t', n') =
          appSNlemma(redsSNapp (REDapp1 red))
  in
     SN{t,n}(redsSNt)
  end

// R1 -> R2 is a candidate if R1 and R2 is
prfn rcfun_is_rc {R1:rc, R2:rc} (rc1:RC R1, rc2:RC R2): RC (RCFUN0 (R1, R2)) =
  let
     prval '(cr11, cr21, cr31) = rc1
     prval '(cr12, cr22, cr32) = rc2
     prfn rcfun_is_cr1 {t:tm} (rcfun : RCFUN0(R1, R2)(t)) 
            : SN0(t) =
       let
          prval RCFUN(rcf) = rcfun
          prval r2 = rcf (cr_cst rc1)
          prval sn2 = cr12 r2
          prval sn = appSNlemma(sn2)
       in
          sn
       end
     prfn rcfun_is_cr2 {t:tm, t':tm} 
          (rcfun : RCFUN0(R1, R2)(t), 
           red   : RED0(t, t'))
            : RCFUN0(R1,R2)(t') =
       let
          prval RCFUN(rcf) = rcfun
          prfn rcf' {t1:tm} (r1:R1(t1)) : R2(TMapp(t', t1)) =
               cr22(rcf r1, REDapp1(red))       
       in
          RCFUN(rcf')
       end 
     prfn rcfun_is_cr3 {t:tm} 
          (neu    : NEU t,
           rcfunf : {t':tm} (RED0(t, t') -> RCFUN0(R1, R2)(t')))
            : RCFUN0(R1, R2)(t) =
       let
          // cr1 holds for R1 so we can argue by induction on SN bound (mu)
          prfun rcfsn {t1:tm, n:nat} .<n>.
                (r1  : R1(t1),
                 sn1 : SN(t1, n)) 
                  : R2(TMapp(t, t1)) = 
            let
               prfn rcf' {t':tm} (red:RED0(TMapp(t, t1), t'))
                         : R2(t') = case* red of
                  | REDapp1(red1) => 
                    let 
                       prval RCFUN(rcf1) = rcfunf(red1)
                    in
                       rcf1 r1
                    end
                  | REDapp2(red2) =>
                    let
                       prval r1' = cr21 (r1, red2)
                       prval sn1' = forwardSN(sn1, red2)
                    in
                       rcfsn(r1', sn1')
                    end
                  | REDapp3() => 
                    (case* neu of NEUcst() => '())
            in
               cr32(NEUapp, rcf')
            end
          prfn rcf {t1:tm} (r1:R1(t1)) : R2(TMapp(t, t1)) =
               let 
                  prval sn1 = cr11 r1
               in
                  rcfsn (r1, sn1)
               end
       in
          RCFUN(rcf)
       end
  in
     '(rcfun_is_cr1, rcfun_is_cr2, rcfun_is_cr3)
  end

//

// lifting of forall to candidates
dataprop RCALL (rc -> rc, tm) =
  {RF: rc -> rc, t:tm}
    RCALL (RF, t) of {R: rc} RC R -> RF R t

propdef RCALL0 (RF: rc -> rc) (t:tm) = RCALL (RF, t)

// forall RF is a candidate if RF R is a candidate whenever R is
prfn rcall_is_rc {RF:rc -> rc} (rcrfrf: {R : rc} RC R -> RC (RF R)) : RC (RCALL0 RF) =
  let
     prfn rcall_is_cr1 {t:tm} (rcall : RCALL0(RF)(t)) 
            : SN0(t) =
       let
          prval RCALL(rfrf) = rcall
          prval rfsn = rfrf{SN0}(sn_is_rc)
          prval rcrfsn = rcrfrf{SN0}(sn_is_rc)
          prval '(cr1, _, _) = rcrfsn
       in
          cr1 rfsn
       end
     prfn rcall_is_cr2 {t:tm, t':tm} 
          (rcall : RCALL0(RF)(t), 
           red   : RED0(t, t'))
            : RCALL0(RF)(t') =
       let
          prfn rcf {R : rc} (rc : RC R) : RF(R)(t') =
               let
                  prval RCALL(rfrf) = rcall
                  prval rfr = rfrf{R}(rc)
                  prval rc' = rcrfrf{R}(rc)
                  prval '(_, cr2, _) = rc'
               in 
                  cr2(rfr,red)
               end
       in
          RCALL(rcf)
       end 
     prfn rcall_is_cr3 {t:tm} 
          (neu    : NEU t,
           rcallf : {t':tm} (RED0(t, t') -> RCALL0(RF)(t')))
            : RCALL0(RF)(t) =
        let
           prfn rcf {R : rc} (rc : RC R) : (RF R)(t) =
                let
                   prfn rcf' {t':tm} (red:RED0(t, t'))
                          : (RF R)(t') = 
                        let
                           prval RCALL(rfrf) = rcallf red
                           prval rfr = rfrf{R}(rc)
                        in 
                           rfr                              
                        end
                   prval rc' = rcrfrf{R}(rc)
                   prval '(_, _, cr3) = rc'
                in
                   cr3 (neu, rcf')
                end
        in
           RCALL(rcf)
        end
  in
     '(rcall_is_cr1, rcall_is_cr2, rcall_is_cr3)
  end

// lam f : R1 -> R2 if R1, R2 are candidates and 
// for all terms t, R1 t implies R2 (f t)
prfn abs_lemma {R1:rc, R2:rc, f:tm->tm} 
      (rc1 : RC R1, 
       rc2 : RC R2,
       rcf : ({t:tm} R1 t -> R2 (f t)))
        : RCFUN0 (R1, R2) (TMlam f) =
  let
     prval '(cr11, cr21, cr31) = rc1
     prval '(cr12, cr22, cr32) = rc2
     // since R1, R2 are candidates, we can argue by induction on the sum
     // of the SN bounds
     prfun rfr_aux  {t1:tm, n:nat, m:nat, f:tm->tm} .<n+m>.
           (r1  : R1(t1),
            sn1 : SN(t1, n),
            sn2 : SN(f TMcst, m),
            rcf : ({t:tm} R1 t -> R2 (f t)))
             : R2(TMapp(TMlam f, t1)) =
       let
          // each reduction of (lam f) t1 results in t' such that R2 t'
          prfn fr2 {t':tm} (red:RED0(TMapp(TMlam f, t1), t'))
                 : R2(t') = case* red of
             | REDapp1(REDlam{f, f', _}(redf)) =>
               let
                  prfn rcf' {t:tm} (r1 : R1(t)) : R2(f' t) =
                       cr22(rcf(r1), redf{t})
               in
                  rfr_aux(r1, sn1, forwardSN(sn2, redf{TMcst}), rcf')
               end
             | REDapp2(red2) =>
               rfr_aux (cr21(r1, red2), forwardSN(sn1, red2), sn2, rcf)
             | REDapp3() => rcf(r1)
       in
          // since cr3 holds of R2, we know R2 ((lam f) t1)
          cr32 (NEUapp, fr2)
       end
     prfn rfr {t1:tm} (r1:R1(t1)) : R2(TMapp(TMlam f, t1)) =
          rfr_aux(r1, cr11(r1), cr12(rcf(cr_cst(rc1))), rcf)
  in
     RCFUN(rfr)
  end

// definition of sort 'tp' of FOAS types
datasort tp =
  | TPvar of int // type variable
  | TPfun of (tp, tp) // T1 -> T2
  | TPall of (tp) // forall X. T

// sequence of candidates (this plays double duty as a candidate context for
// type interpretation and as a bound on the deBruijn indices in derivations)
datasort rcs = RCSnil
             | RCScons of (rc, rcs)

// type context lookup
dataprop RCSI(rcs, rc, int) =
  | {R:rc, C:rcs} 
      RCSIone(RCScons(R, C), R, 0)
  | {R:rc, R':rc, C:rcs, n:nat}
      RCSIshi(RCScons(R', C), R, n + 1) of RCSI(C, R, n)

propdef RCSI0(C:rcs, R:rc) = [n:nat] RCSI(C, R, n)

// typing interpretations
dataprop TPI(rcs, tp, rc, int) =
  | {C:rcs, T:tp, R:rc, n:nat}
      TPIvar(C, TPvar n, R, 0) of (RCSI(C, R, n))
  | {C:rcs, T1:tp, T2:tp, R1:rc, R2:rc, n1:nat, n2:nat}
      TPIfun(C, TPfun(T1, T2), RCFUN0(R1,R2), n1+n2+1) of
        (TPI(C, T1, R1, n1), TPI(C, T2, R2, n2))
  | {C:rcs, T:tp, RF:rc->rc, n:nat}
      TPIall(C, TPall(T), RCALL0(RF), n+1) of
        ({R:rc} TPI(RCScons(R, C), T, RF R, n))

propdef TPI0(C:rcs, T:tp, R:rc) = [n:nat] TPI(C, T, R, n)

// prop for equality of predicates on terms
dataprop RCEQ(rc, rc) = 
    {R:rc} RCEQ(R, R)

// prop for proofs that a sequence of predicates is a sequence of candidates
dataprop RCS(rcs, int) =
  |   RCSnil(RCSnil, 0)
  | {R:rc, C:rcs, n:nat} 
      RCScons(RCScons(R, C), n+1) of (RC R, RCS(C, n))

propdef RCS0 (C: rcs) = [n:nat] RCS (C, n)

// lookup proof that a predicate is a candidate
prfun getRC {R:rc, C:rcs, n:nat} .<n>.
      (rcsi : RCSI(C, R, n), rcs : RCS0 C) : RC R = case* rcsi of
  | RCSIone() =>
    (case* rcs of
    | RCScons(rc, rcs') => rc)
  | RCSIshi(rcsi') =>
    (case* rcs of
    | RCScons(rc, rcs') => getRC(rcsi', rcs'))

// the interpretation of a type, under an assignment of candidates to type
// variables, is a candidate
prfun tpi_is_rc {C:rcs, T:tp, R:rc, n:nat} .<n>.
      (rcs: RCS0 C, tpi: TPI(C, T, R, n)): RC(R) = case* tpi of
  | TPIvar(inr) => getRC(inr, rcs)
  | TPIfun(tpi1, tpi2) => 
    rcfun_is_rc(tpi_is_rc(rcs, tpi1), tpi_is_rc(rcs, tpi2))
  | TPIall{_, F, RF, _}(tpif) => 
    let
       prfn rcf {R1:rc} (rc:RC(R1)) : RC(RF R1) =
            tpi_is_rc(RCScons(rc, rcs), tpif)
    in
       rcall_is_rc(rcf)
    end

// contexts/typed-substitutions
datasort ctx = CTXnil
             | CTXcons of (tm, tp, ctx)

// dynamic representation for types, the index rcs is used only as a bound
// on deBruijn indices, note that R in the var case is arbitrary
dataprop TP(rcs, tp, int) =
  | {C:rcs, T:tp, R:rc, n:nat}
      TPvar(C, TPvar n, 0) of RCSI(C, R, n)
  | {T1:tp, T2:tp, n1:nat, n2:nat, C:rcs}
      TPfun(C, TPfun(T1, T2), n1+n2+1) of 
        (TP(C, T1, n1), TP(C, T2, n2))
  | {T:tp, n:nat, C:rcs}
      TPall(C, TPall T, n+1) of 
        ({R:rc} TP(RCScons(R, C), T, n))

propdef TP0(C:rcs, T:tp) = [n:nat] TP(C, T, n)

// INCTX(t, T, G, n) encodes (t : T) in G at position n
dataprop INCTX(tm, tp, ctx, int) =
  | {t:tm, T:tp, G:ctx} 
      INCTXone(t, T, CTXcons(t, T, G), 0)
  | {t:tm, t':tm, T:tp, T':tp, G:ctx, n:nat}
      INCTXshi(t, T, CTXcons(t', T', G), n+1) of
        INCTX(t, T, G, n)

// (t : T) in G
propdef INCTX0(t:tm, T:tp, G:ctx) = [n:nat] INCTX(t, T, G, n)

// list of types, serves as a substitution for deBruijn indices
datasort tps = TPSnil | TPScons of (tp, tps)

// TPSHI(T, T', i) means T' is T with deBruijn indices >= i shifted up one
dataprop TPSHI (tp, tp, int) =
  | {i:nat, l:nat | i >= l} TPSHIvargte (TPvar i, TPvar (i+1), l)

  | {i:nat, l:nat | i < l} TPSHIvarlt (TPvar i, TPvar i, l)

  | {T:tp, T':tp, l:nat}
      TPSHIall (TPall T, TPall T', l) of TPSHI (T, T', l+1)

  | {T1:tp, T2:tp, T1':tp, T2':tp, l:nat}
      TPSHIfun (TPfun(T1, T2), TPfun(T1', T2'), l) of
        (TPSHI(T1, T1', l), TPSHI(T2, T2', l))

// shift all terms in a context
dataprop SHICTX(ctx, ctx, int) =
  |   SHICTXnil(CTXnil, CTXnil, 0)
  | {t:tm, T:tp, T':tp, G:ctx, G':ctx, n:nat}
      SHICTXcons(CTXcons(t, T, G), CTXcons(t, T', G'), n+1) of
        (TPSHI(T, T', 0), SHICTX(G, G', n))

propdef SHICTX0(G:ctx, G':ctx) = [n:nat] SHICTX(G, G', n)

// shift all indices in the types in a substitution
dataprop SUBSTSHI (tps, tps) =
  | SUBSTSHInil (TPSnil, TPSnil)
  | {S:tps, S':tps, T:tp, T':tp}
      SUBSTSHImore (TPScons (T, S), TPScons (T', S')) of
        (SUBSTSHI (S, S'), TPSHI (T, T', 0))

// INTPS(T, S, i) means T is at index i in substitution S
dataprop INTPS(tp, tps, int) =
  | {T:tp, S:tps} 
      INTPSone(T, TPScons(T, S), 0)
  | {T:tp, T':tp, S:tps, n:nat}
      INTPSshi(T, TPScons(T', S), n+1) of INTPS(T, S, n)

// dynamic representation of substitutions
dataprop TPS(rcs, tps, int) =
  | {C:rcs}
      TPSnil(C, TPSnil, 0)
  | {C:rcs, T:tp, S:tps, n:nat, m:nat}
      TPScons(C, TPScons(T, S), n+1) of (TP(C, T, m), TPS(C, S, n))

// sequence of type interpretations
dataprop TPIS(rcs, tps, rcs, int) = 
  | {C:rcs}
      TPISnil(C, TPSnil, RCSnil, 0)
  | {C:rcs, T:tp, S:tps, RS:rcs, R:rc, n:nat}
      TPIScons(C, TPScons(T, S), RCScons(R, RS), n+1) of 
        (TPI0(C, T, R), TPIS(C, S, RS, n))

// substitution on types
dataprop SUBST(tp, int, tp, tp, int) =
  | {T:tp, n:nat} 
      SUBSTvar_eq(T, n, TPvar n, T, 0)
  | {T:tp, n:nat, m:nat | m < n}
      SUBSTvar_gt(T, m, TPvar n, TPvar (n-1), 0)
  | {T:tp, n:nat, m:nat | m > n}
      SUBSTvar_lt(T, m, TPvar n, TPvar n, 0)
  | {T:tp, T1:tp, T2:tp, T1':tp, T2':tp, n1:nat, n2:nat, m:nat}
      SUBSTfun(T, m, TPfun(T1, T2), TPfun(T1', T2'), n1+n2+1) of
        (SUBST(T, m, T1, T1', n1), SUBST(T, m, T2, T2', n2))
  | {T:tp, T':tp, T1:tp, T1':tp, m:nat}
      SUBSTall(T, m, TPall(T1), TPall(T1'), m+1) of
        (SUBST(T', m+1, T1, T1', m), TPSHI(T, T', 0))

// substitute into first index
propdef SUBST0(T2:tp, T1:tp, T1':tp) = [n:nat] SUBST(T2, 0, T1, T1', n)

// typing derivations
dataprop DER(rcs, ctx, tm, tp, int) =
  | {C:rcs, G:ctx, t:tm, T:tp, n:nat}
      DERvar(C, G, t, T, 0) of (INCTX(t, T, G, n), TP0(C, T))

  | {C:rcs, G:ctx, t1:tm, t2:tm, T1:tp, T2:tp, n1:nat, n2:nat}
      DERapp(C, G, TMapp(t1, t2), T2, n1+n2+1) of
        (DER(C, G, t1, TPfun(T1, T2), n1), DER(C, G, t2, T1, n2))

  | {C:rcs, G:ctx, f:tm->tm, T1:tp, T2:tp, n:nat}
      DERlam(C, G, TMlam(f), TPfun(T1, T2), n+1) of
        (TP0(C, T1), {x:tm} DER(C, CTXcons(x, T1, G), f x, T2, n))

  | {C:rcs, G:ctx, G':ctx, t:tm, T:tp, n:nat, m:nat}
      DERtabs(C, G, t, TPall(T), n+1) of 
        ({R:rc} DER(RCScons(R, C), G', t, T, n), SHICTX(G, G', m))

  | {C:rcs, G:ctx, t:tm, T1:tp, T2:tp, T:tp, n:nat}
      DERtapp(C, G, t, T, n+1) of 
        (DER(C, G, t, TPall(T1), n), TP0(C, T2), SUBST0(T2, T1, T))

propdef DER0(C:rcs, G:ctx, t:tm, T:tp) = [n:nat] DER(C, G, t, T, n)

// insert a predicate into a list of predicates at a given position
dataprop RCSINS(rcs, rc, rcs, int) = 
  | {C:rcs, C':rcs, R:rc} 
      RCSINSone(C, R, RCScons(R, C), 0)
  | {C:rcs, C':rcs, R:rc, R':rc, n:nat}
      RCSINSshi(RCScons(R, C), R', RCScons(R, C'), n+1) of 
        RCSINS(C, R', C', n)

// environments, which interpret contexts, provide proofs that each term
// in a context is in the candidate that interprets its given type
dataprop ETA(rcs, ctx, int) =
  | {C:rcs} 
      ETAnil(C, CTXnil, 0)
  | {C:rcs, t:tm, T:tp, G:ctx, R:rc, n:nat, m:nat}
      ETAcons(C, CTXcons(t, T, G), n+1) of
        (TPI(C, T, R, m), R(t), ETA(C, G, n))

// lookup a term in an environment, getting a proof that the term is in the
// appropriate candidate
prfun getR {C:rcs, G:ctx, n:nat, t:tm, T:tp, m:nat} .<n>.
      (eta : ETA(C, G, n),
       inc : INCTX(t, T, G, m))
        : [R:rc] '(TPI0(C, T, R), R(t)) = case* eta of
  | ETAnil() =/=> (case* inc of INCTXone() => '(eta, inc))
  | ETAcons(tpi, r, eta') =>
    (case* inc of
    | INCTXone() => '(tpi, r)
    | INCTXshi(inc') => getR(eta', inc'))

(* weakening on type interpretations *)
// shift a variable after the insertion point
prfun rcsi_gte {C:rcs, C':rcs, R:rc, R':rc, n:nat, m:nat | n >= m} .<m>.
      (rcsi : RCSI(C, R, n), rcsins : RCSINS(C, R', C', m))
        : RCSI(C', R, n+1) = case* rcsins of
  | RCSINSone() => RCSIshi(rcsi)
  | RCSINSshi(rcsins') =>
    let
       prval RCSIshi(rcsi') = rcsi
    in
       RCSIshi(rcsi_gte(rcsi', rcsins'))
    end

// don't shift a variable before the insertion point
prfun rcsi_lt {C:rcs, C':rcs, R:rc, R':rc, n:nat, m:nat | n < m} .<m>.
      (rcsi : RCSI(C, R, n), rcsins : RCSINS(C, R', C', m))
        : RCSI(C', R, n) = case* rcsins of
  | RCSINSshi(rcsins') =>
    (case* rcsi of
    | RCSIone() => RCSIone()
    | RCSIshi(rcsi') => RCSIshi(rcsi_lt(rcsi', rcsins')))

// shift a type at an insertion point
prfun shi_tpi {C:rcs, C':rcs, T:tp, T':tp, R:rc, R':rc, n:nat, m:nat} .<n>.
       (tpi    : TPI(C, T, R, n), 
        tpshi  : TPSHI(T, T', m), 
        rcsins : RCSINS(C, R', C', m)) 
         : TPI(C', T', R, n) = case* tpi of
  | TPIvar(rcsi) => 
    (case* tpshi of
    | TPSHIvargte() => TPIvar(rcsi_gte(rcsi, rcsins))
    | TPSHIvarlt() => TPIvar(rcsi_lt(rcsi, rcsins)))
  | TPIfun(tpi1, tpi2) =>
    let
       prval TPSHIfun(tpshi1, tpshi2) = tpshi
       prval tpi1' = shi_tpi(tpi1, tpshi1, rcsins)
       prval tpi2' = shi_tpi(tpi2, tpshi2, rcsins)
    in
       TPIfun(tpi1', tpi2')
    end
  | TPIall(tpif) =>
    let
       prval TPSHIall(tpshi') = tpshi
    in
       TPIall(lam {R:rc} => shi_tpi(tpif{R}, tpshi', RCSINSshi(rcsins)))
    end

// unshift a variable after the insertion point
prfun rcsi_unshi_gt {C:rcs, C':rcs, R:rc, R':rc, n:nat, m:nat | n > m} .<m>.
      (rcsi : RCSI(C', R, n), rcsins : RCSINS(C, R', C', m))
        : RCSI(C, R, n-1) = case* rcsins of
  | RCSINSone() => 
    let
       prval RCSIshi(rcsi') = rcsi
    in
       rcsi'
    end
  | RCSINSshi(rcsins') =>
    let
       prval RCSIshi(rcsi') = rcsi
    in
       RCSIshi(rcsi_unshi_gt(rcsi', rcsins'))
    end

// unshift context of a variable before the insertion point
prfun rcsi_unshi_lt {C:rcs, C':rcs, R:rc, R':rc, n:nat, m:nat | n < m} .<m>.
      (rcsi : RCSI(C', R, n), rcsins : RCSINS(C, R', C', m))
        : RCSI(C, R, n) = case* rcsins of
  | RCSINSshi(rcsins') =>
    (case* rcsi of
    | RCSIone() => RCSIone()
    | RCSIshi(rcsi') => RCSIshi(rcsi_unshi_lt(rcsi', rcsins')))

prfun tpi_insert {C:rcs, C':rcs, n:nat, R:rc, R':rc} .<n>.
      (tpi : TPI0(C', TPvar n, R),
       ins : RCSINS(C, R', C', n)) : RCEQ(R, R') = case* ins of
  | RCSINSone() =>
    let
       prval TPIvar(RCSIone()) = tpi
    in
       RCEQ()
    end
  | RCSINSshi(ins') =>
    let
       prval TPIvar(RCSIshi(rcsi)) = tpi
    in
       tpi_insert(TPIvar(rcsi), ins')
    end

// substitution on type interpretations
prfun tpi_subst {C:rcs, S:tps, T:tp, T1:tp, T2:tp, R:rc, 
                 R':rc, RS:rcs, C':rcs, m:nat, n1:nat, n2:nat, l:nat} .<m>.
      (sub   : SUBST(T2, n1, T1, T, n2),
       tpi2 : TPI(C, T2, R, l),
       ins   : RCSINS(C, R, C', n1),
       tpi1 : TPI(C', T1, R', m))
        : TPI0(C, T, R') = case* tpi1 of
    | TPIvar(rcsi) => 
      (case* sub of 
      | SUBSTvar_eq() => 
        let
           prval RCEQ() = tpi_insert(tpi1, ins)
        in
           tpi2
        end
      | SUBSTvar_lt() => TPIvar(rcsi_unshi_lt(rcsi, ins))
      | SUBSTvar_gt() => TPIvar(rcsi_unshi_gt(rcsi, ins)))
    | TPIfun(tpi1', tpi2') =>
      let
         prval SUBSTfun(sub1, sub2) = sub
         prval tpi1'' = tpi_subst(sub1, tpi2, ins, tpi1')
         prval tpi2'' = tpi_subst(sub2, tpi2, ins, tpi2')
      in
         TPIfun(tpi1'', tpi2'')
      end
    | TPIall(tpf) =>
      let
         prval SUBSTall(sub', tpshi) = sub
      in
         TPIall(lam {R:rc} => 
                    tpi_subst(sub', shi_tpi(tpi2, tpshi, 
                              RCSINSone()), RCSINSshi ins, tpf{R}))
      end

// we will prove substitution on types using substitution on type 
// interpretations, first we show that TP(C, T, n) only needs the length of C
dataprop RCSALTER(rcs, rc, rc, rcs, int) =
  | {R:rc, C:rcs, R':rc}
      RCSALTERone(RCScons(R, C), R, R', RCScons(R',C), 0)
  | {R:rc, C:rcs, R1:rc, R1':rc, C':rcs, n:nat}
      RCSALTERshi(RCScons(R, C), R1, R1', RCScons(R, C'), n+1) of
        RCSALTER(C, R1, R1', C', n)
  
// the exact identity of the R's is irrelevent to TP
prfun tp_rcs_arbitrary {R:rc, R':rc, C:rcs, C':rcs, T:tp, m:nat, n:nat} .<m>.
      (tp  : TP(C, T, m),
       alt : RCSALTER(C, R, R', C', n))
    : TP(C', T, m) = case* tp of
  | TPvar(rcsi) =>
    let
       prfun var_aux {C:rcs, R:rc, C':rcs, R1:rc, R1':rc, n:nat, m:nat} .<n>.
             (rcsi : RCSI(C, R, n),
              alt  : RCSALTER(C, R1, R1', C', m)) : [R:rc] RCSI(C', R, n) = 
         case* alt of
         | RCSALTERone() => 
           (case* rcsi of
           | RCSIone() => RCSIone()
           | RCSIshi(rcsi) => RCSIshi(rcsi))
         | RCSALTERshi(alt') =>
           (case* rcsi of
           | RCSIone() => RCSIone()
           | RCSIshi(rcsi') => RCSIshi(var_aux(rcsi', alt')))
       prval #[R:rc] rcsi' = var_aux(rcsi, alt)
    in
       TPvar(rcsi')
    end
  | TPfun(tp1, tp2) => 
    TPfun(tp_rcs_arbitrary (tp1, alt), tp_rcs_arbitrary (tp2, alt))
  | TPall(tpf) => 
    TPall(lam {R:rc} => tp_rcs_arbitrary(tpf{R}, RCSALTERshi(alt)))

// need higher-order pattern matching for this
dynprf hopat_lift : {C:rcs, m:nat, T:tp} 
         ({R:rc} [R':rc] TPI(RCScons(R, C), T, R', m))
           -> [RF:rc->rc] {R:rc} TPI(RCScons(R, C), T, RF R, m)

prfun tp_to_tpi {C:rcs, T:tp, n:nat} .<n>.
      (tp : TP(C, T, n))
        : [R:rc] TPI(C, T, R, n) = case* tp of
  | TPvar(inr) => TPIvar(inr)
  | TPfun(tp1, tp2) => TPIfun(tp_to_tpi(tp1), tp_to_tpi(tp2))
  | TPall(tpf) =>
    let
       prval tpif = hopat_lift(lam {R:rc} => tp_to_tpi(tpf{R}))
    in
       TPIall(tpif)
    end

// the structure of TPI is the same as TPI
prfun tpi_to_tp {C:rcs, T:tp, R:rc, n:nat} .<n>.
       (tpi : TPI(C, T, R, n)) : TP(C, T, n) = case* tpi of
  | TPIvar(rcsi) => TPvar(rcsi)
  | TPIfun(tpi1, tpi2) => TPfun(tpi_to_tp tpi1, tpi_to_tp tpi2)
  | TPIall(tpif) => TPall(lam {R:rc} => tpi_to_tp(tpif{R}))

// substitution on TPI subsumes substitution on TP
prfn tp_subst {C:rcs, T:tp, T1:tp, T2:tp, R:rc, m:nat}
      (sub : SUBST0(T2, T1, T),
       tp2 : TP0(C, T2),
       tp1 : TP(RCScons(R, C), T1, m))
        : TP0(C, T) = 
  let
     prval #[R':rc] tpi2 = tp_to_tpi(tp2)
     prval tp1' = tp_rcs_arbitrary(tp1, RCSALTERone{R, C, R'}())
     prval tpi1 = tp_to_tpi(tp1')
  in
     tpi_to_tp (tpi_subst (sub, tpi2, RCSINSone(), tpi1))
  end

// derivations determine the type in the typing judgment
prfun der_to_tp {C:rcs, G:ctx, t:tm, T:tp, n:nat} .<n>.
      (der : DER(C, G, t, T, n)) : [m:nat] TP(C, T, m) = case* der of
    | DERvar(inc, tp) => tp
    | DERapp(der1, der2) =>
      let
         prval TPfun(tp1, tp2) = der_to_tp(der1)
      in
         tp2
      end
    | DERlam(tp, derf) => TPfun(tp, der_to_tp(derf))
    | DERtabs(dertf, ctxshi) => TPall(lam {R:rc} => der_to_tp(dertf{R}))
    | DERtapp(der', tp, sub) => 
      let
         prval TPall(dertf) = der_to_tp(der')
      in
         tp_subst(sub, tp, dertf)
      end

// shift an environment
prfun shi_eta {R:rc, C:rcs, C':rcs, G:ctx, G':ctx, m:nat, n:nat} .<m>.
      (eta: ETA(C, G, m), shi: SHICTX(G, G', n)) 
        : ETA(RCScons(R, C), G', m) = case* eta of
  | ETAnil() =>
    let
       prval SHICTXnil() = shi
    in
       ETAnil()
    end
  | ETAcons(tpi, r, eta') => 
    let
       prval SHICTXcons(shitp, shi') = shi
    in
       ETAcons(shi_tpi(tpi, shitp, RCSINSone()), r, shi_eta(eta', shi'))
    end

// we need higher-order pattern matching to prove this
dynprf rceq_eta_contract : {RF:rc->rc, RF':rc->rc, n:nat, m:nat} 
         ({X:rc} RCEQ(RF X, RF' X)) -> RCEQ(RCALL0(RF), RCALL0(RF'))

// RCSI is a partial function from the first and third index to the second
prfun rcsi_functional {C:rcs, R:rc, R':rc, n:nat} .<n>.
      (rcsi1 : RCSI(C, R, n),
       rcsi2 : RCSI(C, R', n))
        : RCEQ(R, R') = case* (rcsi1,rcsi2) of
  | (RCSIone(), RCSIone()) => RCEQ()
  | (RCSIshi(rcsi1'), RCSIshi(rcsi2')) => rcsi_functional(rcsi1', rcsi2')

// TPI is a partial function from the first 2 indices to the second 2
prfun tpi_functional {C:rcs, T:tp, R:rc, R':rc, n:nat, m:nat} .<n>.
      (tpi1 : TPI(C, T, R, n),
       tpi2 : TPI(C, T, R', m))
        : [n == m] RCEQ(R, R') = case* tpi1 of
  | TPIvar(rcsi1) =>
    let
       prval TPIvar(rcsi2) = tpi2
    in
       rcsi_functional(rcsi1, rcsi2)
    end
  | TPIfun(tpi11, tpi12) =>
    let
       prval TPIfun(tpi21, tpi22) = tpi2
       prval RCEQ() = tpi_functional(tpi11, tpi21)
       prval RCEQ() = tpi_functional(tpi12, tpi22)
    in
       RCEQ()
    end
  | TPIall{_, _, RF, n1}(ftpi1) =>
    let
       prval TPIall{_, _, RF', n2}(ftpi2) = tpi2
       prval frceq = lam {X:rc} => tpi_functional(ftpi1{X}, ftpi2{X})
       prval rceq = rceq_eta_contract{RF, RF', n1, n2}(frceq)

    in
       rceq
    end

// main lemma for reducibility candidates
prfun der_rc_lemma {G:ctx, t:tm, T:tp, n:nat, C:rcs, m:nat} .<n>.
      (der : DER(C, G, t, T, n),
       eta : ETA(C, G, m),
       rcs : RCS0 C)
    : [R:rc] '(TPI0(C, T, R), R(t)) = case* der of
  | DERvar(inctx, tp) => getR(eta, inctx)

  | DERapp(der1, der2) =>
    let
       prval '(tpif, r1) = der_rc_lemma(der1, eta, rcs)
       prval '(tpi, r2) = der_rc_lemma(der2, eta, rcs)
       prval TPIfun(tpi1, tpi2) = tpif
       prval RCFUN(rcf) = r1
       prval RCEQ() = tpi_functional(tpi, tpi1)
    in
       '(tpi2, rcf r2)
    end

  | DERlam{_, _, f, _, _, _}(tp, derf) =>
    let
       prval tpi = tp_to_tpi(der_to_tp(der))
       prval TPIfun{_, _, _, R1, R2, _, _}(tpi1, tpi2) = tpi
       prval rc1 = tpi_is_rc(rcs, tpi1)
       prval rc2 = tpi_is_rc(rcs, tpi2)
       prfn rcimp {t:tm} (r1:R1(t)) : R2(f t) =
            let
               prval '(tpi2', r2) = der_rc_lemma(derf{t},
                                             ETAcons(tpi1, r1, eta),
                                             rcs)
               prval RCEQ() = tpi_functional(tpi2, tpi2')
            in
               r2
            end
    in
       '(tpi, abs_lemma(rc1, rc2, rcimp))
    end

  | DERtabs(dertf, ctxshi) => 
    let
       prval tpi = tp_to_tpi(der_to_tp(der))
       prval TPIall{_, _, RF, _}(tpif) = tpi
       prfn rcf {R:rc} (rc: RC R) : (RF R t) =
         let
            prval rcs' = RCScons(rc, rcs)
            prval eta' = shi_eta(eta, ctxshi)
            prval '(tpi1, rfr) = der_rc_lemma(dertf{R}, eta', rcs')
            prval RCEQ() = tpi_functional(tpi1, tpif{R})
         in
            rfr
         end
    in
       '(tpi, RCALL(rcf))
    end

  | DERtapp{C, G, t, T1, T2, T, n}(derall, tp, subst) =>
    let
       prval #[R:rc] tpi = tp_to_tpi(tp)
       prval '(tpiall, rcall) = der_rc_lemma(derall, eta, rcs)
       prval TPIall(tpif) = tpiall
       prval RCALL(rcf) = rcall
       prval rc = tpi_is_rc(rcs, tpi)
       prval tpi' = tpi_subst(subst, tpi, RCSINSone(), tpif{R})
    in
       '(tpi', rcf rc)
    end

// all terms with a type in the empty context are in the interpretation of
// the type assigned given
prfn der_rc {t:tm, T:tp} (der : DER0(RCSnil, CTXnil, t, T)) 
   : [R:rc] '(TPI0(RCSnil, T, R), R(t)) =
  der_rc_lemma (der, ETAnil(), RCSnil())

// all terms with a type in the empty context are SN
prfn der_sn {t:tm, T:tp} (der : DER0(RCSnil, CTXnil, t, T)) : SN0(t) =
  let 
     prval '(tpi, r) = der_rc(der)
     prval '(cr1, cr2, cr3) = tpi_is_rc(RCSnil, tpi)
  in
     cr1 r
  end