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