Step
*
1
of Lemma
dm-neg-neg
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-DeMorgan-lattice(T;eq))
4. ∀g,h:Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq))).
(((λz.free-dl-inc(z))
= (g o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ ((λz.free-dl-inc(z))
= (h o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ (g = h ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⊢ ¬(¬(x)) = x ∈ Point(free-DeMorgan-lattice(T;eq))
BY
{ (InstHyp [⌜λx.x⌝;⌜λx.¬(¬(x))⌝] (-1)⋅
THENM (ApFunToHypEquands `Z' ⌜Z x⌝ ⌜Point(free-DeMorgan-lattice(T;eq))⌝ (-1)⋅ THEN Reduce (-1) THEN Auto)
) }
1
.....wf.....
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-DeMorgan-lattice(T;eq))
4. ∀g,h:Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq))).
(((λz.free-dl-inc(z))
= (g o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ ((λz.free-dl-inc(z))
= (h o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ (g = h ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⊢ λx.x ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq)))
2
.....wf.....
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-DeMorgan-lattice(T;eq))
4. ∀g,h:Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq))).
(((λz.free-dl-inc(z))
= (g o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ ((λz.free-dl-inc(z))
= (h o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ (g = h ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⊢ λx.¬(¬(x)) ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq)))
3
.....antecedent.....
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-DeMorgan-lattice(T;eq))
4. ∀g,h:Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq))).
(((λz.free-dl-inc(z))
= (g o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ ((λz.free-dl-inc(z))
= (h o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ (g = h ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⊢ (λz.free-dl-inc(z))
= ((λx.x) o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq))))
4
.....antecedent.....
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-DeMorgan-lattice(T;eq))
4. ∀g,h:Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq))).
(((λz.free-dl-inc(z))
= (g o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ ((λz.free-dl-inc(z))
= (h o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⇒ (g = h ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T; union-deq(T;T;eq;eq)))))
⊢ (λz.free-dl-inc(z))
= ((λx.¬(¬(x))) o (λx.free-dl-inc(x)))
∈ ((T + T) ⟶ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq))))
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-DeMorgan-lattice(T;eq))
4. \mforall{}g,h:Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));free-dist-lattice(T + T;
union-deq(T;T;eq;eq))).
(((\mlambda{}z.free-dl-inc(z)) = (g o (\mlambda{}x.free-dl-inc(x))))
{}\mRightarrow{} ((\mlambda{}z.free-dl-inc(z)) = (h o (\mlambda{}x.free-dl-inc(x))))
{}\mRightarrow{} (g = h))
\mvdash{} \mneg{}(\mneg{}(x)) = x
By
Latex:
(InstHyp [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{};\mkleeneopen{}\mlambda{}x.\mneg{}(\mneg{}(x))\mkleeneclose{}] (-1)\mcdot{}
THENM (ApFunToHypEquands `Z' \mkleeneopen{}Z x\mkleeneclose{} \mkleeneopen{}Point(free-DeMorgan-lattice(T;eq))\mkleeneclose{} (-1)\mcdot{}
THEN Reduce (-1)
THEN Auto)
)
Home
Index