1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "subterms/carrier.ma".
16 include "subterms/boolean.ma".
18 (* BOOLEANIZED SUBSET (EMPTY OR FULL) **************************************)
20 definition booleanized: bool → subterms → subterms ≝
23 interpretation "make boolean (subterms)"
24 'ProjectSame b F = (booleanized b F).
26 notation "hvbox( { term 46 b } ⇕ break term 46 F)"
27 non associative with precedence 46
28 for @{ 'ProjectSame $b $F }.
30 lemma booleanized_inv_vref: ∀j,c,b,F. {b}⇕ F = {c}#j →
31 ∃∃b1. b = c & F = {b1}#j.
33 elim (boolean_inv_vref … H) -H #H0 #H
34 elim (carrier_inv_vref … H) -H /2 width=2/
37 lemma booleanized_inv_abst: ∀U,c,b,F. {b}⇕ F = {c}𝛌.U →
38 ∃∃b1,T. b = c & {b}⇕T = U & F = {b1}𝛌.T.
40 elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
41 elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
44 lemma booleanized_inv_appl: ∀W,U,c,b,F. {b}⇕ F = {c}@W.U →
45 ∃∃b1,V,T. b = c & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
47 elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
48 elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
51 lemma booleanized_booleanized: ∀c,b,F. {b}⇕ {c}⇕ F = {b}⇕ F.
55 lemma booleanized_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F.
59 lemma booleanized_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F.