Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Stmt = Set
- data _∧_ (P Q : Stmt) : Stmt where
- ⟨_,_⟩ : P → Q → P ∧ Q
- data _∨_ (P Q : Stmt) : Stmt where
- inl : P → P ∨ Q
- inr : Q → P ∨ Q
- data ⊥ : Stmt where
- ¬_ : Stmt → Stmt
- ¬ P = P → ⊥
- module _ (Ω : Set) where
- Set' = Ω → Stmt
- _⊆_ : (A B : Set') → Stmt
- A ⊆ B = {x : Ω} → A x → B x
- infix 9 _⊆_
- _-_ : (A B : Set') → Set'
- (A - B) x = A x ∧ (¬ B x)
- _∪_ : (A B : Set') → Set'
- (A ∪ B) x = A x ∨ B x
- ∅ : Set'
- ∅ x = ⊥
- _=ₛₑₜ_ : Set' → Set' → Set
- A =ₛₑₜ B = (A ⊆ B) ∧ (B ⊆ A)
- infix 9 _=ₛₑₜ_
- module _ {A B C : Set'} where
- thm₁ : A ⊆ B → (A - C) ⊆ (B - C)
- thm₁ f ⟨ a , nc ⟩ = {!!}
- thm₂ : (A ∪ B) - C =ₛₑₜ (A - C) ∪ (B - C)
- thm₂ = ⟨ ABC-⊆ , ABC-⊇ ⟩
- where
- ABC-⊆ : (A ∪ B) - C ⊆ (A - C) ∪ (B - C)
- ABC-⊆ = {!!}
- ABC-⊇ : (A - C) ∪ (B - C) ⊆ (A ∪ B) - C
- ABC-⊇ = {!!}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement