mirror of
https://github.com/Brandon-Rozek/website.git
synced 2025-08-04 15:42:00 +00:00
New post
This commit is contained in:
parent
4c5cf6a081
commit
2d6e7972b4
2 changed files with 491 additions and 0 deletions
132
content/blog/verifying-proofs-type-checkers.md
Normal file
132
content/blog/verifying-proofs-type-checkers.md
Normal file
|
|
@ -0,0 +1,132 @@
|
||||||
|
---
|
||||||
|
title: "Verifying Proofs with Type Checkers"
|
||||||
|
date: 2025-05-27T09:27:59-04:00
|
||||||
|
draft: false
|
||||||
|
tags: ["Formal Methods"]
|
||||||
|
math: true
|
||||||
|
medium_enabled: false
|
||||||
|
---
|
||||||
|
|
||||||
|
The [Curry-Howard Correspondance](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) establishes a direct connection between computer programs and mathematical proofs.
|
||||||
|
|
||||||
|
| Programs | Proofs |
|
||||||
|
| ----------------------------- | ----------------------- |
|
||||||
|
| Type | Formula |
|
||||||
|
| Term | Proof |
|
||||||
|
| Type has an element | Formula is provable |
|
||||||
|
| Type does not have an element | Formula is not provable |
|
||||||
|
|
||||||
|
When we think about traditional type systems, however, most are uncapable of expressing interesting formula. This ultimately limits the formulas we can prove.
|
||||||
|
|
||||||
|
For example, consider the simply typed lambda calculus. In that system we have base types like `int` and `bool`, as well as function types $t1 \rightarrow t2$ which take a type and return a type.
|
||||||
|
|
||||||
|
From that system, we can then create a proof of an integer by showing the term `0`. The following shows how to use the Lean 4 type checker to verify that `0` is an integer:
|
||||||
|
|
||||||
|
```lean4
|
||||||
|
#check (0: Int)
|
||||||
|
```
|
||||||
|
|
||||||
|
This, however, isn't a very interesting proof or formula. What would be more interesting is if we can use a type checker to verify the following:
|
||||||
|
|
||||||
|
```lean4
|
||||||
|
#check (by exists [] : ∃ (x : List Int), x.length = 0)
|
||||||
|
```
|
||||||
|
|
||||||
|
Sadly, we can't verify this with the simply typed lambda calculus. This does not mean that we cannot design a type system that can.
|
||||||
|
|
||||||
|
Interactive theorem provers (ITPs) or [proof assistants](https://en.wikipedia.org/wiki/Proof_assistant) help fill this void. Equipped with sophisticated type systems, they allow us to prove a formula by writing a program of that type. Some of the most popular ones include [Lean](https://lean-lang.org/), [Rocq](https://rocq-prover.org/), [Isabelle](https://isabelle.in.tum.de/), [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php), and [F*](https://fstar-lang.org/).
|
||||||
|
|
||||||
|
The underlying type system of each proof assistant is different. However, there are many similarities. In general, most aim to be at least as powerful as the calculus of constructions developed by Thierry Coquand.
|
||||||
|
|
||||||
|
To get an idea of how expressive these type systems are, we can analyze the [Lambda cube](https://en.wikipedia.org/wiki/Lambda_cube). Developed by Henk Barendregt, this characterizes the space between the simply typed lambda calculus and the calculus of constructions.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
[Image courtesy of Tellofou on Wikipedia](https://commons.wikimedia.org/wiki/File:Lambda_Cube_img.svg).
|
||||||
|
|
||||||
|
Each dimension corresponds to an extension of the simply typed lambda calculus:
|
||||||
|
- X Axis: Dependent types (Types that depend on terms)
|
||||||
|
- Y Axis: Polymorphic types (Terms that depend on types)
|
||||||
|
- Z Axis: Type Operators (Types that depend on types)
|
||||||
|
|
||||||
|
**Dependent Type**
|
||||||
|
|
||||||
|
A dependent type is a type that depends on some term. We can use this to, for example, write functions that return entirely different base types depending on the outcome of some conditional.
|
||||||
|
|
||||||
|
Here's an example function you can write in Lean 4:
|
||||||
|
|
||||||
|
```lean4
|
||||||
|
def isZeroOrMore (n : Nat) : (if n == 0 then Bool else Nat) :=
|
||||||
|
if H: n == 0 then by
|
||||||
|
rw [if_pos (by exact H)]
|
||||||
|
exact true
|
||||||
|
else by
|
||||||
|
rw [if_neg (by exact H)]
|
||||||
|
exact n
|
||||||
|
```
|
||||||
|
|
||||||
|
The function `isZeroOrMore` will return `true` if the parameter `n` is equal to zero, otherwise it'll return the natural number parameter itself.
|
||||||
|
|
||||||
|
**Type Operators**
|
||||||
|
|
||||||
|
A type operator takes a type and produces a type. For example, we can create a triple type that represents the product of three base types.
|
||||||
|
|
||||||
|
```lean4
|
||||||
|
structure Triple {A B C : Type} where
|
||||||
|
a: A
|
||||||
|
b: B
|
||||||
|
c: C
|
||||||
|
```
|
||||||
|
|
||||||
|
Let's say that we want to enforce that all three elements of the triple are of type `Int`. Then we can create a new type `IntTriple` as follows:
|
||||||
|
|
||||||
|
```Lean 4
|
||||||
|
def IntTriple := @Triple Int Int Int
|
||||||
|
```
|
||||||
|
|
||||||
|
From here, we can use `IntTriple` when type checking values.
|
||||||
|
|
||||||
|
```
|
||||||
|
#check (Triple.mk 1 2 3 : IntTriple)
|
||||||
|
````
|
||||||
|
|
||||||
|
|
||||||
|
**Type Polymorphism**
|
||||||
|
|
||||||
|
Type polymorphism allows us to write one function which covers many different types. There are two common places that we see this often.
|
||||||
|
|
||||||
|
Identity function:
|
||||||
|
```lean4
|
||||||
|
def iden {α : Type} (x : α) : α := x
|
||||||
|
```
|
||||||
|
|
||||||
|
Here we're saying that the parameter a can be of any arbitrary type α, and the function `iden` will then just return the parameter itself.
|
||||||
|
|
||||||
|
We also see this often when defining operations over lists
|
||||||
|
|
||||||
|
```lean4
|
||||||
|
def map {α β : Type} (f: α → β) (as: List α): List β :=
|
||||||
|
match as with
|
||||||
|
| [] => []
|
||||||
|
| (head::tail) => f head :: map f tail
|
||||||
|
```
|
||||||
|
|
||||||
|
The calculus of constructions support all of these three extensions. We've introduced enough here to write a more interesting proof.
|
||||||
|
|
||||||
|
```lean4
|
||||||
|
theorem map_iden_idempotent {α : Type} (as: List α) : (map iden as = as) := by
|
||||||
|
unfold iden
|
||||||
|
induction as
|
||||||
|
case nil =>
|
||||||
|
unfold map
|
||||||
|
rfl
|
||||||
|
case cons h t IH =>
|
||||||
|
unfold map
|
||||||
|
rw [IH]
|
||||||
|
```
|
||||||
|
|
||||||
|
We've invoked the Lean type checker to verify that for a list of any arbitrary type, when you map over it with the identity function you get back the list itself.
|
||||||
|
|
||||||
|
You might ask, why don't all programming languages support this? By adding expressivity to our type system, we sacrifice computational efficiency. For most standard programming tasks, we want our type checker to be as fast as possible. However when we require stronger guarentees of correctness about our code, proof assistants are a great tool for the job. Many of them even generate code for mainstream programming languages.
|
||||||
|
|
||||||
|
That's all for today. I'd like to thank James Oswald for the inspiration to write this post and some of its examples. This was adapted from a presentation we gave last month to our weekly seminar series.
|
||||||
359
static/files/images/blog/Lambda_Cube_img.svg
Normal file
359
static/files/images/blog/Lambda_Cube_img.svg
Normal file
|
|
@ -0,0 +1,359 @@
|
||||||
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||||
|
<svg
|
||||||
|
xmlns:dc="http://purl.org/dc/elements/1.1/"
|
||||||
|
xmlns:cc="http://creativecommons.org/ns#"
|
||||||
|
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
|
||||||
|
xmlns:svg="http://www.w3.org/2000/svg"
|
||||||
|
xmlns="http://www.w3.org/2000/svg"
|
||||||
|
viewBox="0 0 252.98267 203.86"
|
||||||
|
height="203.86"
|
||||||
|
width="252.98267"
|
||||||
|
xml:space="preserve"
|
||||||
|
id="svg2"
|
||||||
|
version="1.1"><metadata
|
||||||
|
id="metadata8"><rdf:RDF><cc:Work
|
||||||
|
rdf:about=""><dc:format>image/svg+xml</dc:format><dc:type
|
||||||
|
rdf:resource="http://purl.org/dc/dcmitype/StillImage" /></cc:Work></rdf:RDF></metadata><defs
|
||||||
|
id="defs6" /><g
|
||||||
|
transform="matrix(1.3333333,0,0,-1.3333333,0,203.86)"
|
||||||
|
id="g10"><g
|
||||||
|
transform="translate(94.868,76.448)"
|
||||||
|
id="g12"><g
|
||||||
|
id="g14"><g
|
||||||
|
id="g16"><g
|
||||||
|
id="g18"><g
|
||||||
|
transform="translate(-91.548,-68.735)"
|
||||||
|
id="g20"><g
|
||||||
|
transform="translate(11.208,132.107)"
|
||||||
|
id="g22"><g
|
||||||
|
id="g24" /><g
|
||||||
|
transform="translate(50.601)"
|
||||||
|
id="g26"><g
|
||||||
|
id="g28"><g
|
||||||
|
id="g30"><g
|
||||||
|
transform="translate(-6.185)"
|
||||||
|
id="g32"><g
|
||||||
|
id="g34"><g
|
||||||
|
transform="translate(-58.944,-139.82)"
|
||||||
|
id="g36"><text
|
||||||
|
id="text40"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMMI10;-inkscape-font-specification:CMMI10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,58.944,139.82)"><tspan
|
||||||
|
id="tspan38"
|
||||||
|
y="0"
|
||||||
|
x="0 5.8111844">λω</tspan></text>
|
||||||
|
<g
|
||||||
|
transform="translate(58.944,139.82)"
|
||||||
|
id="g42" /></g></g><g
|
||||||
|
transform="translate(6.185)"
|
||||||
|
id="g44" /></g></g></g><g
|
||||||
|
transform="translate(52.001)"
|
||||||
|
id="g46"><g
|
||||||
|
id="g48" /><g
|
||||||
|
transform="translate(55.89)"
|
||||||
|
id="g50"><g
|
||||||
|
id="g52"><g
|
||||||
|
id="g54"><g
|
||||||
|
transform="translate(-6.822)"
|
||||||
|
id="g56"><g
|
||||||
|
id="g58"><g
|
||||||
|
transform="translate(-166.198,-139.82)"
|
||||||
|
id="g60"><text
|
||||||
|
id="text64"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMMI10;-inkscape-font-specification:CMMI10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,166.198,139.82)"><tspan
|
||||||
|
id="tspan62"
|
||||||
|
y="0"
|
||||||
|
x="0 5.8111844">λC</tspan></text>
|
||||||
|
<g
|
||||||
|
transform="translate(166.198,139.82)"
|
||||||
|
id="g66" /></g></g><g
|
||||||
|
transform="translate(6.822)"
|
||||||
|
id="g68" /></g></g></g><g
|
||||||
|
transform="translate(-158.492,-44.035)"
|
||||||
|
id="g70"><g
|
||||||
|
id="g72"><g
|
||||||
|
id="g74"><g
|
||||||
|
transform="translate(-5.396)"
|
||||||
|
id="g76"><g
|
||||||
|
id="g78"><g
|
||||||
|
transform="translate(-9.132,-95.785)"
|
||||||
|
id="g80"><text
|
||||||
|
id="text84"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMMI10;-inkscape-font-specification:CMMI10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,9.132,95.785)"><tspan
|
||||||
|
id="tspan82"
|
||||||
|
y="0"
|
||||||
|
x="0">λ</tspan></text>
|
||||||
|
<text
|
||||||
|
id="text88"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMR10;-inkscape-font-specification:CMR10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,14.943,95.785)"><tspan
|
||||||
|
id="tspan86"
|
||||||
|
y="0"
|
||||||
|
x="0">2</tspan></text>
|
||||||
|
<g
|
||||||
|
transform="translate(9.132,95.785)"
|
||||||
|
id="g90" /></g></g><g
|
||||||
|
transform="translate(5.396)"
|
||||||
|
id="g92" /></g></g></g><g
|
||||||
|
transform="translate(50.601)"
|
||||||
|
id="g94"><g
|
||||||
|
id="g96" /><g
|
||||||
|
transform="translate(52.001)"
|
||||||
|
id="g98"><g
|
||||||
|
id="g100"><g
|
||||||
|
id="g102"><g
|
||||||
|
transform="translate(-9.286)"
|
||||||
|
id="g104"><g
|
||||||
|
id="g106"><g
|
||||||
|
transform="translate(-107.844,-95.785)"
|
||||||
|
id="g108"><text
|
||||||
|
id="text112"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMMI10;-inkscape-font-specification:CMMI10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,107.844,95.785)"><tspan
|
||||||
|
id="tspan110"
|
||||||
|
y="0"
|
||||||
|
x="0 5.8111844">λP</tspan></text>
|
||||||
|
<text
|
||||||
|
id="text116"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMR10;-inkscape-font-specification:CMR10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,121.435,95.785)"><tspan
|
||||||
|
id="tspan114"
|
||||||
|
y="0"
|
||||||
|
x="0">2</tspan></text>
|
||||||
|
<g
|
||||||
|
transform="translate(107.844,95.785)"
|
||||||
|
id="g118" /></g></g><g
|
||||||
|
transform="translate(9.286)"
|
||||||
|
id="g120" /></g></g></g><g
|
||||||
|
transform="translate(-102.602,-44.036)"
|
||||||
|
id="g122"><g
|
||||||
|
id="g124" /><g
|
||||||
|
transform="translate(50.601)"
|
||||||
|
id="g126"><g
|
||||||
|
id="g128"><g
|
||||||
|
id="g130"><g
|
||||||
|
transform="translate(-6.185)"
|
||||||
|
id="g132"><g
|
||||||
|
id="g134"><g
|
||||||
|
transform="translate(-58.944,-51.749)"
|
||||||
|
id="g136"><text
|
||||||
|
id="text140"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMMI10;-inkscape-font-specification:CMMI10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,58.944,51.749)"><tspan
|
||||||
|
id="tspan138"
|
||||||
|
y="0"
|
||||||
|
x="0 5.8111844">λω</tspan></text>
|
||||||
|
<g
|
||||||
|
transform="translate(64.756,50.354)"
|
||||||
|
id="g142"><path
|
||||||
|
id="path144"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.398;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 0,0 H 6.559" /></g><g
|
||||||
|
transform="translate(58.944,51.749)"
|
||||||
|
id="g146" /></g></g><g
|
||||||
|
transform="translate(6.185)"
|
||||||
|
id="g148" /></g></g></g><g
|
||||||
|
transform="translate(52.001)"
|
||||||
|
id="g150"><g
|
||||||
|
id="g152" /><g
|
||||||
|
transform="translate(55.89)"
|
||||||
|
id="g154"><g
|
||||||
|
id="g156"><g
|
||||||
|
id="g158"><g
|
||||||
|
transform="translate(-10.075)"
|
||||||
|
id="g160"><g
|
||||||
|
id="g162"><g
|
||||||
|
transform="translate(-162.945,-51.749)"
|
||||||
|
id="g164"><text
|
||||||
|
id="text168"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMMI10;-inkscape-font-specification:CMMI10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,162.945,51.749)"><tspan
|
||||||
|
id="tspan166"
|
||||||
|
y="0"
|
||||||
|
x="0 5.8111844 13.591975">λPω</tspan></text>
|
||||||
|
<g
|
||||||
|
transform="translate(176.537,50.354)"
|
||||||
|
id="g170"><path
|
||||||
|
id="path172"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.398;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 0,0 H 6.559" /></g><g
|
||||||
|
transform="translate(162.945,51.749)"
|
||||||
|
id="g174" /></g></g><g
|
||||||
|
transform="translate(10.075)"
|
||||||
|
id="g176" /></g></g></g><g
|
||||||
|
transform="translate(-158.492,-44.036)"
|
||||||
|
id="g178"><g
|
||||||
|
id="g180"><g
|
||||||
|
id="g182"><g
|
||||||
|
transform="translate(-7.887)"
|
||||||
|
id="g184"><g
|
||||||
|
id="g186"><g
|
||||||
|
transform="translate(-6.641,-7.713)"
|
||||||
|
id="g188"><text
|
||||||
|
id="text192"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMMI10;-inkscape-font-specification:CMMI10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,6.641,7.713)"><tspan
|
||||||
|
id="tspan190"
|
||||||
|
y="0"
|
||||||
|
x="0">λ</tspan></text>
|
||||||
|
<text
|
||||||
|
id="text196"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMSY10;-inkscape-font-specification:CMSY10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,12.453,7.713)"><tspan
|
||||||
|
id="tspan194"
|
||||||
|
y="0"
|
||||||
|
x="0">→</tspan></text>
|
||||||
|
<g
|
||||||
|
transform="translate(6.641,7.713)"
|
||||||
|
id="g198" /></g></g><g
|
||||||
|
transform="translate(7.887)"
|
||||||
|
id="g200" /></g></g></g><g
|
||||||
|
transform="translate(50.601)"
|
||||||
|
id="g202"><g
|
||||||
|
id="g204" /><g
|
||||||
|
transform="translate(52.001)"
|
||||||
|
id="g206"><g
|
||||||
|
id="g208"><g
|
||||||
|
id="g210"><g
|
||||||
|
transform="translate(-6.796)"
|
||||||
|
id="g212"><g
|
||||||
|
id="g214"><g
|
||||||
|
transform="translate(-110.334,-7.713)"
|
||||||
|
id="g216"><text
|
||||||
|
id="text220"
|
||||||
|
style="font-variant:normal;font-weight:normal;font-size:9.96259975px;font-family:CMMI10;-inkscape-font-specification:CMMI10;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none"
|
||||||
|
transform="matrix(1,0,0,-1,110.334,7.713)"><tspan
|
||||||
|
id="tspan218"
|
||||||
|
y="0"
|
||||||
|
x="0 5.8111844">λP</tspan></text>
|
||||||
|
<g
|
||||||
|
transform="translate(110.334,7.713)"
|
||||||
|
id="g222" /></g></g><g
|
||||||
|
transform="translate(6.796)"
|
||||||
|
id="g224" /></g></g></g><g
|
||||||
|
transform="translate(-113.81)"
|
||||||
|
id="g226" /></g></g></g></g></g></g></g></g></g></g></g></g></g></g><g
|
||||||
|
transform="translate(91.548,68.735)"
|
||||||
|
id="g228" /></g></g><g
|
||||||
|
id="g230"><path
|
||||||
|
id="path232"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M -20.03418,66.0542 H 60.92348" /><g
|
||||||
|
transform="translate(60.92348,66.0542)"
|
||||||
|
id="g234"><g
|
||||||
|
id="g236"><path
|
||||||
|
id="path238"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g240"><path
|
||||||
|
id="path242"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M -71.42479,22.01807 H 2.56822" /><g
|
||||||
|
transform="translate(2.56822,22.01807)"
|
||||||
|
id="g244"><g
|
||||||
|
id="g246"><path
|
||||||
|
id="path248"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g250"><path
|
||||||
|
id="path252"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M -71.98294,29.29121 -43.289,54.25972" /><g
|
||||||
|
transform="matrix(0.75444,0.65646,-0.65646,0.75444,-43.289,54.25972)"
|
||||||
|
id="g254"><g
|
||||||
|
id="g256"><path
|
||||||
|
id="path258"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g260"><path
|
||||||
|
id="path262"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M -29.73921,-14.7449 V 51.89362" /><g
|
||||||
|
transform="rotate(90,-40.816415,11.077205)"
|
||||||
|
id="g264"><g
|
||||||
|
id="g266"><path
|
||||||
|
id="path268"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g270"><path
|
||||||
|
id="path272"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M -20.03418,-22.01805 H 57.67068" /><g
|
||||||
|
transform="translate(57.67068,-22.01805)"
|
||||||
|
id="g274"><g
|
||||||
|
id="g276"><path
|
||||||
|
id="path278"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g280"><path
|
||||||
|
id="path282"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M -80.34113,-58.78104 V 7.85748" /><g
|
||||||
|
transform="rotate(90,-44.099305,-36.241825)"
|
||||||
|
id="g284"><g
|
||||||
|
id="g286"><path
|
||||||
|
id="path288"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g290"><path
|
||||||
|
id="path292"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M -71.98294,-58.78104 -43.289,-33.81253" /><g
|
||||||
|
transform="matrix(0.75444,0.65646,-0.65646,0.75444,-43.289,-33.81253)"
|
||||||
|
id="g294"><g
|
||||||
|
id="g296"><path
|
||||||
|
id="path298"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g300"><path
|
||||||
|
id="path302"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M -68.9341,-66.05418 H 5.05891" /><g
|
||||||
|
transform="translate(5.05891,-66.05418)"
|
||||||
|
id="g304"><g
|
||||||
|
id="g306"><path
|
||||||
|
id="path308"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g310"><path
|
||||||
|
id="path312"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 78.15315,-14.7449 V 51.89362" /><g
|
||||||
|
transform="rotate(90,13.129765,65.023385)"
|
||||||
|
id="g314"><g
|
||||||
|
id="g316"><path
|
||||||
|
id="path318"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g320"><path
|
||||||
|
id="path322"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 31.49377,29.29121 63.49562,54.50247" /><g
|
||||||
|
transform="matrix(0.7885,0.62122,-0.62122,0.7885,63.4956,54.50247)"
|
||||||
|
id="g324"><g
|
||||||
|
id="g326"><path
|
||||||
|
id="path328"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g330"><path
|
||||||
|
id="path332"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="m 31.49377,-58.78104 32.00185,25.21126" /><g
|
||||||
|
transform="matrix(0.7885,0.62122,-0.62122,0.7885,63.4956,-33.56978)"
|
||||||
|
id="g334"><g
|
||||||
|
id="g336"><path
|
||||||
|
id="path338"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g><g
|
||||||
|
id="g340"><path
|
||||||
|
id="path342"
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 22.26196,-58.78104 V 7.85748" /><g
|
||||||
|
transform="rotate(90,7.20224,15.05972)"
|
||||||
|
id="g344"><g
|
||||||
|
id="g346"><path
|
||||||
|
id="path348"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:10;stroke-dasharray:none;stroke-opacity:1"
|
||||||
|
d="M 5.87146,0 C 5.1504,0.14133 1.98094,0.94218 0,1.81369 V -1.81369 C 1.98094,-0.94218 5.1504,-0.14133 5.87146,0 Z" /></g></g></g></g></g></g></g></svg>
|
||||||
|
After Width: | Height: | Size: 24 KiB |
Loading…
Add table
Reference in a new issue