equal
deleted
inserted
replaced
31 defs |
31 defs |
32 sat_def "H |= p == (!tt. (!q:H. tt[q]) --> tt[p])" |
32 sat_def "H |= p == (!tt. (!q:H. tt[q]) --> tt[p])" |
33 eval_def "tt[p] == eval2 p tt" |
33 eval_def "tt[p] == eval2 p tt" |
34 |
34 |
35 primrec eval2 pl |
35 primrec eval2 pl |
36 eval2_false "eval2(false) = (%x.False)" |
36 "eval2(false) = (%x.False)" |
37 eval2_var "eval2(#v) = (%tt.v:tt)" |
37 "eval2(#v) = (%tt.v:tt)" |
38 eval2_imp "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)" |
38 "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)" |
39 |
39 |
40 primrec hyps pl |
40 primrec hyps pl |
41 hyps_false "hyps(false) = (%tt.{})" |
41 "hyps(false) = (%tt.{})" |
42 hyps_var "hyps(#v) = (%tt.{if v:tt then #v else #v->false})" |
42 "hyps(#v) = (%tt.{if v:tt then #v else #v->false})" |
43 hyps_imp "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)" |
43 "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)" |
44 |
44 |
45 end |
45 end |
|
46 |