---

Step * 1 1 1 1 of Lemma int_ring_wf


<ℤ, λu,v. (u =z v), λu,v. u ≤z v, λu,v. (u + v), 0, λu.(-u), λu,v. (u * v), 1, λu,v. if (v =z 0) then inr ⋅  else inl (u\000C ÷ v) fi >
∈ car:Type
× eq:car ⟶ car ⟶ 𝔹
× le:car ⟶ car ⟶ 𝔹
× plus:car ⟶ car ⟶ car
× zero:car
× minus:car ⟶ car
× times:car ⟶ car ⟶ car
× one:car
× (car ⟶ car ⟶ (car?))
BY
{ RepeatFor 8 ((MemCD THENL [Auto;Id;Auto⋅]))
THEN RepeatFor 2 (MemCD THENL [Id; Auto])
THEN SplitOnConclITE
THEN Auto
THEN Unfold `bfalse` 0
THEN Auto }

---

Latex:

---

Latex:

<\mBbbZ{}
,  \mlambda{}u,v.  (u  =\msubz{}  v)
,  \mlambda{}u,v.  u  \mleq{}z  v
,  \mlambda{}u,v.  (u  +  v)
,  0
,  \mlambda{}u.(-u)
,  \mlambda{}u,v.  (u  *  v)
,  1
,  \mlambda{}u,v.  if  (v  =\msubz{}  0)  then  inr  \mcdot{}    else  inl  (u  \mdiv{}  v)  fi  >  \mmember{}  car:Type
\mtimes{}  eq:car  {}\mrightarrow{}  car  {}\mrightarrow{}  \mBbbB{}
\mtimes{}  le:car  {}\mrightarrow{}  car  {}\mrightarrow{}  \mBbbB{}
\mtimes{}  plus:car  {}\mrightarrow{}  car  {}\mrightarrow{}  car
\mtimes{}  zero:car
\mtimes{}  minus:car  {}\mrightarrow{}  car
\mtimes{}  times:car  {}\mrightarrow{}  car  {}\mrightarrow{}  car
\mtimes{}  one:car
\mtimes{}  (car  {}\mrightarrow{}  car  {}\mrightarrow{}  (car?))


By

---

Latex:
RepeatFor  8  ((MemCD  THENL  [Auto;Id;Auto\mcdot{}]))
THEN  RepeatFor  2  (MemCD  THENL  [Id;  Auto])
THEN  SplitOnConclITE
THEN  Auto
THEN  Unfold  `bfalse`  0
THEN  Auto

---

Home Index