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 "lambda/subterms/boolean.ma".
17 include "lambda/notation/functions/projectsame_2.ma".
19 include "lambda/xoa/ex_4_3.ma".
21 (* BOOLEANIZED SUBSET (EMPTY OR FULL) ***************************************)
23 definition booleanized: bool → subterms → subterms ≝
26 interpretation "booleanized (subterms)"
27 'ProjectSame b F = (booleanized b F).
29 lemma booleanized_inv_vref: ∀j,c,b,F. {b}⇕ F = {c}#j →
30 ∃∃b1. b = c & F = {b1}#j.
32 elim (boolean_inv_vref … H) -H #H0 #H
33 elim (carrier_inv_vref … H) -H /2 width=2/
36 lemma booleanized_inv_abst: ∀U,c,b,F. {b}⇕ F = {c}𝛌.U →
37 ∃∃b1,T. b = c & {b}⇕T = U & F = {b1}𝛌.T.
39 elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
40 elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
43 lemma booleanized_inv_appl: ∀W,U,c,b,F. {b}⇕ F = {c}@W.U →
44 ∃∃b1,V,T. b = c & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
46 elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
47 elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
50 lemma booleanized_booleanized: ∀c,b,F. {b}⇕ {c}⇕ F = {b}⇕ F.
54 lemma booleanized_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F.
58 lemma booleanized_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F.