Step * of Lemma mk-eo-record_wf

`∀[E:Type]. ∀[dom:E ─→ 𝔹]. ∀[l:E ─→ Id]. ∀[R:E ─→ E ─→ ℙ]. ∀[locless:E ─→ E ─→ 𝔹]. ∀[pred:E ─→ E]. ∀[rank:E ─→ ℕ].`
`  (mk-eo-record(E;dom;l;R;locless;pred;rank) ∈ eo_record{i:l}())`
BY
`{ (Auto`
`   THEN RepUR ``mk-eo-record eo_record`` 0`
`   THEN RepeatFor 7 ((RecordPlusTypeCD THEN Reduce 0 THEN Try (Trivial)))`
`   THEN RepUR ``record record-update`` 0`
`   THEN Auto) }`

Latex:

\mforall{}[E:Type].  \mforall{}[dom:E  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[l:E  {}\mrightarrow{}  Id].  \mforall{}[R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[locless:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[pred:E  {}\mrightarrow{}  E].
\mforall{}[rank:E  {}\mrightarrow{}  \mBbbN{}].
(mk-eo-record(E;dom;l;R;locless;pred;rank)  \mmember{}  eo\_record\{i:l\}())

By

(Auto
THEN  RepUR  ``mk-eo-record  eo\_record``  0
THEN  RepeatFor  7  ((RecordPlusTypeCD  THEN  Reduce  0  THEN  Try  (Trivial)))
THEN  RepUR  ``record  record-update``  0
THEN  Auto)

Home Index