27 |
27 |
28 (*----------------------scripts-----------------------*) |
28 (*----------------------scripts-----------------------*) |
29 Norm'_sq'_root'_equation |
29 Norm'_sq'_root'_equation |
30 :: "[bool,real, |
30 :: "[bool,real, |
31 bool list] => bool list" |
31 bool list] => bool list" |
32 ("((Script Norm'_sq'_root'_equation (_ _ =))// |
32 ("((Script Norm'_sq'_root'_equation (_ _ =))// (_))" 9) |
33 (_))" 9) |
|
34 Solve'_sq'_root'_equation |
33 Solve'_sq'_root'_equation |
35 :: "[bool,real, |
34 :: "[bool,real, |
36 bool list] => bool list" |
35 bool list] => bool list" |
37 ("((Script Solve'_sq'_root'_equation (_ _ =))// |
36 ("((Script Solve'_sq'_root'_equation (_ _ =))// (_))" 9) |
38 (_))" 9) |
|
39 Solve'_left'_sq'_root'_equation |
37 Solve'_left'_sq'_root'_equation |
40 :: "[bool,real, |
38 :: "[bool,real, |
41 bool list] => bool list" |
39 bool list] => bool list" |
42 ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// |
40 ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// (_))" 9) |
43 (_))" 9) |
|
44 Solve'_right'_sq'_root'_equation |
41 Solve'_right'_sq'_root'_equation |
45 :: "[bool,real, |
42 :: "[bool,real, |
46 bool list] => bool list" |
43 bool list] => bool list" |
47 ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// |
44 ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// (_))" 9) |
48 (_))" 9) |
|
49 |
45 |
50 axiomatization where |
46 axiomatization where |
51 |
47 |
52 (* normalize *) |
48 (* normalize *) |
53 makex1_x: "a^^^1 = a" and |
49 makex1_x: "a^^^1 = a" and |