Step
*
1
1
2
1
1
of Lemma
in-hull-sorted
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)}
3. i : ℕ||xs||
4. j : ℕ||xs||
5. ¬(i = j ∈ ℤ)
6. ij ∈ Hull(xs)
7. hull-cmp(g;xs;i;j) ∈ comparison({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} )
8. L : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
9. filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));upto(||xs||)) = L ∈ ({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List)
10. v : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
11. [%14] : sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));v)
12. comparison-sort(hull-cmp(g;xs;i;j);L)
= v
∈ {srtd:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List| sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));srtd)}
13. permutation({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} ;v;L)
⊢ sorted-by(λx,y. ((¬(x = y ∈ ℤ)) ⇒ (↑x L yi));v)
BY
{ (Unhide THEN Try (QuickAuto)) }
1
.....wf.....
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)}
3. i : ℕ||xs||
4. j : ℕ||xs||
5. ¬(i = j ∈ ℤ)
6. ij ∈ Hull(xs)
7. hull-cmp(g;xs;i;j) ∈ comparison({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} )
8. L : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
9. filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));upto(||xs||)) = L ∈ ({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List)
10. v : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
11. sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));v)
12. comparison-sort(hull-cmp(g;xs;i;j);L)
= v
∈ {srtd:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List| sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));srtd)}
13. permutation({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} ;v;L)
⊢ λx,y. ((¬(x = y ∈ ℤ)) ⇒ (↑x L yi)) ∈ {x:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} | (x ∈ v)}
⟶ {x:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} | (x ∈ v)}
⟶ ℙ
2
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)}
3. i : ℕ||xs||
4. j : ℕ||xs||
5. ¬(i = j ∈ ℤ)
6. ij ∈ Hull(xs)
7. hull-cmp(g;xs;i;j) ∈ comparison({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} )
8. L : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
9. filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));upto(||xs||)) = L ∈ ({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List)
10. v : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
11. [%14] : sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));v)
12. comparison-sort(hull-cmp(g;xs;i;j);L)
= v
∈ {srtd:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List| sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));srtd)}
13. permutation({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} ;v;L)
14. x : {x:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} | (x ∈ v)}
15. y : {x:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} | (x ∈ v)}
⊢ SqStable((λx,y. ((¬(x = y ∈ ℤ)) ⇒ (↑x L yi))) x y)
3
.....wf.....
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)}
3. i : ℕ||xs||
4. j : ℕ||xs||
5. ¬(i = j ∈ ℤ)
6. ij ∈ Hull(xs)
7. hull-cmp(g;xs;i;j) ∈ comparison({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} )
8. L : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
9. filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));upto(||xs||)) = L ∈ ({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List)
10. v : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
11. sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));v)
12. comparison-sort(hull-cmp(g;xs;i;j);L)
= v
∈ {srtd:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List| sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));srtd)}
13. permutation({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} ;v;L)
⊢ istype({x:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} | (x ∈ v)} )
4
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)}
3. i : ℕ||xs||
4. j : ℕ||xs||
5. ¬(i = j ∈ ℤ)
6. ij ∈ Hull(xs)
7. hull-cmp(g;xs;i;j) ∈ comparison({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} )
8. L : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
9. filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));upto(||xs||)) = L ∈ ({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List)
10. v : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List
11. sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));v)
12. comparison-sort(hull-cmp(g;xs;i;j);L)
= v
∈ {srtd:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} List| sorted-by(λx,y. (0 ≤ (hull-cmp(g;xs;i;j) x y));srtd)}
13. permutation({k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} ;v;L)
⊢ sorted-by(λx,y. ((¬(x = y ∈ ℤ)) ⇒ (↑x L yi));v)
Latex:
Latex:
1. g : OrientedPlane
2. xs : \{xs:Point List| geo-general-position(g;xs)\}
3. i : \mBbbN{}||xs||
4. j : \mBbbN{}||xs||
5. \mneg{}(i = j)
6. ij \mmember{} Hull(xs)
7. hull-cmp(g;xs;i;j) \mmember{} comparison(\{k:\mBbbN{}||xs||| (\mneg{}(k = i)) \mwedge{} (\mneg{}(k = j))\} )
8. L : \{k:\mBbbN{}||xs||| (\mneg{}(k = i)) \mwedge{} (\mneg{}(k = j))\} List
9. filter(\mlambda{}k.((\mneg{}\msubb{}(k =\msubz{} i)) \mwedge{}\msubb{} (\mneg{}\msubb{}(k =\msubz{} j)));upto(||xs||)) = L
10. v : \{k:\mBbbN{}||xs||| (\mneg{}(k = i)) \mwedge{} (\mneg{}(k = j))\} List
11. [\%14] : sorted-by(\mlambda{}x,y. (0 \mleq{} (hull-cmp(g;xs;i;j) x y));v)
12. comparison-sort(hull-cmp(g;xs;i;j);L) = v
13. permutation(\{k:\mBbbN{}||xs||| (\mneg{}(k = i)) \mwedge{} (\mneg{}(k = j))\} ;v;L)
\mvdash{} sorted-by(\mlambda{}x,y. ((\mneg{}(x = y)) {}\mRightarrow{} (\muparrow{}x L yi));v)
By
Latex:
(Unhide THEN Try (QuickAuto))
Home
Index