Step * of Lemma is-list_wf

`∀[T:Type]. ∀[t:colist(T)].  (is-list(t) ∈ partial(𝔹))`
BY
`{ ((Auto`
`    THEN Unfold `colist` -1`
`    THEN Unfold `is-list` 0`
`    THEN InstLemma `fix_wf_corec-partial1` [⌜𝔹⌝;⌜λ2L.Unit ⋃ (T × L)⌝;⌜λis-list,t. eval u = t in`
`                                                                                  if u is a pair then is-list (snd(u))`
`                                                                                  otherwise if u = Ax then tt`
`                                                                                            otherwise ⊥⌝]⋅`
`    THEN Auto)`
`   THEN D_b_union (-1)`
`   THEN D -1`
`   THEN Reduce 0`
`   THEN Auto) }`

Latex:

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    (is-list(t)  \mmember{}  partial(\mBbbB{}))

By

Latex:
((Auto
THEN  Unfold  `colist`  -1
THEN  Unfold  `is-list`  0
THEN  InstLemma  `fix\_wf\_corec-partial1`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}L.Unit  \mcup{}  (T  \mtimes{}  L)\mkleeneclose{};
\mkleeneopen{}\mlambda{}is-list,t.  eval  u  =  t  in
if  u  is  a  pair  then  is-list  (snd(u))  otherwise  if  u  =  Ax  then  tt  otherwise  \mbot{}\mkleeneclose{}]\mcdot{}
THEN  Auto)
THEN  D\_b\_union  (-1)
THEN  D  -1
THEN  Reduce  0
THEN  Auto)

Home Index