| changeset 48 | 21291189b51e |
| parent 0 | 7949f97df77a |
| child 56 | 385d51d74f71 |
| 47:69d815b0e1eb | 48:21291189b51e |
|---|---|
44 pl_rec_imp "pl_rec(p->q,f,y,g) = g(pl_rec(p,f,y,g),pl_rec(q,f,y,g))" |
44 pl_rec_imp "pl_rec(p->q,f,y,g) = g(pl_rec(p,f,y,g),pl_rec(q,f,y,g))" |
45 |
45 |
46 eval_def "tt[p] == pl_rec(p, %v.v:tt, False, op -->)" |
46 eval_def "tt[p] == pl_rec(p, %v.v:tt, False, op -->)" |
47 |
47 |
48 hyps_def |
48 hyps_def |
49 "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, #a->false)}, {}, op Un)" |
49 "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, (#a)->false)}, {}, op Un)" |
50 |
50 |
51 var_inject "(#v = #w) ==> v = w" |
51 var_inject "(#v = #w) ==> v = w" |
52 imp_inject "[| (p -> q) = (p' -> q'); [| p = p'; q = q' |] ==> R |] ==> R" |
52 imp_inject "[| (p -> q) = (p' -> q'); [| p = p'; q = q' |] ==> R |] ==> R" |
53 var_neq_imp "(#v = (p -> q)) ==> R" |
53 var_neq_imp "(#v = (p -> q)) ==> R" |
54 pl_ind "[| P(false); !!v. P(#v); !!p q. P(p)-->P(q)-->P(p->q)|] ==> !t.P(t)" |
54 pl_ind "[| P(false); !!v. P(#v); !!p q. P(p)-->P(q)-->P(p->q)|] ==> !t.P(t)" |