| changeset 12195 | ed2893765a08 |
| parent 11479 | 697dcaaf478f |
| child 14092 | 68da54626309 |
| 12194:13909cb72129 | 12195:ed2893765a08 |
|---|---|
12 |
12 |
13 FP = UNITY + |
13 FP = UNITY + |
14 |
14 |
15 constdefs |
15 constdefs |
16 FP_Orig :: i=>i |
16 FP_Orig :: i=>i |
17 "FP_Orig(F) == Union({A:condition. ALL B:condition. F : stable(A Int B)})" |
17 "FP_Orig(F) == Union({A:Pow(state). ALL B. F : stable(A Int B)})" |
18 |
18 |
19 FP :: i=>i |
19 FP :: i=>i |
20 "FP(F) == {s:state. F : stable({s})}" |
20 "FP(F) == {s:state. F : stable({s})}" |
21 |
21 |
22 end |
22 end |