equal
deleted
inserted
replaced
25 by (rtac AlwaysI 1); |
25 by (rtac AlwaysI 1); |
26 by (Force_tac 1); |
26 by (Force_tac 1); |
27 by (rtac (constrains_imp_Constrains RS StableI) 1); |
27 by (rtac (constrains_imp_Constrains RS StableI) 1); |
28 by (auto_tac (claset(), simpset() addsimps [constrains_Join])); |
28 by (auto_tac (claset(), simpset() addsimps [constrains_Join])); |
29 by (constrains_tac 2); |
29 by (constrains_tac 2); |
30 by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset())); |
30 by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset())); |
31 by (constrains_tac 1); |
31 by (constrains_tac 1); |
32 qed "invFG"; |
32 qed "invFG"; |
33 |
33 |
34 Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \ |
34 Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \ |
35 \ ({s. NF s = k} Int {s. BB s})"; |
35 \ ({s. NF s = k} Int {s. BB s})"; |