X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=e67e7d200a6807b1c5fb552290938d59bd3474c6;hb=04ffe68396b98bbf21bcd403ffba03b94eaebadc;hp=c543bb9d2f1816f8d95a5cd4369588ef2a57ec91;hpb=b2c1a95861424ba23e491e2b258f7413efbc1fba;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index c543bb9d2..e67e7d200 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -6,8 +6,8 @@ - - lambdadelta version 2 + + \lambda\delta home page @@ -19,240 +19,239 @@ [lambdadelta home] -
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
+
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" - of the System's syntactic items and reductions. -
-
+
+
+
+
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - - - + - + + + + + - - - - - - - + + + + - - - - - - - - - - - - - - - +
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}local typed abstraction *Γ ⊢ +λWⓐV→βno#i
-
+ 		+ home local typed declaration **Γ ⊢ -λWⓐV→βno#i
-
+ 		+ news global typed declaration ***Γ ⊢ pλWnonono$p
+ + documentation + + specification +
native type annotation *Γ ⊢ ⓝWnonoyesno
{X | Γ ⊢ X = V}local abbreviation *Γ ⊢ +δVnolocal →δyes#i + implementation +
-
+ 		+ foreword + + milestones + + version 2 + + version 2 + (background - core - applications) + library local definition **Γ ⊢ -δVnolocal →δno#i
+ + citations + + visibility + + version 1 + + version 1 +
global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono + helena +
-
* In terms only. - ** In terms and local environments only. - *** In global environments only. - **** Sort level k in terms only. -
-
Summary of the Specification
+ +
Summary of the Specification [spacer] +
Here is a numerical acount of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78].
- - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles247 characters366699nodes1091471sizesfiles360characters433402nodes1874774
propositionstheorems76lemmas748total824propositionstheorems130lemmas1286total1416
conceptsdeclared41defined77total118conceptsdeclared54defined89total143
+ +
Stage "B"
+ +
Stage "A": "Extending the Applicability Condition"
+ + + + + + -
Logical Structure of the Specification
-
The source files are grouped in planes and components - according to the following table. - A notation file covering the whole specification is provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). +
Logical Structure of the Specification [spacer] +
+
This table reports the specification's components and their planes.
- - - - + + + - - - - - - - - + + + + + + + + + + + + + + + + + + + - + + + - - - - - - - - - - + + + + + + + + + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + - + - - - - + + + + - + + + - + + + + - - - - - + + + - - - - - - - + + + - - - - - - + + + - - - - - - + + + - + + + + - - - - - - + + + + + - + + - - - + + + - - + + + + - - - - - - - - - - + + - - - - - - + + + - - + - - - - - + + + - - - - - + + + + - - - - - - + + + + - + + + + + + + - - - - - + + - - - - - - + + + - - - - - - + + + - - + - - - - + + - - - - - - + + + - - - + + + - - - - + + + + + + + - - - - - + + + - - + - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - + - + + + + - - - - + + + + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + - - + + + + - - - - + + + + + + - - - - - - - + + + - - - - - + + + - - + + + + - + + + - - - + + + - - + + + + + - - - - - - - - - - - + + + + + - + - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - - + + + + + + + + + + + + - + + + - - - - - - - - - - + + + - - + + + + + - - - + + - + + + - - - + + + + - - - - - + + + + - - - - - - - + + + - - + + + - - + + + + + + + + + + + + + + + + + + + - + + + + + - - - + + - + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -1046,10 +1340,6 @@
componentplanefiles + componentplanefiles
+
+
dynamic typing"big tree" parallel computationyprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )yprs_yprsygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )ygt_ygtexamplesterms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta +
+ 		+
+ 		+
+
+ + + +
+ 		+
+ 		+
+
dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⫃¡[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv +
+ 		+
+
+ +
+ 		stratified native validityshnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )
"big tree" parallel reductionypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) +
+
+
local env. ref. for stratified native validitylsubsv ( ? ⊢ ? ¡⊑[?,?] ? )lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv + +
+ 		snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve +
+ 		+
+
equivalencedecomposed rt-equivalencescpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )scpes_aaa scpes_cpcs scpes_scpes
+
+
stratified native validitysnv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_ssta snv_sstas snv_ssta_lpr snv_lpr snv_cpcs + context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs
+
equivalencecontext-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs + conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc
+
conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc + computationevaluation for context-sensitive rt-reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
+ +
+
computationcontext-sensitive extended evaluationcpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) + +
+ 		evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre
+ +
+

+ strongly normalizing qrst-computationfsb ( ⦥[?,?] ⦃?,?,?⦄ )fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )fsb_aaa fsb_csx
+
context-sensitive evaluationcpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre + strongly normalizing rt-computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx
+
+
strongly normalizing computationcsn_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csn_tstc_vector csn_aaa +
+ lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx
+
+
csn ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csn_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csn_lift csn_lpx + csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tsts_vector csx_aaa +
+
+
decomposed extended computationdxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )dxprs_lift dxprs_aaa dxprs_dxprs +
+ csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs
+ +
+ 		parallel qrst-computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg
context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )lpxs_ldrop lpxs_aaa lpxs_cpxs lpxs_lpxs +
+ +
+ 		+
+ 		fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs
+

cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_aaa cpxs_cpxs + decomposed rt-computationscpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )scpds_lift scpds_aaa scpds_scpds
+
+ +
+ 		context-sensitive rt-computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? )lprs_ldrop lprs_cprs lprs_lprs +
+
+
cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs + cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
+
+
local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊢ ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba + context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_drop lprs_cprs lprs_lprs
+
+ +
+
support for abstract computation propertiesacpacp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )acp_aaa + cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs +
+
reductioncontext-sensitive extended normal formscnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )cnx_lift cnx_crx cnx_cix + +
+ 		local env. ref. for generic reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba
+
+
context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_ldrop lpx_aaa + support for generic computation propertiesgcpgcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa
+
reductionparallel qrst-reductionfpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )fpbq_lift fpbq_aaa
+
+
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lift cpx_cix + fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpb_lift fpb_lleq fpb_fleq
+
+
context-sensitive extended irreducible formscix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ )cix_append cix_lift + normal forms for context-sensitive rt-reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix
+
+
context-sensitive extended reducible formscrx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ )crx_append crx_lift + context-sensitive rt-reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_frees lpx_lleq lpx_aaa
+
+ +
+
context-sensitive normal formscnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir + cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix
+
+
context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_ldrop lpr_lpr + irreducible forms for context-sensitive rt-reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift
+
+
+ reducible forms for context-sensitive rt-reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift
cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_cir +
+
+
+ 		normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir +
+
+
context-sensitive irreducible formscir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ )cir_append cir_lift + context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr
+
+ +
+
context-sensitive reducible formscrr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ )crr_append crr_lift + cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir
+
unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) +
+ irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift
+
+
iterated stratified static type assignmentsstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )sstas_lift sstas_aaa sstas_sstas + reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift
+
static typingstratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ⦃?,?⦄ )ssta_lift ssta_aaa ssta_ssta + unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )
+ +
+
+ +
+ 		iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas
local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba + +
+
static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ⫃▪[?,?] ? )lsubd_da lsubd_lsubd
+
+
atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_aaa + degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_da
+
+
parametersshsd + parametersshsd
+
substitutionrestricted local env. ref.lsubr ( ? ⊑ ? )lsubr_lsubr + +
+ 		local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_aaa lsuba_lsuba
+
+
iterated structural successor for closuresfsups ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )fsups_fsups + atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
+
+ +
+ 		restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr
+
fsupp ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )fsupp_fsupp +
multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq
+
+
generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldrop ldrops_ldrops +
+ lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq +
+
+
generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector + lazy pointwise extension of a relationllpx_snllpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor
+
+ +
+ 		pointwise union for local environmentsllor ( ? ⋓[?,?] ? ≡ ? )llor_alt llor_drop
+ +
+

lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts + context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_lreq frees_lift
+
+ +
+ 		contxt-sensitive multiple rt-substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys
support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
relocationstructural successor for closuresfsup ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )fsupq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )fsupq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ ) + +
+ 		iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus +
+
+ +
+
global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop + fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup
+
+
basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_append ldrop_lpx_sn ldrop_ldrop + iterated local env. slicingdrops ( ⬇*[?,?] ? ≡ ? )drops_drop drops_drops
+
+
basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector + generic term relocationlifts_vector ( ⬆*[?] ? ≡ ? )lifts_lift_vector
+
+
+
lift ( ⇧[?,?] ? ≡ ? )lift_lift + lifts ( ⬆*[?] ? ≡ ? )lifts_lift lifts_lifts
+
grammarpointwise extension of a relationlpx_snlpx_sn_tc lpx_sn_lpx_sn +
+ support for multiple relocationmr2 ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )mr2_mr2
substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ ) +
+
+ +
+ 		+
+ 		fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector +
+
+
closurescl_shift ( ? @@ ? )cl_weight ( ♯{?,?,?} ) + global env. slicinggget ( ⬇[?] ? ≡ ? )gget_gget
+
+ +
+ 		contxt-sensitive ordinary rt-substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy +
+
internal syntaxgenv +

+ local env. ref. for rt-substitutionlsuby ( ? ⊆[?,?] ? )lsuby_lsuby
+
+
+ pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn +
+
lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )
+ +
+ 		basic local env. slicingdrop ( ⬇[?,?,?] ? ≡ ? )drop_append drop_lreq drop_drop
+
termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector
+
+ basic term relocationlift_vector ( ⬆[?,?] ? ≡ ? )lift_lift_vector
item + +
+

+
+ lift ( ⬆[?,?] ? ≡ ? )lift_neq lift_lift +
+ 		+
+
grammarequivalence for local environmentslreq ( ? ⩬[?,?] ? )lreq_lreq +
+ 		+
+
+
+ 		same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector +
+
+ +
+ 		closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} ) +
+
external syntaxaarity +

+ internal syntaxgenv +
+ 		+
+ 		+
+

+ +
+ 		lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )
+
+ 		+
+ 		termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )
+
+ 		+
+ 		item +
+ 		+
+ 		+
+
+
+ 		external syntaxaarity +
+ 		+
+
-
Physical Structure of the Specification
-
The source files are grouped in directories, - one for each component. -
[Spacer]
@@ -1076,6 +1366,6 @@

-
Last update: Wed, 07 Aug 2013 23:40:05 +0200
+
Last update: Tue, 04 Nov 2014 16:28:52 +0100