---

Step * of Lemma Girard-theorem-extract

¬(Type ∈ Type)
BY
{ Extract of Obid: Girard-theorem
  not unfolding  max-WO max-WFTO DCC order-type-less DCC-order-type Maximal-order-type
  finishing with (Folds ``pi1 pi2`` 0 THEN Auto)
  normalizes to:
  
  λ_.(DCC-order-type() (λn.max-WO{i:l}()) 
      (λn.<λa.<b:WFO{i:l}() × (order-type-less() b a), λp1,p2. (order-type-less() (fst(p1)) (fst(p2))), λf,_. Ax>
          , <WFO{i:l}(), order-type-less(), DCC-order-type()>
          , λa1,a2,z. <λp1.let a,p2 = p1 in <a, ot-less-trans() a a1 a2 p2 z>, <a1, z>, λ_,_,z. z, λa.(snd(a))>
          , λa.<λx.(fst(x)), a, λ_,_,z. z, λa.(snd(a))>>)) }

---

Latex:

---

Latex:
\mneg{}(Type  \mmember{}  Type)


By

---

Latex:
Extract  of  Obid:  Girard-theorem
not  unfolding    max-WO  max-WFTO  DCC  order-type-less  DCC-order-type  Maximal-order-type
finishing  with  (Folds  ``pi1  pi2``  0  THEN  Auto)
normalizes  to:

\mlambda{}$_{}$.(DCC-order-type()  (\mlambda{}n.max-WO\{i:l\}()) 
      (\mlambda{}n.<\mlambda{}a.<b:WFO\{i:l\}()  \mtimes{}  (order-type-less()  b  a)
                      ,  \mlambda{}p1,p2.  (order-type-less()  (fst(p1))  (fst(p2)))
                      ,  \mlambda{}f,$_{}$.  Ax>
              ,  <WFO\{i:l\}(),  order-type-less(),  DCC-order-type()>
              ,  \mlambda{}a1,a2,z.  <\mlambda{}p1.let  a,p2  =  p1  in  <a,  ot-less-trans()  a  a1  a2  p2  z>,  <a1,  z>,  \mlambda{}$_\mbackslash{}ff7\000Cb}$,$_{}$,z.  z,  \mlambda{}a.(snd(a))>
              ,  \mlambda{}a.<\mlambda{}x.(fst(x)),  a,  \mlambda{}$_{}$,$_{}$,z.  z,  \mlambda{}a.(snd(a))>\000C>))

---

Home Index