---

Step * of Lemma ifthenelse_wf-partial-base

∀T:Type
  (value-type(T) ⇒ (∀c1,c2:partial(T). ∀b:Base.  if b then c1 else c2 fi  ∈ partial(T) supposing ¬is-exception(b)))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN Assert ⌜∀x,y:Base.  ((x ∈ partial(T)) ⇒ (y ∈ partial(T)) ⇒ (if b then x else y fi  ∈ base-partial(T)))⌝
               ⋅
          ) }

1
.....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)))

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,y:Base.  ((x ∈ partial(T)) ⇒ (y ∈ partial(T)) ⇒ (if b then x else y fi  ∈ base-partial(T)))
⊢ if b then c1 else c2 fi  ∈ partial(T)

---

Latex:

---

Latex:
\mforall{}T:Type
    (value-type(T)
    {}\mRightarrow{}  (\mforall{}c1,c2:partial(T).  \mforall{}b:Base.
                if  b  then  c1  else  c2  fi    \mmember{}  partial(T)  supposing  \mneg{}is-exception(b)))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  Assert  \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{}
                )

---

Home Index