---

Step * 1 of Lemma lifting-strict-ifthenelse


1. F : Base
2. p : Top
3. q : Top
4. r : Top
5. strict4(λx,y,z,w. F[x;y;z;w])
6. a : Top
7. A : Top
8. B : Top
⊢ F[if a then A else B fi ;p;q;r] ~ if a then F[A;p;q;r] else F[B;p;q;r] fi 
BY
{ (Unfold `ifthenelse` 0 THEN InstLemma `lifting-strict-decide` [⌜F⌝;⌜p⌝;⌜q⌝;⌜r⌝;⌜a⌝;⌜λ2x.A⌝;⌜λ2x.B⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  Base
2.  p  :  Top
3.  q  :  Top
4.  r  :  Top
5.  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])
6.  a  :  Top
7.  A  :  Top
8.  B  :  Top
\mvdash{}  F[if  a  then  A  else  B  fi  ;p;q;r]  \msim{}  if  a  then  F[A;p;q;r]  else  F[B;p;q;r]  fi 


By

---

Latex:
(Unfold  `ifthenelse`  0
  THEN  InstLemma  `lifting-strict-decide`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.B\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index