---

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
{ (SymbComp 0
   THEN RepeatFor 2 (EqCD)
   THEN RepeatFor 3 ((RW (SweepUpC UnrollRecursionC) 0 THEN Reduce 0))
   THEN SymbComp 0
   THEN Auto) }

---

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

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

---

Home Index