---

Step * 1 of Lemma ifthenelse_wf-partial-base

.....assertion..... 
1. T : Type
2. value-type(T)
3. c1 : partial(T)
4. c2 : partial(T)
5. b : Base
6. ¬is-exception(b)
⊢ ∀x,y:Base.  ((x ∈ partial(T)) ⇒ (y ∈ partial(T)) ⇒ (if b then x else y fi  ∈ base-partial(T)))
BY
{ (TACTIC:(UnivCD THENA Auto)
   THEN At ⌜Type⌝ MemTypeCD⋅
   THEN Try (Complete (Auto))
   THEN (At ⌜Type⌝ (D 0)⋅ THENA TACTIC:(GenConclAtAddrType ⌜Base⌝ [2;1]⋅ THEN Auto))) }

1
1. T : Type
2. value-type(T)
3. c1 : partial(T)
4. c2 : partial(T)
5. b : Base
6. ¬is-exception(b)
7. x : Base
8. y : Base
9. x ∈ partial(T)
10. y ∈ partial(T)
⊢ if b then x else y fi  ∈ T supposing (if b then x else y fi )↓

2
1. T : Type
2. value-type(T)
3. c1 : partial(T)
4. c2 : partial(T)
5. b : Base
6. ¬is-exception(b)
7. x : Base
8. y : Base
9. x ∈ partial(T)
10. y ∈ partial(T)
⊢ ¬is-exception(if b then x else y fi )

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  value-type(T)
3.  c1  :  partial(T)
4.  c2  :  partial(T)
5.  b  :  Base
6.  \mneg{}is-exception(b)
\mvdash{}  \mforall{}x,y:Base.    ((x  \mmember{}  partial(T))  {}\mRightarrow{}  (y  \mmember{}  partial(T))  {}\mRightarrow{}  (if  b  then  x  else  y  fi    \mmember{}  base-partial(T)))


By

---

Latex:
(TACTIC:(UnivCD  THENA  Auto)
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  TACTIC:(GenConclAtAddrType  \mkleeneopen{}Base\mkleeneclose{}  [2;1]\mcdot{}  THEN  Auto)))

---

Home Index