Step * 1 of Lemma is-list-if-has-value-decomp


1. ListLike
2. (t)↓
⊢ ((↑isaxiom(t)) ∧ (t Ax ∈ Unit)) ∨ ((↑ispair(t)) ∧ (∃a:Top. ∃b:ListLike. (t = <a, b> ∈ (Top × ListLike))))
BY
(UseWitness ⌜if Ax then inl <Ax, Ax> otherwise let t,y 
                                  in inr <Ax, t, y, Ax> ⌝⋅
   THEN GenConcl ⌜c ∈ (Unit ⋃ (Top × ListLike))⌝⋅
   THEN Auto) }

1
.....wf..... 
1. ListLike
2. (t)↓
⊢ t ∈ Unit ⋃ (Top × ListLike)

2
.....wf..... 
1. ListLike
2. (t)↓
3. a1 0 ∈ ℤ
4. ((λ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