---

Step * of Lemma fpf-conversion-test

4 : 2 ⊕ 6 : 2 ⊕ 7 : 5 = <[4; 6; 7], λx.if x ∈b [4; 6]) then 2 else 5 fi > ∈ i:ℤ fp-> ℤ
BY
{ skip{ this doesn't test the NormalizeIntFpfC anymore. Instead it shows how SymbolicCompute works on fpfs}
THEN Subst' <[4; 6; 7], λx.if x ∈b [4; 6]) then 2 else 5 fi > ~ 4 : 2 ⊕ 6 : 2 ⊕ 7 : 5 0 }

1
.....equality..... 
<[4; 6; 7], λx.if x ∈b [4; 6]) then 2 else 5 fi > ~ 4 : 2 ⊕ 6 : 2 ⊕ 7 : 5

2
4 : 2 ⊕ 6 : 2 ⊕ 7 : 5 = 4 : 2 ⊕ 6 : 2 ⊕ 7 : 5 ∈ i:ℤ fp-> ℤ

---

Latex:


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


By

skip\{...\}
THEN  Subst'  <[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  0

---

Home Index