Step
*
1
of Lemma
is-list-if-has-value-decomp
1. t : ListLike
2. (t)↓
⊢ ((↑isaxiom(t)) ∧ (t = Ax ∈ Unit)) ∨ ((↑ispair(t)) ∧ (∃a:Top. ∃b:ListLike. (t = <a, b> ∈ (Top × ListLike))))
BY
{ (UseWitness ⌜if t = Ax then inl <Ax, Ax> otherwise let t,y = t 
                                  in inr <Ax, t, y, Ax> ⌝⋅
   THEN GenConcl ⌜t = c ∈ (Unit ⋃ (Top × ListLike))⌝⋅
   THEN Auto) }
1
.....wf..... 
1. t : ListLike
2. (t)↓
⊢ t ∈ Unit ⋃ (Top × ListLike)
2
.....wf..... 
1. t : ListLike
2. (t)↓
3. a1 : 0 = 0 ∈ ℤ
4. t = ((λp.(snd(p))) <inl Ax, Ax>) ∈ (Unit ⋃ (Top × ListLike))
⊢ ispair((λp.(snd(p))) <inl Ax, Ax>) ∈ 𝔹
Latex:
Latex:
1.  t  :  ListLike
2.  (t)\mdownarrow{}
\mvdash{}  ((\muparrow{}isaxiom(t))  \mwedge{}  (t  =  Ax))  \mvee{}  ((\muparrow{}ispair(t))  \mwedge{}  (\mexists{}a:Top.  \mexists{}b:ListLike.  (t  =  <a,  b>)))
By
Latex:
(UseWitness  \mkleeneopen{}if  t  =  Ax  then  inl  <Ax,  Ax>  otherwise  let  t,y  =  t  in  inr  <Ax,  t,  y,  Ax>  \mkleeneclose{}\mcdot{}  THEN  GenConc\000Cl  \mkleeneopen{}t  =  c\mkleeneclose{}\mcdot{}  THEN  Auto)
Home
Index