---

Step * 1 of Lemma fpf-conversion-test

.....equality..... 
<[4; 6; 7], λx.if x ∈b [4; 6] then 2 else 5 fi > ~ 4 : 2 ⊕ 6 : 2 ⊕ 7 : 5
BY
{ xxx(SymbComp 0
      THEN RepeatFor 2 (EqCD)
      THEN RepeatFor 3 ((RW (SweepUpC UnrollRecursionC) 0 THEN Reduce 0))
      THEN SymbComp 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
.....equality..... 
<[4;  6;  7],  \mlambda{}x.if  x  \mmember{}\msubb{}  [4;  6]  then  2  else  5  fi  >  \msim{}  4  :  2  \moplus{}  6  :  2  \moplus{}  7  :  5


By

---

Latex:
xxx(SymbComp  0
        THEN  RepeatFor  2  (EqCD)
        THEN  RepeatFor  3  ((RW  (SweepUpC  UnrollRecursionC)  0  THEN  Reduce  0))
        THEN  SymbComp  0
        THEN  Auto)xxx

---

Home Index