equal
deleted
inserted
replaced
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
6 |
7 Goal |
7 Goal |
|
8 "DA.accepts (na2da(rexp2na r)) w = (w : lang r)"; |
|
9 by (simp_tac (simpset() addsimps [NA_DA_equiv RS sym,accepts_rexp2na]) 1); |
|
10 qed "accepts_na2da_rexp2na"; |
|
11 |
|
12 Goal |
8 "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"; |
13 "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"; |
9 by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1); |
14 by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1); |
10 qed "accepts_nae2da_rexp2nae"; |
15 qed "accepts_nae2da_rexp2nae"; |