Step * 1 of Lemma fpf-conversion-test

.....equality..... 
<[4; 6; 7], λx.if x ∈b [4; 6]) then else fi > 2 ⊕ 2 ⊕ 5
BY
(SymbComp 0
   THEN RepeatFor (EqCD)
   THEN RepeatFor ((RW (SweepUpC UnrollRecursionC) 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