-intro l;
-apply mk_semi_lattice;
- [apply mk_excess;
- [apply mk_excess_;
- [apply (mk_excess_dual_smart l);
- |apply (exc_ap l);
- |reflexivity]
- |unfold mk_excess_dual_smart; simplify;
- intros (x y H); cases (ap2exc ??? H); [right|left] assumption;
- |unfold mk_excess_dual_smart; simplify;
- intros (x y H);cases H; apply exc2ap;[right|left] assumption;]]
-unfold mk_excess_dual_smart; simplify;
-[1: change with ((λx.ap_carr x) l → (λx.ap_carr x) l → (λx.ap_carr x) l);
- simplify; unfold apartness_OF_lattice_;
- cases (latt_with3 l); apply (sl_meet (latt_jcarr_ l));
-|2: change in ⊢ (%→?) with ((λx.ap_carr x) l); simplify;
- unfold apartness_OF_lattice_;
- cases (latt_with3 l); apply (sl_meet_refl (latt_jcarr_ l));
-|3: change in ⊢ (%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
- cases (latt_with3 l); apply (sl_meet_comm (latt_jcarr_ l));
-|4: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
- cases (latt_with3 l); apply (sl_meet_assoc (latt_jcarr_ l));
-|5: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
- cases (latt_with3 l); apply (sl_strong_extm (latt_jcarr_ l));
-|7:
-(*
-unfold excess_base_OF_lattice_;
- change in ⊢ (?→?→? ? (% ? ?) ?)
- with (match latt_with3 l
- in eq
- return
-λright_1:apartness
-.(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right_1
- .ap_carr right_1→ap_carr right_1→ap_carr right_1)
- with
-[refl_eq⇒sl_meet (latt_jcarr_ l)]
- : ?
-);
- change in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?)
- with ((λx.exc_carr x) (excess_base_OF_semi_lattice (latt_mcarr l)));
- unfold excess_base_OF_lattice_ in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
- simplify in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
-change in ⊢ (?→?→? ? (% ? ?) ?) with
- (match refl_eq ? (excess__OF_semi_lattice (latt_mcarr l)) in eq
- return (λR.λE:eq ? (excess_base_OF_semi_lattice (latt_mcarr l)) R.R → R → R)
- with [refl_eq⇒
- (match latt_with3 l in eq
- return
- (λright:apartness
- .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
- .ap_carr right→ap_carr right→ap_carr right))
- with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
- :
- exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
- →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
- →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
- )
- ]);
- generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
- unfold excess_base_OF_lattice_ in ⊢ (? ? ? %→?);
- cases (latt_with1 l);
- change in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?)
- with ((λx.ap_carr x) (latt_mcarr l));
- simplify in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?);
- cases (latt_with3 l);
-
- change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
- simplify in ⊢ (% → ?);
- change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
- with ((λx.ap_carr x) (apartness_OF_lattice_ l));
- unfold apartness_OF_lattice_;
- cases (latt_with3 l); simplify;
- change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
- unfold excess_base_OF_lattice_;
- cases (latt_with1 l); simplify;
- change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
- change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
- with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
- simplify;
- intro H;
- unfold excess_base_OF_semi_lattice1;
- unfold excess_base_OF_excess1;
- unfold excess_base_OF_excess_1;
- change
-*)
-
-change in ⊢ (?→?→? ? (% ? ?) ?) with
- (match refl_eq ? (Type_OF_lattice_ l) in eq
- return (λR.λE:eq ? (Type_OF_lattice_ l) R.R → R → R)
- with [refl_eq⇒
- match latt_with3 l in eq
- return
- (λright:apartness
- .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
- .ap_carr right→ap_carr right→ap_carr right))
- with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
- ]);
- generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
- change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
- simplify in ⊢ (% → ?);
- change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
- with ((λx.ap_carr x) (apartness_OF_lattice_ l));
- unfold apartness_OF_lattice_;
- cases (latt_with3 l); simplify;
- change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
- unfold excess_base_OF_lattice_;
- cases (latt_with1 l); simplify;
- change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
- change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
- with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
- simplify;
- intro H;
- change in ⊢ (?→?→%) with (le (mk_excess_base
- ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
- ((λx.exc_excess x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
- ((λx.exc_coreflexive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
- ((λx.exc_cotransitive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
- ) (match H
- in eq
- return
-λR:Type
-.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R
- .R→R→R)
- with
-[refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y);
- simplify in ⊢ (?→?→? (? % ???) ? ?);
- change in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
- with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
- simplify in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?);
- lapply (match H in eq return
- λright.λe:eq ? (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) right.
-
-∀x:right
-.∀y:right
- .le
- (mk_excess_base right ???)
- (match e
- in eq
- return
- λR:Type.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R.R→R→R)
- with
- [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y
- with [refl_eq ⇒ ?]) as XX;
- [cases e; apply (exc_excess (latt_jcarr_ l));
- |unfold;cases e;simplify;apply (exc_coreflexive (latt_jcarr_ l));
- |unfold;cases e;simplify;apply (exc_cotransitive (latt_jcarr_ l));
- ||apply XX|
- |apply XX;
-
- simplify; apply (sl_lem);
-|elim FALSE]