From 17c6ac2888a1f30aee059f5cf6b8872bb4f3ab61 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 1 Aug 2009 16:50:02 +0000 Subject: [PATCH] Smaller formulae. --- helm/software/matita/nlibrary/sets/sets.ma | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 20d069caa..81f0f07c7 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -41,11 +41,11 @@ ndefinition powerset_setoid1: setoid → setoid1. [ napply (Ω \sup S) | napply mk_equivalence_relation1 [ #A; #B; napply (∀x. iff (x ∈ A) (x ∈ B)) - | nnormalize; #x; #x0; napply mk_iff; #H; nassumption - | nnormalize; #x; #y; #H; #A; napply mk_iff; #K + | nwhd; #x; #x0; napply mk_iff; #H; nassumption + | nwhd; #x; #y; #H; #A; napply mk_iff; #K [ napply (fi ?? (H ?)) | napply (if ?? (H ?)) ] nassumption - | nnormalize; #A; #B; #C; #H1; #H2; #H3; napply mk_iff; #H4 + | nwhd; #A; #B; #C; #H1; #H2; #H3; napply mk_iff; #H4 [ napply (if ?? (H2 ?)); napply (if ?? (H1 ?)); nassumption | napply (fi ?? (H1 ?)); napply (fi ?? (H2 ?)); nassumption]##] nqed. @@ -69,8 +69,8 @@ interpretation "overlaps" 'overlaps U V = (overlaps ? U V). ndefinition intersects ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∧ x ∈ V }. #a; #a'; #H; napply mk_iff; *; #H1; #H2 - [ napply (. ((H^-1‡#)‡(H^-1‡#))); nnormalize; napply conj; nassumption - | napply (. ((H‡#)‡(H‡#))); nnormalize; napply conj; nassumption] + [ napply (. ((H^-1‡#)‡(H^-1‡#))); nwhd; napply conj; nassumption + | napply (. ((H‡#)‡(H‡#))); nwhd; napply conj; nassumption] nqed. (*interpretation "intersects" 'intersects U V = (intersects ? U V).*) -- 2.39.2