<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:39 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:39 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:39 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<tr>
<td class="snns capitalize italic cyan">sizes</td>
<td class="snns italic cyan">files</td>
- <td class="snnn right italic cyan">143</td>
+ <td class="snnn right italic cyan">133</td>
<td class="snns italic cyan">characters</td>
- <td class="snnn right italic cyan">116151</td>
+ <td class="snnn right italic cyan">92667</td>
<td class="snns italic cyan">nodes</td>
- <td class="ssnn right italic cyan">604153</td>
+ <td class="ssnn right italic cyan">334596</td>
</tr>
<tr>
<td class="snns capitalize italic green">propositions</td>
<td class="snns italic green">theorems</td>
- <td class="snnn right italic green">45</td>
+ <td class="snnn right italic green">44</td>
<td class="snns italic green">lemmas</td>
- <td class="snnn right italic green">428</td>
+ <td class="snnn right italic green">369</td>
<td class="snns italic green">total</td>
- <td class="ssnn right italic green">473</td>
+ <td class="ssnn right italic green">413</td>
</tr>
<tr>
<td class="snss capitalize italic yellow">concepts</td>
<td class="snss italic yellow">declared</td>
- <td class="snsn right italic yellow">23</td>
+ <td class="snsn right italic yellow">22</td>
<td class="snss italic yellow">defined</td>
- <td class="snsn right italic yellow">33</td>
+ <td class="snsn right italic yellow">32</td>
<td class="snss italic yellow">total</td>
- <td class="sssn right italic yellow">56</td>
+ <td class="sssn right italic yellow">54</td>
</tr>
</tbody>
</table>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:39 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:38 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:39 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<td class="snns italic cyan">files</td>
<td class="snnn right italic cyan">86</td>
<td class="snns italic cyan">characters</td>
- <td class="snnn right italic cyan">109249</td>
+ <td class="snnn right italic cyan">98269</td>
<td class="snns italic cyan">nodes</td>
- <td class="ssnn right italic cyan">217872</td>
+ <td class="ssnn right italic cyan">207871</td>
</tr>
<tr>
<td class="snns capitalize italic green">propositions</td>
<td class="snns italic green">theorems</td>
- <td class="snnn right italic green">30</td>
+ <td class="snnn right italic green">23</td>
<td class="snns italic green">lemmas</td>
- <td class="snnn right italic green">506</td>
+ <td class="snnn right italic green">497</td>
<td class="snns italic green">total</td>
- <td class="ssnn right italic green">536</td>
+ <td class="ssnn right italic green">520</td>
</tr>
<tr>
<td class="snss capitalize italic yellow">concepts</td>
<td class="snss italic yellow">declared</td>
- <td class="snsn right italic yellow">59</td>
- <td class="snss italic yellow">defined</td>
<td class="snsn right italic yellow">55</td>
+ <td class="snss italic yellow">defined</td>
+ <td class="snsn right italic yellow">57</td>
<td class="snss italic yellow">total</td>
- <td class="sssn right italic yellow">114</td>
+ <td class="sssn right italic yellow">112</td>
</tr>
</tbody>
</table>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:39 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:38 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:38 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:37 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
<tr>
<td class="snns top capitalize italic gray">version</td>
<td class="snnn top capitalize italic gray">name</td>
- <td class="snnn top capitalize italic gray">developed with</td>
<td class="snnn top capitalize italic gray">stage</td>
+ <td class="snnn top capitalize italic gray">developed with</td>
<td class="snnn top capitalize italic gray">started</td>
<td class="snnn top capitalize italic gray">announced</td>
<td class="snnn top capitalize italic gray">released</td>
<a href="http://lambdadelta.info/specification.html#v2">Version 2</a>
</td>
<td class="snnn top orange">"basic_2"</td>
+ <td class="snns top orange">"A2"</td>
<td class="snnn top orange">
- <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
+ <a href="http://matita.cs.unibo.it/">Matita 0.99.3</a>
</td>
- <td class="snns top orange">"A2"</td>
<td class="snnn top orange">October 2015</td>
<td class="snnn top orange" />
<td class="snnn top orange" />
<td class="snnn top orange" />
- <td class="ssnn top orange">
- <br />
- </td>
+ <td class="ssnn top orange" />
</tr>
<tr>
<td class="nnns top orange">
<td class="nnnn top orange">
<br />
</td>
- <td class="nnnn top orange">
- <br />
- </td>
<td class="snns top orange">"A1"</td>
+ <td class="snnn top orange">
+ <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
+ </td>
<td class="snnn top orange">April 2011</td>
<td class="snnn top orange">June 2014</td>
<td class="snnn top orange">October 2014</td>
<tr>
<td class="snns top orange">Abandoned</td>
<td class="snnn top orange" />
+ <td class="snnn top orange" />
<td class="snnn top orange">
<a href="http://coq.inria.fr/">Coq 7.3.1</a>
</td>
- <td class="snnn top orange" />
<td class="snnn top orange">March 2008</td>
<td class="snnn top orange" />
<td class="snnn top orange" />
<td class="snnn top orange">February 2011</td>
- <td class="ssnn top orange">
- <br />
- </td>
+ <td class="ssnn top orange" />
</tr>
<tr>
<td class="snss top red">
<a href="http://lambdadelta.info/specification.html#v1">Version 1</a>
</td>
<td class="snsn top red">"basic_1"</td>
+ <td class="snsn top red" />
<td class="snsn top red">
<a href="http://coq.inria.fr/">Coq 7.3.1</a>
</td>
- <td class="snsn top red" />
<td class="snsn top red">May 2004</td>
<td class="snsn top red">December 2005</td>
<td class="snsn top red">November 2006</td>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 May 2016 22:22:39 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 11:12:18 +0200</div>
</body>
</html>
table {
class "gray"
- [ "version" "name" "developed with"
- "stage" "started" "announced" "released" "concluded"
+ [ "version" "name"
+ "stage" "developed with"
+ "started" "announced" "released" "concluded"
"references"
]
class "yellow"
- [ @@("specification#v3" "Version 3") "\"basic_3\"" ""
- "" "" "" "" ""
+ [ @@("specification#v3" "Version 3") "\"basic_3\""
+ "" ""
+ "" "" "" ""
@@("documentation#ldJ3a" "J3a")
]
class "orange" {
[ { @@("specification#v2" "Version 2") * }
{ "\"basic_2\"" * }
- { @("http://matita.cs.unibo.it/" "Matita 0.99.2") * }
- { [ "\"A2\"" "October 2015" "" "" ""
- *
+ { [ "\"A2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.3")
+ "October 2015" "" "" ""
+ "" *
]
- [ "\"A1\"" "April 2011" "June 2014" "October 2014" "August 2015"
- @@("documentation#ldV2a" "V2a") + " " + @@("documentation#ldR2c" "R2c")
+ [ "\"A1\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
+ "April 2011" "June 2014" "October 2014" "August 2015"
+ @@("documentation#ldV2a" "V2a") + " " + @@("documentation#ldR2c" "R2c") *
]
}
]
- [ "Abandoned" "" @("http://coq.inria.fr/" "Coq 7.3.1")
- "" "March 2008" "" "" "February 2011" *
+ [ "Abandoned" ""
+ "" @("http://coq.inria.fr/" "Coq 7.3.1")
+ "March 2008" "" "" "February 2011"
+ "" *
]
}
class "red"
- [ @@("specification#v1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1")
- "" "May 2004" "December 2005" "November 2006" "May 2008"
- @@("documentation#ldV1a" "V1a") + " " + @@("documentation#ldJ1a" "J1a")
+ [ @@("specification#v1" "Version 1") "\"basic_1\""
+ "" @("http://coq.inria.fr/" "Coq 7.3.1")
+ "May 2004" "December 2005" "November 2006" "May 2008"
+ @@("documentation#ldV1a" "V1a") + " " + @@("documentation#ldJ1a" "J1a") *
]
}
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 c , break term 46 h ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PRed $c $h $G $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ break [ term 46 h ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedTy $h $G $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ break [ term 46 c , break term 46 h ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedTy $c $h $G $L $T1 $T2 }.
(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION ON TERMS ****)
definition cpxe: ∀h. sd h → relation4 genv lenv term term ≝
- λh,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 â\88§ â¦\83G, Lâ¦\84 â\8a¢ â\9e¡[h, o] 𝐍⦃T2⦄.
+ λh,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 â\88§ â¦\83G, Lâ¦\84 â\8a¢ â¬\88[h, o] 𝐍⦃T2⦄.
interpretation "evaluation for context-sensitive extended parallel reduction (term)"
'PRedEval h o G L T1 T2 = (cpxe h o G L T1 T2).
(* Basic properties *********************************************************)
-lemma csx_cpxe: â\88\80h,o,G,L,T1. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] T1 â\86\92 â\88\83T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] 𝐍⦃T2⦄.
+lemma csx_cpxe: â\88\80h,o,G,L,T1. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] T1 â\86\92 â\88\83T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] 𝐍⦃T2⦄.
#h #o #G #L #T1 #H @(csx_ind … H) -T1
#T1 #_ #IHT1 elim (cnx_dec h o G L T1) /3 width=3 by ex_intro, conj/
* #T #H1T1 #H2T1 elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1
(* Basic eliminators ********************************************************)
lemma cpxs_ind: ∀h,o,G,L,T1. ∀R:predicate term. R T1 →
- (â\88\80T,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡[h, o] T2 → R T → R T2) →
- â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 → R T2.
+ (â\88\80T,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[h, o] T2 → R T → R T2) →
+ â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 → R T2.
#h #o #L #G #T1 #R #HT1 #IHT1 #T2 #HT12
@(TC_star_ind … HT1 IHT1 … HT12) //
qed-.
lemma cpxs_ind_dx: ∀h,o,G,L,T2. ∀R:predicate term. R T2 →
- (â\88\80T1,T. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[h, o] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[h, o] T2 → R T → R T1) →
- â\88\80T1. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 → R T1.
+ (â\88\80T1,T. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h, o] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h, o] T2 → R T → R T1) →
+ â\88\80T1. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 → R T1.
#h #o #G #L #T2 #R #HT2 #IHT2 #T1 #HT12
@(TC_star_ind_dx … HT2 IHT2 … HT12) //
qed-.
(* Basic properties *********************************************************)
-lemma cpxs_refl: â\88\80h,o,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[h, o] T.
+lemma cpxs_refl: â\88\80h,o,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h, o] T.
/2 width=1 by inj/ qed.
-lemma cpx_cpxs: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2.
+lemma cpx_cpxs: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2.
/2 width=1 by inj/ qed.
-lemma cpxs_strap1: â\88\80h,o,G,L,T1,T. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T →
- â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2.
+lemma cpxs_strap1: â\88\80h,o,G,L,T1,T. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T →
+ â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2.
normalize /2 width=3 by step/ qed.
-lemma cpxs_strap2: â\88\80h,o,G,L,T1,T. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[h, o] T →
- â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2.
+lemma cpxs_strap2: â\88\80h,o,G,L,T1,T. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h, o] T →
+ â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2.
normalize /2 width=3 by TC_strap/ qed.
lemma lsubr_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) lsubr.
/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/
qed-.
-lemma cprs_cpxs: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡* T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2.
+lemma cprs_cpxs: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88* T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2.
#h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/
qed.
lemma cpxs_sort: ∀h,o,G,L,s,d1. deg h o s d1 →
- â\88\80d2. d2 â\89¤ d1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â\9e¡*[h, o] ⋆((next h)^d2 s).
+ â\88\80d2. d2 â\89¤ d1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â¬\88*[h, o] ⋆((next h)^d2 s).
#h #o #G #L #s #d1 #Hkd1 #d2 @(nat_ind_plus … d2) -d2 /2 width=1 by cpx_cpxs/
#d2 #IHd2 #Hd21 >iter_SO
@(cpxs_strap1 … (⋆(iter d2 ℕ (next h) s)))
]
qed.
-lemma cpxs_bind_dx: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, o] V2 →
- â\88\80I,T1,T2. â¦\83G, L. â\93\91{I}V1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â\88\80a. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{a,I}V1.T1 â\9e¡*[h, o] ⓑ{a,I}V2.T2.
+lemma cpxs_bind_dx: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h, o] V2 →
+ â\88\80I,T1,T2. â¦\83G, L. â\93\91{I}V1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â\88\80a. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{a,I}V1.T1 â¬\88*[h, o] ⓑ{a,I}V2.T2.
#h #o #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
/3 width=3 by cpxs_strap2, cpx_cpxs, cpx_pair_sn, cpx_bind/
qed.
-lemma cpxs_flat_dx: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, o] V2 →
- â\88\80T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â\88\80I. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.T1 â\9e¡*[h, o] ⓕ{I}V2.T2.
+lemma cpxs_flat_dx: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h, o] V2 →
+ â\88\80T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â\88\80I. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.T1 â¬\88*[h, o] ⓕ{I}V2.T2.
#h #o #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2
/3 width=5 by cpxs_strap1, cpx_cpxs, cpx_pair_sn, cpx_flat/
qed.
-lemma cpxs_flat_sn: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[h, o] T2 →
- â\88\80V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V2 →
- â\88\80I. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.T1 â\9e¡*[h, o] ⓕ{I}V2.T2.
+lemma cpxs_flat_sn: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h, o] T2 →
+ â\88\80V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V2 →
+ â\88\80I. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.T1 â¬\88*[h, o] ⓕ{I}V2.T2.
#h #o #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2
/3 width=5 by cpxs_strap1, cpx_cpxs, cpx_pair_sn, cpx_flat/
qed.
-lemma cpxs_pair_sn: â\88\80h,o,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V2 →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â\9e¡*[h, o] ②{I}V2.T.
+lemma cpxs_pair_sn: â\88\80h,o,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V2 →
+ â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â¬\88*[h, o] ②{I}V2.T.
#h #o #I #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
/3 width=3 by cpxs_strap1, cpx_pair_sn/
qed.
lemma cpxs_zeta: ∀h,o,G,L,V,T1,T,T2. ⬆[0, 1] T2 ≡ T →
- â¦\83G, L.â\93\93Vâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ +â\93\93V.T1 â\9e¡*[h, o] T2.
+ â¦\83G, L.â\93\93Vâ¦\84 â\8a¢ T1 â¬\88*[h, o] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ +â\93\93V.T1 â¬\88*[h, o] T2.
#h #o #G #L #V #T1 #T #T2 #HT2 #H @(cpxs_ind_dx … H) -T1
/3 width=3 by cpxs_strap2, cpx_cpxs, cpx_bind, cpx_zeta/
qed.
-lemma cpxs_eps: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â\88\80V. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV.T1 â\9e¡*[h, o] T2.
+lemma cpxs_eps: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â\88\80V. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV.T1 â¬\88*[h, o] T2.
#h #o #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_eps/
qed.
-lemma cpxs_ct: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V2 →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.T â\9e¡*[h, o] V2.
+lemma cpxs_ct: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V2 →
+ â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.T â¬\88*[h, o] V2.
#h #o #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ct/
qed.
lemma cpxs_beta_dx: ∀h,o,a,G,L,V1,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, o] V2 â\86\92 â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[h, o] W2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\9b{a}W1.T1 â\9e¡*[h, o] ⓓ{a}ⓝW2.V2.T2.
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h, o] V2 â\86\92 â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[h, o] W2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\9b{a}W1.T1 â¬\88*[h, o] ⓓ{a}ⓝW2.V2.T2.
#h #o #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2
/4 width=7 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/
qed.
lemma cpxs_theta_dx: ∀h,o,a,G,L,V1,V,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, o] V â\86\92 â¬\86[0, 1] V â\89¡ V2 â\86\92 â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[h, o] W2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{a}W1.T1 â\9e¡*[h, o] ⓓ{a}W2.ⓐV2.T2.
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h, o] V â\86\92 â¬\86[0, 1] V â\89¡ V2 â\86\92 â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[h, o] W2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{a}W1.T1 â¬\88*[h, o] ⓓ{a}W2.ⓐV2.T2.
#h #o #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2
/4 width=9 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma cpxs_inv_sort1: â\88\80h,o,G,L,U2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â\9e¡*[h, o] U2 →
+lemma cpxs_inv_sort1: â\88\80h,o,G,L,U2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â¬\88*[h, o] U2 →
∃∃n,d. deg h o s (n+d) & U2 = ⋆((next h)^n s).
#h #o #G #L #U2 #s #H @(cpxs_ind … H) -U2
[ elim (deg_total h o s) #d #Hkd
]
qed-.
-lemma cpxs_inv_cast1: â\88\80h,o,G,L,W1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dW1.T1 â\9e¡*[h, o] U2 →
- â\88¨â\88¨ â\88\83â\88\83W2,T2. â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡*[h, o] W2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 & U2 = ⓝW2.T2
- | â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] U2
- | â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡*[h, o] U2.
+lemma cpxs_inv_cast1: â\88\80h,o,G,L,W1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dW1.T1 â¬\88*[h, o] U2 →
+ â\88¨â\88¨ â\88\83â\88\83W2,T2. â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88*[h, o] W2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 & U2 = ⓝW2.T2
+ | â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] U2
+ | â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88*[h, o] U2.
#h #o #G #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/
#U2 #U #_ #HU2 * /3 width=3 by cpxs_strap1, or3_intro1, or3_intro2/ *
#W #T #HW1 #HT1 #H destruct
lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/
qed-.
-lemma cpxs_inv_cnx1: â\88\80h,o,G,L,T,U. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[h, o] U â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\9e¡[h, o] 𝐍⦃T⦄ → T = U.
+lemma cpxs_inv_cnx1: â\88\80h,o,G,L,T,U. â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h, o] U â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¬\88[h, o] 𝐍⦃T⦄ → T = U.
#h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/
qed-.
-lemma cpxs_neq_inv_step_sn: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 → (T1 = T2 → ⊥) →
- â\88\83â\88\83T. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[h, o] T & T1 = T â\86\92 â\8a¥ & â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[h, o] T2.
+lemma cpxs_neq_inv_step_sn: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 → (T1 = T2 → ⊥) →
+ â\88\83â\88\83T. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h, o] T & T1 = T â\86\92 â\8a¥ & â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h, o] T2.
#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
[ #H elim H -H //
| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct
(* Properties about atomic arity assignment on terms ************************)
lemma cpxs_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
- â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+ â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
#h #o #G #L #T1 #A #HT1 #T2 #HT12
@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/
qed-.
-lemma cprs_aaa_conf: â\88\80G,L,T1,A. â¦\83G, Lâ¦\84 â\8a¢ T1 â\81\9d A â\86\92 â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+lemma cprs_aaa_conf: â\88\80G,L,T1,A. â¦\83G, Lâ¦\84 â\8a¢ T1 â\81\9d A â\86\92 â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
/3 width=5 by cpxs_aaa_conf, cprs_cpxs/ qed-.
theorem cpxs_trans: ∀h,o,G,L. Transitive … (cpxs h o G L).
normalize /2 width=3 by trans_TC/ qed-.
-theorem cpxs_bind: â\88\80h,o,a,I,G,L,V1,V2,T1,T2. â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\91{a,I}V1.T1 â\9e¡*[h, o] ⓑ{a,I}V2.T2.
+theorem cpxs_bind: â\88\80h,o,a,I,G,L,V1,V2,T1,T2. â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\91{a,I}V1.T1 â¬\88*[h, o] ⓑ{a,I}V2.T2.
#h #o #a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2
/3 width=5 by cpxs_trans, cpxs_bind_dx/
qed.
-theorem cpxs_flat: â\88\80h,o,I,G,L,V1,V2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.T1 â\9e¡*[h, o] ⓕ{I}V2.T2.
+theorem cpxs_flat: â\88\80h,o,I,G,L,V1,V2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.T1 â¬\88*[h, o] ⓕ{I}V2.T2.
#h #o #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2
/3 width=5 by cpxs_trans, cpxs_flat_dx/
qed.
theorem cpxs_beta_rc: ∀h,o,a,G,L,V1,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, o] V2 â\86\92 â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡*[h, o] W2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\9b{a}W1.T1 â\9e¡*[h, o] ⓓ{a}ⓝW2.V2.T2.
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h, o] V2 â\86\92 â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88*[h, o] W2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\9b{a}W1.T1 â¬\88*[h, o] ⓓ{a}ⓝW2.V2.T2.
#h #o #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2
/4 width=5 by cpxs_trans, cpxs_beta_dx, cpxs_bind_dx, cpx_pair_sn/
qed.
theorem cpxs_beta: ∀h,o,a,G,L,V1,V2,W1,W2,T1,T2.
- â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡*[h, o] W2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\9b{a}W1.T1 â\9e¡*[h, o] ⓓ{a}ⓝW2.V2.T2.
+ â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88*[h, o] W2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\9b{a}W1.T1 â¬\88*[h, o] ⓓ{a}ⓝW2.V2.T2.
#h #o #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2
/4 width=5 by cpxs_trans, cpxs_beta_rc, cpxs_bind_dx, cpx_flat/
qed.
theorem cpxs_theta_rc: ∀h,o,a,G,L,V1,V,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, o] V → ⬆[0, 1] V ≡ V2 →
- â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡*[h, o] W2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{a}W1.T1 â\9e¡*[h, o] ⓓ{a}W2.ⓐV2.T2.
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h, o] V → ⬆[0, 1] V ≡ V2 →
+ â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88*[h, o] W2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{a}W1.T1 â¬\88*[h, o] ⓓ{a}W2.ⓐV2.T2.
#h #o #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cpxs_ind … H) -W2
/3 width=5 by cpxs_trans, cpxs_theta_dx, cpxs_bind_dx/
qed.
theorem cpxs_theta: ∀h,o,a,G,L,V1,V,V2,W1,W2,T1,T2.
- â¬\86[0, 1] V â\89¡ V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡*[h, o] W2 →
- â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{a}W1.T1 â\9e¡*[h, o] ⓓ{a}W2.ⓐV2.T2.
+ â¬\86[0, 1] V â\89¡ V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88*[h, o] W2 →
+ â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{a}W1.T1 â¬\88*[h, o] ⓓ{a}W2.ⓐV2.T2.
#h #o #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1
/3 width=5 by cpxs_trans, cpxs_theta_rc, cpxs_flat_dx/
qed.
(* Advanced inversion lemmas ************************************************)
-lemma cpxs_inv_appl1: â\88\80h,o,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â\9e¡*[h, o] U2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 &
+lemma cpxs_inv_appl1: â\88\80h,o,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â¬\88*[h, o] U2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2 &
U2 = ⓐV2. T2
- | â\88\83â\88\83a,W,T. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] â\93\9b{a}W.T & â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}â\93\9dW.V1.T â\9e¡*[h, o] U2
- | â\88\83â\88\83a,V0,V2,V,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡*[h, o] V0 & ⬆[0,1] V0 ≡ V2 &
- â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] â\93\93{a}V.T & â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}V.â\93\90V2.T â\9e¡*[h, o] U2.
+ | â\88\83â\88\83a,W,T. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] â\93\9b{a}W.T & â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}â\93\9dW.V1.T â¬\88*[h, o] U2
+ | â\88\83â\88\83a,V0,V2,V,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88*[h, o] V0 & ⬆[0,1] V0 ≡ V2 &
+ â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] â\93\93{a}V.T & â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}V.â\93\90V2.T â¬\88*[h, o] U2.
#h #o #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5 by or3_intro0, ex3_2_intro/ ]
#U #U2 #_ #HU2 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
]
qed-.
-lemma cpx_bind2: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, o] V2 →
- â\88\80I,T1,T2. â¦\83G, L.â\93\91{I}V2â¦\84 â\8a¢ T1 â\9e¡[h, o] T2 →
- â\88\80a. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{a,I}V1.T1 â\9e¡*[h, o] ⓑ{a,I}V2.T2.
+lemma cpx_bind2: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h, o] V2 →
+ â\88\80I,T1,T2. â¦\83G, L.â\93\91{I}V2â¦\84 â\8a¢ T1 â¬\88[h, o] T2 →
+ â\88\80a. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{a,I}V1.T1 â¬\88*[h, o] ⓑ{a,I}V2.T2.
/4 width=5 by lpx_cpx_trans, cpxs_bind_dx, lpx_pair/ qed.
(* Advanced properties ******************************************************)
#h #o #G @b_c_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *)
qed-.
-lemma cpxs_bind2_dx: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h, o] V2 →
- â\88\80I,T1,T2. â¦\83G, L.â\93\91{I}V2â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â\88\80a. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{a,I}V1.T1 â\9e¡*[h, o] ⓑ{a,I}V2.T2.
+lemma cpxs_bind2_dx: â\88\80h,o,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h, o] V2 →
+ â\88\80I,T1,T2. â¦\83G, L.â\93\91{I}V2â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â\88\80a. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{a,I}V1.T1 â¬\88*[h, o] ⓑ{a,I}V2.T2.
/4 width=5 by lpx_cpxs_trans, cpxs_bind_dx, lpx_pair/ qed.
(* Properties on supclosure *************************************************)
lemma fqu_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡*[h, o] U2 → (T2 = U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h, o] U2 → (T2 = U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
#U2 #HVU2 @(ex3_intro … U2)
qed-.
lemma fquq_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡*[h, o] U2 → (T2 = U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h, o] U2 → (T2 = U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12
[ #H12 elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fquq, ex3_intro/
qed-.
lemma fqup_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡*[h, o] U2 → (T2 = U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h, o] U2 → (T2 = U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fqup, ex3_intro/
qed-.
lemma fqus_cpxs_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡*[h, o] U2 → (T2 = U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h, o] U2 → (T2 = U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12
[ #H12 elim (fqup_cpxs_trans_neq … H12 … HTU2 H) -T2
/3 width=4 by fqup_fqus, ex3_intro/
(* Advanced properties ******************************************************)
lemma cpxs_delta: ∀h,o,I,G,L,K,V,V2,i.
- â¬\87[i] L â\89¡ K.â\93\91{I}V â\86\92 â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡*[h, o] V2 →
- â\88\80W2. â¬\86[0, i+1] V2 â\89¡ W2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ #i â\9e¡*[h, o] W2.
+ â¬\87[i] L â\89¡ K.â\93\91{I}V â\86\92 â¦\83G, Kâ¦\84 â\8a¢ V â¬\88*[h, o] V2 →
+ â\88\80W2. â¬\86[0, i+1] V2 â\89¡ W2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ #i â¬\88*[h, o] W2.
#h #o #I #G #L #K #V #V2 #i #HLK #H elim H -V2
[ /3 width=9 by cpx_cpxs, cpx_delta/
| #V1 lapply (drop_fwd_drop2 … HLK) -HLK
qed.
lemma lstas_cpxs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 →
- â\88\80d1. â¦\83G, Lâ¦\84 â\8a¢ T1 â\96ª[h, o] d1 â\86\92 d2 â\89¤ d1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[h, o] T2.
+ â\88\80d1. â¦\83G, Lâ¦\84 â\8a¢ T1 â\96ª[h, o] d1 â\86\92 d2 â\89¤ d1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h, o] T2.
#h #o #G #L #T1 #T2 #d2 #H elim H -G -L -T1 -T2 -d2 //
[ /3 width=3 by cpxs_sort, da_inv_sort/
| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #d1 #H #Hd21
(* Advanced inversion lemmas ************************************************)
-lemma cpxs_inv_lref1: â\88\80h,o,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #i â\9e¡*[h, o] T2 →
+lemma cpxs_inv_lref1: â\88\80h,o,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #i â¬\88*[h, o] T2 →
T2 = #i ∨
- â\88\83â\88\83I,K,V1,T1. â¬\87[i] L â\89¡ K.â\93\91{I}V1 & â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡*[h, o] T1 &
+ â\88\83â\88\83I,K,V1,T1. â¬\87[i] L â\89¡ K.â\93\91{I}V1 & â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88*[h, o] T1 &
⬆[0, i+1] T1 ≡ T2.
#h #o #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
#T #T2 #_ #HT2 *
(* Properties on supclosure *************************************************)
-lemma fqu_cpxs_trans: â\88\80h,o,G1,G2,L1,L2,T2,U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡*[h, o] U2 →
+lemma fqu_cpxs_trans: â\88\80h,o,G1,G2,L1,L2,T2,U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h, o] U2 →
∀T1. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/
#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqu_cpx_trans … HT1 … HT2) -T
#T #HT1 #HT2 elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/
qed-.
-lemma fquq_cpxs_trans: â\88\80h,o,G1,G2,L1,L2,T2,U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡*[h, o] U2 →
+lemma fquq_cpxs_trans: â\88\80h,o,G1,G2,L1,L2,T2,U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h, o] U2 →
∀T1. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fquq_inv_gen … H) -H
[ #HT12 elim (fqu_cpxs_trans … HTU2 … HT12) /3 width=3 by fqu_fquq, ex2_intro/
| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
lemma fquq_lstas_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
∀U2,d1. ⦃G2, L2⦄ ⊢ T2 •*[h, d1] U2 →
∀d2. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d2 → d1 ≤ d2 →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
/3 width=5 by fquq_cpxs_trans, lstas_cpxs/ qed-.
-lemma fqup_cpxs_trans: â\88\80h,o,G1,G2,L1,L2,T2,U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡*[h, o] U2 →
+lemma fqup_cpxs_trans: â\88\80h,o,G1,G2,L1,L2,T2,U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h, o] U2 →
∀T1. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/
#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqup_cpx_trans … HT1 … HT2) -T
#U1 #HTU1 #H2 elim (IHTU2 … H2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/
qed-.
-lemma fqus_cpxs_trans: â\88\80h,o,G1,G2,L1,L2,T2,U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡*[h, o] U2 →
+lemma fqus_cpxs_trans: â\88\80h,o,G1,G2,L1,L2,T2,U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h, o] U2 →
∀T1. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fqus_inv_gen … H) -H
[ #HT12 elim (fqup_cpxs_trans … HTU2 … HT12) /3 width=3 by fqup_fqus, ex2_intro/
| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
lemma fqus_lstas_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
∀U2,d1. ⦃G2, L2⦄ ⊢ T2 •*[h, d1] U2 →
∀d2. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d2 → d1 ≤ d2 →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
/3 width=6 by fqus_cpxs_trans, lstas_cpxs/ qed-.
(* Properties on lazy equivalence for local environments ********************)
-lemma lleq_cpxs_trans: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â\88\80L1. L1 â\89¡[T1, 0] L2 â\86\92 â¦\83G, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2.
+lemma lleq_cpxs_trans: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â\88\80L1. L1 â\89¡[T1, 0] L2 â\86\92 â¦\83G, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2.
#h #o #G #L2 #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/4 width=6 by cpx_lleq_conf_dx, lleq_cpx_trans, cpxs_strap2/
qed-.
-lemma cpxs_lleq_conf: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
- â\88\80L1. L2 â\89¡[T1, 0] L1 â\86\92 â¦\83G, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2.
+lemma cpxs_lleq_conf: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
+ â\88\80L1. L2 â\89¡[T1, 0] L1 â\86\92 â¦\83G, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2.
/3 width=3 by lleq_cpxs_trans, lleq_sym/ qed-.
-lemma cpxs_lleq_conf_dx: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
+lemma cpxs_lleq_conf_dx: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
∀L1. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2.
#h #o #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by cpx_lleq_conf_dx/
qed-.
-lemma cpxs_lleq_conf_sn: â\88\80h,o,G,L1,T1,T2. â¦\83G, L1â¦\84 â\8a¢ T1 â\9e¡*[h, o] T2 →
+lemma cpxs_lleq_conf_sn: â\88\80h,o,G,L1,T1,T2. â¦\83G, L1â¦\84 â\8a¢ T1 â¬\88*[h, o] T2 →
∀L2. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2.
/4 width=6 by cpxs_lleq_conf_dx, lleq_sym/ qed-.
(* Forward lemmas involving same top term structure *************************)
-lemma cpxs_fwd_cnx: â\88\80h,o,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â\9e¡[h, o] ð\9d\90\8dâ¦\83Tâ¦\84 â\86\92 â\88\80U. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[h, o] U → T ≂ U.
+lemma cpxs_fwd_cnx: â\88\80h,o,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\88[h, o] ð\9d\90\8dâ¦\83Tâ¦\84 â\86\92 â\88\80U. â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h, o] U → T ≂ U.
#h #o #G #L #T #HT #U #H
>(cpxs_inv_cnx1 … H HT) -G -L -T //
qed-.
-lemma cpxs_fwd_sort: â\88\80h,o,G,L,U,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â\9e¡*[h, o] U →
- â\8b\86s â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\8b\86(next h s) â\9e¡*[h, o] U.
+lemma cpxs_fwd_sort: â\88\80h,o,G,L,U,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â¬\88*[h, o] U →
+ â\8b\86s â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\8b\86(next h s) â¬\88*[h, o] U.
#h #o #G #L #U #s #H
elim (cpxs_inv_sort1 … H) -H #n #d generalize in match s; -s @(nat_ind_plus … n) -n
[ #s #_ #H -d destruct /2 width=1 by or_introl/
qed-.
(* Basic_1: was just: pr3_iso_beta *)
-lemma cpxs_fwd_beta: â\88\80h,o,a,G,L,V,W,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{a}W.T â\9e¡*[h, o] U →
- â\93\90V.â\93\9b{a}W.T â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}â\93\9dW.V.T â\9e¡*[h, o] U.
+lemma cpxs_fwd_beta: â\88\80h,o,a,G,L,V,W,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{a}W.T â¬\88*[h, o] U →
+ â\93\90V.â\93\9b{a}W.T â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}â\93\9dW.V.T â¬\88*[h, o] U.
#h #o #a #G #L #V #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
(* Note: probably this is an inversion lemma *)
lemma cpxs_fwd_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 →
∀V2. ⬆[0, i + 1] V1 ≡ V2 →
- â\88\80U. â¦\83G, Lâ¦\84 â\8a¢ #i â\9e¡*[h, o] U →
- #i â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ V2 â\9e¡*[h, o] U.
+ â\88\80U. â¦\83G, Lâ¦\84 â\8a¢ #i â¬\88*[h, o] U →
+ #i â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ V2 â¬\88*[h, o] U.
#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/
* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
/4 width=10 by cpxs_lift, drop_fwd_drop2, or_intror/
qed-.
-lemma cpxs_fwd_theta: â\88\80h,o,a,G,L,V1,V,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{a}V.T â\9e¡*[h, o] U →
+lemma cpxs_fwd_theta: â\88\80h,o,a,G,L,V1,V,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{a}V.T â¬\88*[h, o] U →
∀V2. ⬆[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨
- â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}V.â\93\90V2.T â\9e¡*[h, o] U.
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}V.â\93\90V2.T â¬\88*[h, o] U.
#h #o #a #G #L #V1 #V #T #U #H #V2 #HV12
elim (cpxs_inv_appl1 … H) -H *
[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
]
qed-.
-lemma cpxs_fwd_cast: â\88\80h,o,G,L,W,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dW.T â\9e¡*[h, o] U →
- â\88¨â\88¨ â\93\9dW. T â\89\82 U | â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[h, o] U | â¦\83G, Lâ¦\84 â\8a¢ W â\9e¡*[h, o] U.
+lemma cpxs_fwd_cast: â\88\80h,o,G,L,W,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dW.T â¬\88*[h, o] U →
+ â\88¨â\88¨ â\93\9dW. T â\89\82 U | â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h, o] U | â¦\83G, Lâ¦\84 â\8a¢ W â¬\88*[h, o] U.
#h #o #G #L #W #T #U #H
elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
#W0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/
(* Vector form of forward lemmas involving same top term structure **********)
(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: â\88\80h,o,G,L,T. ð\9d\90\92â¦\83Tâ¦\84 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\9e¡[h, o] 𝐍⦃T⦄ →
- â\88\80Vs,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.T â\9e¡*[h, o] U → ⒶVs.T ≂ U.
+lemma cpxs_fwd_cnx_vector: â\88\80h,o,G,L,T. ð\9d\90\92â¦\83Tâ¦\84 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¬\88[h, o] 𝐍⦃T⦄ →
+ â\88\80Vs,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.T â¬\88*[h, o] U → ⒶVs.T ≂ U.
#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
#V #Vs #IHVs #U #H
elim (cpxs_inv_appl1 … H) -H *
]
qed-.
-lemma cpxs_fwd_sort_vector: â\88\80h,o,G,L,s,Vs,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\8b\86s â\9e¡*[h, o] U →
- â\92¶Vs.â\8b\86s â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\8b\86(next h s) â\9e¡*[h, o] U.
+lemma cpxs_fwd_sort_vector: â\88\80h,o,G,L,s,Vs,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\8b\86s â¬\88*[h, o] U →
+ â\92¶Vs.â\8b\86s â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\8b\86(next h s) â¬\88*[h, o] U.
#h #o #G #L #s #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
#V #Vs #IHVs #U #H
elim (cpxs_inv_appl1 … H) -H *
(* Basic_1: was just: pr3_iso_appls_beta *)
-lemma cpxs_fwd_beta_vector: â\88\80h,o,a,G,L,Vs,V,W,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\93\90V.â\93\9b{a}W.T â\9e¡*[h, o] U →
- â\92¶Vs. â\93\90V. â\93\9b{a}W. T â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\93\93{a}â\93\9dW.V.T â\9e¡*[h, o] U.
+lemma cpxs_fwd_beta_vector: â\88\80h,o,a,G,L,Vs,V,W,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\93\90V.â\93\9b{a}W.T â¬\88*[h, o] U →
+ â\92¶Vs. â\93\90V. â\93\9b{a}W. T â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\93\93{a}â\93\9dW.V.T â¬\88*[h, o] U.
#h #o #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
#V0 #Vs #IHVs #V #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
lemma cpxs_fwd_delta_vector: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 →
∀V2. ⬆[0, i + 1] V1 ≡ V2 →
- â\88\80Vs,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.#i â\9e¡*[h, o] U →
- â\92¶Vs.#i â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.V2 â\9e¡*[h, o] U.
+ â\88\80Vs,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.#i â¬\88*[h, o] U →
+ â\92¶Vs.#i â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.V2 â¬\88*[h, o] U.
#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/
#V #Vs #IHVs #U #H -K -V1
elim (cpxs_inv_appl1 … H) -H *
(* Basic_1: was just: pr3_iso_appls_abbr *)
lemma cpxs_fwd_theta_vector: ∀h,o,G,L,V1b,V2b. ⬆[0, 1] V1b ≡ V2b →
- â\88\80a,V,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶V1b.â\93\93{a}V.T â\9e¡*[h, o] U →
- â\92¶V1b. â\93\93{a}V. T â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}V.â\92¶V2b.T â\9e¡*[h, o] U.
+ â\88\80a,V,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶V1b.â\93\93{a}V.T â¬\88*[h, o] U →
+ â\92¶V1b. â\93\93{a}V. T â\89\82 U â\88¨ â¦\83G, Lâ¦\84 â\8a¢ â\93\93{a}V.â\92¶V2b.T â¬\88*[h, o] U.
#h #o #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/
#V1b #V2b #V1a #V2a #HV12a #HV12b #a
generalize in match HV12a; -HV12a
qed-.
(* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_cast_vector: â\88\80h,o,G,L,Vs,W,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\93\9dW.T â\9e¡*[h, o] U →
+lemma cpxs_fwd_cast_vector: â\88\80h,o,G,L,Vs,W,T,U. â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.â\93\9dW.T â¬\88*[h, o] U →
∨∨ ⒶVs. ⓝW. T ≂ U
- | â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.T â\9e¡*[h, o] U
- | â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.W â\9e¡*[h, o] U.
+ | â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.T â¬\88*[h, o] U
+ | â¦\83G, Lâ¦\84 â\8a¢ â\92¶Vs.W â¬\88*[h, o] U.
#h #o #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
#V #Vs #IHVs #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
include "ground_2/steps/rtc_shift.ma".
include "ground_2/steps/rtc_plus.ma".
-include "basic_2/notation/relations/pred_6.ma".
+include "basic_2/notation/relations/predty_6.ma".
include "basic_2/grammar/lenv.ma".
include "basic_2/grammar/genv.ma".
include "basic_2/relocation/lifts.ma".
interpretation
"counted context-sensitive parallel rt-transition (term)"
- 'PRed c h G L T1 T2 = (cpg h c G L T1 T2).
+ 'PRedTy c h G L T1 T2 = (cpg h c G L T1 T2).
(* Basic properties *********************************************************)
(* Note: this is "∀h,g,L. reflexive … (cpg h (𝟘𝟘) L)" *)
-lemma cpg_refl: â\88\80h,G,T,L. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡[𝟘𝟘, h] T.
+lemma cpg_refl: â\88\80h,G,T,L. â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[𝟘𝟘, h] T.
#h #G #T elim T -T // * /2 width=1 by cpg_bind, cpg_flat/
qed.
-lemma cpg_pair_sn: â\88\80c,h,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[c, h] V2 →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â\9e¡[↓c, h] ②{I}V2.T.
+lemma cpg_pair_sn: â\88\80c,h,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[c, h] V2 →
+ â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â¬\88[↓c, h] ②{I}V2.T.
#c #h * /2 width=1 by cpg_bind, cpg_flat/
qed.
(* Basic inversion lemmas ***************************************************)
-fact cpg_inv_atom1_aux: â\88\80c,h,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[c, h] T2 → ∀J. T1 = ⓪{J} →
+fact cpg_inv_atom1_aux: â\88\80c,h,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[c, h] T2 → ∀J. T1 = ⓪{J} →
∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘
| ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & J = LRef 0 & c = cV
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
- | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 &
+ | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[c, h] T & ⬆*[1] T ≡ T2 &
L = K.ⓑ{I}V & J = LRef (⫯i).
#c #h #G #L #T1 #T2 * -c -G -L -T1 -T2
[ #I #G #L #J #H destruct /3 width=1 by or5_intro0, conj/
]
qed-.
-lemma cpg_inv_atom1: â\88\80c,h,J,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{J} â\9e¡[c, h] T2 →
+lemma cpg_inv_atom1: â\88\80c,h,J,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{J} â¬\88[c, h] T2 →
∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘
| ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & J = LRef 0 & c = cV
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
- | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 &
+ | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[c, h] T & ⬆*[1] T ≡ T2 &
L = K.ⓑ{I}V & J = LRef (⫯i).
/2 width=3 by cpg_inv_atom1_aux/ qed-.
-lemma cpg_inv_sort1: â\88\80c,h,G,L,T2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â\9e¡[c, h] T2 →
+lemma cpg_inv_sort1: â\88\80c,h,G,L,T2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â¬\88[c, h] T2 →
(T2 = ⋆s ∧ c = 𝟘𝟘) ∨ (T2 = ⋆(next h s) ∧ c = 𝟘𝟙).
#c #h #G #L #T2 #s #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
]
qed-.
-lemma cpg_inv_zero1: â\88\80c,h,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #0 â\9e¡[c, h] T2 →
+lemma cpg_inv_zero1: â\88\80c,h,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #0 â¬\88[c, h] T2 →
∨∨ (T2 = #0 ∧ c = 𝟘𝟘)
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & c = cV
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & c = (↓cV)+𝟘𝟙.
#c #h #G #L #T2 #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/
]
qed-.
-lemma cpg_inv_lref1: â\88\80c,h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i â\9e¡[c, h] T2 →
+lemma cpg_inv_lref1: â\88\80c,h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i â¬\88[c, h] T2 →
(T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨
- â\88\83â\88\83I,K,V,T. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
+ â\88\83â\88\83I,K,V,T. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
#c #h #G #L #T2 #i #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
[ #s #H destruct
]
qed-.
-lemma cpg_inv_gref1: â\88\80c,h,G,L,T2,l. â¦\83G, Lâ¦\84 â\8a¢ §l â\9e¡[c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
+lemma cpg_inv_gref1: â\88\80c,h,G,L,T2,l. â¦\83G, Lâ¦\84 â\8a¢ §l â¬\88[c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
#c #h #G #L #T2 #l #H
elim (cpg_inv_atom1 … H) -H * /2 width=1 by conj/
[ #s #H destruct
]
qed-.
-fact cpg_inv_bind1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡[c, h] U2 →
+fact cpg_inv_bind1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â¬\88[c, h] U2 →
∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → (
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\91{J}V1â¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\91{J}V1â¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓑ{p,J}V2.T2 & c = (↓cV)+cT
) ∨
- â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ U1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+ â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ U1 â¬\88[cT, h] T & ⬆*[1] U2 ≡ T &
p = true & J = Abbr & c = (↓cT)+𝟙𝟘.
#c #h #G #L #U #U2 * -c -G -L -U -U2
[ #I #G #L #q #J #W #U1 #H destruct
]
qed-.
-lemma cpg_inv_bind1: â\88\80c,h,p,I,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[c, h] U2 → (
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_bind1: â\88\80c,h,p,I,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[c, h] U2 → (
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U2 = ⓑ{p,I}V2.T2 & c = (↓cV)+cT
) ∨
- â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+ â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T & ⬆*[1] U2 ≡ T &
p = true & I = Abbr & c = (↓cT)+𝟙𝟘.
/2 width=3 by cpg_inv_bind1_aux/ qed-.
-lemma cpg_inv_abbr1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 â\9e¡[c, h] U2 → (
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_abbr1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 â¬\88[c, h] U2 → (
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U2 = ⓓ{p}V2.T2 & c = (↓cV)+cT
) ∨
- â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+ â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T & ⬆*[1] U2 ≡ T &
p = true & c = (↓cT)+𝟙𝟘.
#c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
/3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/
qed-.
-lemma cpg_inv_abst1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 â\9e¡[c, h] U2 →
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\9bV1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_abst1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 â¬\88[c, h] U2 →
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\9bV1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U2 = ⓛ{p}V2.T2 & c = (↓cV)+cT.
#c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
[ /3 width=8 by ex4_4_intro/
]
qed-.
-fact cpg_inv_flat1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡[c, h] U2 →
+fact cpg_inv_flat1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â¬\88[c, h] U2 →
∀J,V1,U1. U = ⓕ{J}V1.U1 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓕ{J}V2.T2 & c = (↓cV)+cT
- | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & J = Cast & c = (↓cT)+𝟙𝟘
- | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & J = Cast & c = (↓cV)+𝟘𝟙
- | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & J = Cast & c = (↓cT)+𝟙𝟘
+ | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] U2 & J = Cast & c = (↓cV)+𝟘𝟙
+ | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
- | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
#c #h #G #L #U #U2 * -c -G -L -U -U2
[ #I #G #L #J #W #U1 #H destruct
]
qed-.
-lemma cpg_inv_flat1: â\88\80c,h,I,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 â\9e¡[c, h] U2 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_flat1: â\88\80c,h,I,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 â¬\88[c, h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓕ{I}V2.T2 & c = (↓cV)+cT
- | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & I = Cast & c = (↓cT)+𝟙𝟘
- | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & I = Cast & c = (↓cV)+𝟘𝟙
- | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & I = Cast & c = (↓cT)+𝟙𝟘
+ | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] U2 & I = Cast & c = (↓cV)+𝟘𝟙
+ | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
- | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
/2 width=3 by cpg_inv_flat1_aux/ qed-.
-lemma cpg_inv_appl1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.U1 â\9e¡[c, h] U2 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_appl1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.U1 â¬\88[c, h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓐV2.T2 & c = (↓cV)+cT
- | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
- | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
#c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
[ /3 width=8 by or3_intro0, ex4_4_intro/
]
qed-.
-lemma cpg_inv_cast1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.U1 â\9e¡[c, h] U2 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_cast1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.U1 â¬\88[c, h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓝV2.T2 & c = (↓cV)+cT
- | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & c = (↓cT)+𝟙𝟘
- | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & c = (↓cV)+𝟘𝟙.
+ | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & c = (↓cT)+𝟙𝟘
+ | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] U2 & c = (↓cV)+𝟘𝟙.
#c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
[ /3 width=8 by or3_intro0, ex4_4_intro/
|2,3: /3 width=3 by or3_intro1, or3_intro2, ex2_intro/
(* Basic forward lemmas *****************************************************)
-lemma cpg_fwd_bind1_minus: â\88\80c,h,I,G,L,V1,T1,T. â¦\83G, Lâ¦\84 â\8a¢ -â\93\91{I}V1.T1 â\9e¡[c, h] T → ∀p.
- â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[c, h] ⓑ{p,I}V2.T2 &
+lemma cpg_fwd_bind1_minus: â\88\80c,h,I,G,L,V1,T1,T. â¦\83G, Lâ¦\84 â\8a¢ -â\93\91{I}V1.T1 â¬\88[c, h] T → ∀p.
+ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[c, h] ⓑ{p,I}V2.T2 &
T = -ⓑ{I}V2.T2.
#c #h #I #G #L #V1 #T1 #T #H #p elim (cpg_inv_bind1 … H) -H *
[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct /3 width=4 by cpg_bind, ex2_2_intro/
(* Advanced properties ******************************************************)
-lemma cpg_delta_drops: â\88\80c,h,G,K,V,V2,i,L,T2. â¬\87*[i] L â\89¡ K.â\93\93V â\86\92 â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[c, h] V2 →
- â¬\86*[⫯i] V2 â\89¡ T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ #i â\9e¡[c, h] T2.
+lemma cpg_delta_drops: â\88\80c,h,G,K,V,V2,i,L,T2. â¬\87*[i] L â\89¡ K.â\93\93V â\86\92 â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[c, h] V2 →
+ â¬\86*[⫯i] V2 â\89¡ T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ #i â¬\88[c, h] T2.
#c #h #G #K #V #V2 #i elim i -i
[ #L #T2 #HLK lapply (drops_fwd_isid … HLK ?) // #H destruct /3 width=3 by cpg_delta/
| #i #IH #L0 #T0 #H0 #HV2 #HVT2
]
qed.
-lemma cpg_ell_drops: â\88\80c,h,G,K,V,V2,i,L,T2. â¬\87*[i] L â\89¡ K.â\93\9bV â\86\92 â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[c, h] V2 →
- â¬\86*[⫯i] V2 â\89¡ T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ #i â\9e¡[(↓c)+𝟘𝟙, h] T2.
+lemma cpg_ell_drops: â\88\80c,h,G,K,V,V2,i,L,T2. â¬\87*[i] L â\89¡ K.â\93\9bV â\86\92 â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[c, h] V2 →
+ â¬\86*[⫯i] V2 â\89¡ T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ #i â¬\88[(↓c)+𝟘𝟙, h] T2.
#c #h #G #K #V #V2 #i elim i -i
[ #L #T2 #HLK lapply (drops_fwd_isid … HLK ?) // #H destruct /3 width=3 by cpg_ell/
| #i #IH #L0 #T0 #H0 #HV2 #HVT2
(* Advanced inversion lemmas ************************************************)
-lemma cpg_inv_lref1_drops: â\88\80c,h,G,i,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #i â\9e¡[c, h] T2 →
+lemma cpg_inv_lref1_drops: â\88\80c,h,G,i,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #i â¬\88[c, h] T2 →
∨∨ T2 = #i ∧ c = 𝟘𝟘
- | â\88\83â\88\83cV,K,V,V2. â¬\87*[i] L â\89¡ K.â\93\93V & â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[cV, h] V2 &
+ | â\88\83â\88\83cV,K,V,V2. â¬\87*[i] L â\89¡ K.â\93\93V & â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & c = cV
- | â\88\83â\88\83cV,K,V,V2. â¬\87*[i] L â\89¡ K.â\93\9bV & â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[cV, h] V2 &
+ | â\88\83â\88\83cV,K,V,V2. â¬\87*[i] L â\89¡ K.â\93\9bV & â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & c = (↓cV) + 𝟘𝟙.
#c #h #G #i elim i -i
[ #L #T2 #H elim (cpg_inv_zero1 … H) -H * /3 width=1 by or3_intro0, conj/
]
qed-.
-lemma cpg_inv_atom1_drops: â\88\80c,h,I,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{I} â\9e¡[c, h] T2 →
+lemma cpg_inv_atom1_drops: â\88\80c,h,I,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{I} â¬\88[c, h] T2 →
∨∨ T2 = ⓪{I} ∧ c = 𝟘𝟘
| ∃∃s. T2 = ⋆(next h s) & I = Sort s & c = 𝟘𝟙
- | â\88\83â\88\83cV,i,K,V,V2. â¬\87*[i] L â\89¡ K.â\93\93V & â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[cV, h] V2 &
+ | â\88\83â\88\83cV,i,K,V,V2. â¬\87*[i] L â\89¡ K.â\93\93V & â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV
- | â\88\83â\88\83cV,i,K,V,V2. â¬\87*[i] L â\89¡ K.â\93\9bV & â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[cV, h] V2 &
+ | â\88\83â\88\83cV,i,K,V,V2. â¬\87*[i] L â\89¡ K.â\93\9bV & â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = (↓cV) + 𝟘𝟙.
#c #h * #n #G #L #T2 #H
[ elim (cpg_inv_sort1 … H) -H *
(* Properties with simple terms *********************************************)
(* Note: the main property of simple terms *)
-lemma cpg_inv_appl1_simple: â\88\80c,h,G,L,V1,T1,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â\9e¡[c, h] U → 𝐒⦃T1⦄ →
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_appl1_simple: â\88\80c,h,G,L,V1,T1,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â¬\88[c, h] U → 𝐒⦃T1⦄ →
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U = ⓐV2.T2 & c = (↓cV)+cT.
#c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *
[ /2 width=8 by ex4_4_intro/
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/pred_5.ma".
+include "basic_2/notation/relations/predty_5.ma".
include "basic_2/rt_transition/cpg.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS *****************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
definition cpx (h): relation4 genv lenv term term ≝
- λG,L,T1,T2. â\88\83c. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[c, h] T2.
+ λG,L,T1,T2. â\88\83c. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[c, h] T2.
interpretation
"uncounted context-sensitive parallel reduction (term)"
- 'PRed h G L T1 T2 = (cpx h G L T1 T2).
+ 'PRedTy h G L T1 T2 = (cpx h G L T1 T2).
(* Basic properties *********************************************************)
-lemma cpx_atom: â\88\80h,I,G,L. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{I} â\9e¡[h] ⓪{I}.
+lemma cpx_atom: â\88\80h,I,G,L. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{I} â¬\88[h] ⓪{I}.
/2 width=2 by cpg_atom, ex_intro/ qed.
(* Basic_2A1: was: cpx_st *)
-lemma cpx_ess: â\88\80h,G,L,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â\9e¡[h] ⋆(next h s).
+lemma cpx_ess: â\88\80h,G,L,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â¬\88[h] ⋆(next h s).
/2 width=2 by cpg_ess, ex_intro/ qed.
-lemma cpx_delta: â\88\80h,I,G,K,V1,V2,W2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[h] V2 →
- â¬\86*[1] V2 â\89¡ W2 â\86\92 â¦\83G, K.â\93\91{I}V1â¦\84 â\8a¢ #0 â\9e¡[h] W2.
+lemma cpx_delta: â\88\80h,I,G,K,V1,V2,W2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[h] V2 →
+ â¬\86*[1] V2 â\89¡ W2 â\86\92 â¦\83G, K.â\93\91{I}V1â¦\84 â\8a¢ #0 â¬\88[h] W2.
#h * #G #K #V1 #V2 #W2 *
/3 width=4 by cpg_delta, cpg_ell, ex_intro/
qed.
-lemma cpx_lref: â\88\80h,I,G,K,V,T,U,i. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[h] T →
- â¬\86*[1] T â\89¡ U â\86\92 â¦\83G, K.â\93\91{I}Vâ¦\84 â\8a¢ #⫯i â\9e¡[h] U.
+lemma cpx_lref: â\88\80h,I,G,K,V,T,U,i. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[h] T →
+ â¬\86*[1] T â\89¡ U â\86\92 â¦\83G, K.â\93\91{I}Vâ¦\84 â\8a¢ #⫯i â¬\88[h] U.
#h #I #G #K #V #T #U #i *
/3 width=4 by cpg_lref, ex_intro/
qed.
lemma cpx_bind: ∀h,p,I,G,L,V1,V2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 â\86\92 â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â\9e¡[h] T2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[h] ⓑ{p,I}V2.T2.
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 â\86\92 â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â¬\88[h] T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[h] ⓑ{p,I}V2.T2.
#h #p #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
/3 width=2 by cpg_bind, ex_intro/
qed.
lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[h] T2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.T1 â\9e¡[h] ⓕ{I}V2.T2.
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.T1 â¬\88[h] ⓕ{I}V2.T2.
#h #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
/3 width=2 by cpg_flat, ex_intro/
qed.
-lemma cpx_zeta: â\88\80h,G,L,V,T1,T,T2. â¦\83G, L.â\93\93Vâ¦\84 â\8a¢ T1 â\9e¡[h] T →
- â¬\86*[1] T2 â\89¡ T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ +â\93\93V.T1 â\9e¡[h] T2.
+lemma cpx_zeta: â\88\80h,G,L,V,T1,T,T2. â¦\83G, L.â\93\93Vâ¦\84 â\8a¢ T1 â¬\88[h] T →
+ â¬\86*[1] T2 â\89¡ T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ +â\93\93V.T1 â¬\88[h] T2.
#h #G #L #V #T1 #T #T2 *
/3 width=4 by cpg_zeta, ex_intro/
qed.
-lemma cpx_eps: â\88\80h,G,L,V,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[h] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV.T1 â\9e¡[h] T2.
+lemma cpx_eps: â\88\80h,G,L,V,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV.T1 â¬\88[h] T2.
#h #G #L #V #T1 #T2 *
/3 width=2 by cpg_eps, ex_intro/
qed.
(* Basic_2A1: was: cpx_ct *)
-lemma cpx_ee: â\88\80h,G,L,V1,V2,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.T â\9e¡[h] V2.
+lemma cpx_ee: â\88\80h,G,L,V1,V2,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.T â¬\88[h] V2.
#h #G #L #V1 #V2 #T *
/3 width=2 by cpg_ee, ex_intro/
qed.
lemma cpx_beta: ∀h,p,G,L,V1,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[h] W2 â\86\92 â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[h] T2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\9b{p}W1.T1 â\9e¡[h] ⓓ{p}ⓝW2.V2.T2.
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[h] W2 â\86\92 â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[h] T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\9b{p}W1.T1 â¬\88[h] ⓓ{p}ⓝW2.V2.T2.
#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 * #cV #HV12 * #cW #HW12 *
/3 width=2 by cpg_beta, ex_intro/
qed.
lemma cpx_theta: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V â\86\92 â¬\86*[1] V â\89¡ V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[h] W2 →
- â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[h] T2 →
- â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{p}W1.T1 â\9e¡[h] ⓓ{p}W2.ⓐV2.T2.
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V â\86\92 â¬\86*[1] V â\89¡ V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[h] W2 →
+ â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[h] T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.â\93\93{p}W1.T1 â¬\88[h] ⓓ{p}W2.ⓐV2.T2.
#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #cV #HV1 #HV2 * #cW #HW12 *
/3 width=4 by cpg_theta, ex_intro/
qed.
lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L).
/2 width=2 by ex_intro/ qed.
-lemma cpx_pair_sn: â\88\80h,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â\9e¡[h] ②{I}V2.T.
+lemma cpx_pair_sn: â\88\80h,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 →
+ â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â¬\88[h] ②{I}V2.T.
#h #I #G #L #V1 #V2 *
/3 width=2 by cpg_pair_sn, ex_intro/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma cpx_inv_atom1: â\88\80h,J,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{J} â\9e¡[h] T2 →
+lemma cpx_inv_atom1: â\88\80h,J,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{J} â¬\88[h] T2 →
∨∨ T2 = ⓪{J}
| ∃∃s. T2 = ⋆(next h s) & J = Sort s
- | â\88\83â\88\83I,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83I,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓑ{I}V1 & J = LRef 0
- | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[h] T & ⬆*[1] T ≡ T2 &
+ | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[h] T & ⬆*[1] T ≡ T2 &
L = K.ⓑ{I}V & J = LRef (⫯i).
#h #J #G #L #T2 * #c #H elim (cpg_inv_atom1 … H) -H *
/4 width=9 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex4_5_intro, ex4_4_intro, ex2_intro, ex_intro/
qed-.
-lemma cpx_inv_sort1: â\88\80h,G,L,T2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â\9e¡[h] T2 →
+lemma cpx_inv_sort1: â\88\80h,G,L,T2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â¬\88[h] T2 →
T2 = ⋆s ∨ T2 = ⋆(next h s).
#h #G #L #T2 #s * #c #H elim (cpg_inv_sort1 … H) -H *
/2 width=1 by or_introl, or_intror/
qed-.
-lemma cpx_inv_zero1: â\88\80h,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #0 â\9e¡[h] T2 →
+lemma cpx_inv_zero1: â\88\80h,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #0 â¬\88[h] T2 →
T2 = #0 ∨
- â\88\83â\88\83I,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & ⬆*[1] V2 ≡ T2 &
+ â\88\83â\88\83I,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓑ{I}V1.
#h #G #L #T2 * #c #H elim (cpg_inv_zero1 … H) -H *
/4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/
qed-.
-lemma cpx_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i â\9e¡[h] T2 →
+lemma cpx_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i â¬\88[h] T2 →
T2 = #(⫯i) ∨
- â\88\83â\88\83I,K,V,T. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
+ â\88\83â\88\83I,K,V,T. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
#h #G #L #T2 #i * #c #H elim (cpg_inv_lref1 … H) -H *
/4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/
qed-.
-lemma cpx_inv_gref1: â\88\80h,G,L,T2,l. â¦\83G, Lâ¦\84 â\8a¢ §l â\9e¡[h] T2 → T2 = §l.
+lemma cpx_inv_gref1: â\88\80h,G,L,T2,l. â¦\83G, Lâ¦\84 â\8a¢ §l â¬\88[h] T2 → T2 = §l.
#h #G #L #T2 #l * #c #H elim (cpg_inv_gref1 … H) -H //
qed-.
-lemma cpx_inv_bind1: â\88\80h,p,I,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[h] U2 → (
- â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â\9e¡[h] T2 &
+lemma cpx_inv_bind1: â\88\80h,p,I,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[h] U2 → (
+ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â¬\88[h] T2 &
U2 = ⓑ{p,I}V2.T2
) ∨
- â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[h] T & ⬆*[1] U2 ≡ T &
+ â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[h] T & ⬆*[1] U2 ≡ T &
p = true & I = Abbr.
#h #p #I #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_bind1 … H) -H *
/4 width=5 by ex4_intro, ex3_2_intro, ex_intro, or_introl, or_intror/
qed-.
-lemma cpx_inv_abbr1: â\88\80h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 â\9e¡[h] U2 → (
- â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[h] T2 &
+lemma cpx_inv_abbr1: â\88\80h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 â¬\88[h] U2 → (
+ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[h] T2 &
U2 = ⓓ{p}V2.T2
) ∨
- â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[h] T & ⬆*[1] U2 ≡ T & p = true.
+ â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[h] T & ⬆*[1] U2 ≡ T & p = true.
#h #p #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_abbr1 … H) -H *
/4 width=5 by ex3_2_intro, ex3_intro, ex_intro, or_introl, or_intror/
qed-.
-lemma cpx_inv_abst1: â\88\80h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 â\9e¡[h] U2 →
- â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, L.â\93\9bV1â¦\84 â\8a¢ T1 â\9e¡[h] T2 &
+lemma cpx_inv_abst1: â\88\80h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 â¬\88[h] U2 →
+ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, L.â\93\9bV1â¦\84 â\8a¢ T1 â¬\88[h] T2 &
U2 = ⓛ{p}V2.T2.
#h #p #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_abst1 … H) -H
/3 width=5 by ex3_2_intro, ex_intro/
qed-.
-lemma cpx_inv_flat1: â\88\80h,I,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 â\9e¡[h] U2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[h] T2 &
+lemma cpx_inv_flat1: â\88\80h,I,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 â¬\88[h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[h] T2 &
U2 = ⓕ{I}V2.T2
- | (â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[h] U2 ∧ I = Cast)
- | (â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] U2 ∧ I = Cast)
- | â\88\83â\88\83p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[h] W2 &
- â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[h] T2 &
+ | (â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[h] U2 ∧ I = Cast)
+ | (â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] U2 ∧ I = Cast)
+ | â\88\83â\88\83p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[h] W2 &
+ â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[h] T2 &
U1 = ⓛ{p}W1.T1 &
U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
- | â\88\83â\88\83p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V & ⬆*[1] V ≡ V2 &
- â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[h] T2 &
+ | â\88\83â\88\83p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V & ⬆*[1] V ≡ V2 &
+ â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[h] T2 &
U1 = ⓓ{p}W1.T1 &
U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
#h #I #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_flat1 … H) -H *
/4 width=14 by or5_intro0, or5_intro1, or5_intro2, or5_intro3, or5_intro4, ex7_7_intro, ex6_6_intro, ex3_2_intro, ex_intro, conj/
qed-.
-lemma cpx_inv_appl1: â\88\80h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90 V1.U1 â\9e¡[h] U2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[h] T2 &
+lemma cpx_inv_appl1: â\88\80h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90 V1.U1 â¬\88[h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[h] T2 &
U2 = ⓐV2.T2
- | â\88\83â\88\83p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[h] W2 &
- â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[h] T2 &
+ | â\88\83â\88\83p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[h] W2 &
+ â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[h] T2 &
U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2
- | â\88\83â\88\83p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V & ⬆*[1] V ≡ V2 &
- â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[h] T2 &
+ | â\88\83â\88\83p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V & ⬆*[1] V ≡ V2 &
+ â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[h] T2 &
U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2.
#h #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_appl1 … H) -H *
/4 width=13 by or3_intro0, or3_intro1, or3_intro2, ex6_7_intro, ex5_6_intro, ex3_2_intro, ex_intro/
qed-.
-lemma cpx_inv_cast1: â\88\80h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.U1 â\9e¡[h] U2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[h] T2 &
+lemma cpx_inv_cast1: â\88\80h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.U1 â¬\88[h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[h] T2 &
U2 = ⓝV2.T2
- | â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[h] U2
- | â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] U2.
+ | â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[h] U2
+ | â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] U2.
#h #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_cast1 … H) -H *
/4 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex_intro/
qed-.
(* Basic forward lemmas *****************************************************)
-lemma cpx_fwd_bind1_minus: â\88\80h,I,G,L,V1,T1,T. â¦\83G, Lâ¦\84 â\8a¢ -â\93\91{I}V1.T1 â\9e¡[h] T → ∀p.
- â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[h] ⓑ{p,I}V2.T2 &
+lemma cpx_fwd_bind1_minus: â\88\80h,I,G,L,V1,T1,T. â¦\83G, Lâ¦\84 â\8a¢ -â\93\91{I}V1.T1 â¬\88[h] T → ∀p.
+ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[h] ⓑ{p,I}V2.T2 &
T = -ⓑ{I}V2.T2.
#h #I #G #L #V1 #T1 #T * #c #H #p elim (cpg_fwd_bind1_minus … H p) -H
/3 width=4 by ex2_2_intro, ex_intro/
include "basic_2/rt_transition/cpg_drops.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS *****************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
(* Advanced properties ******************************************************)
(* Basic_2A1: was: cpx_delta *)
lemma cpx_delta_drops: ∀h,I,G,L,K,V,V2,W2,i.
- â¬\87*[i] L â\89¡ K.â\93\91{I}V â\86\92 â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[h] V2 →
- â¬\86*[⫯i] V2 â\89¡ W2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ #i â\9e¡[h] W2.
+ â¬\87*[i] L â\89¡ K.â\93\91{I}V â\86\92 â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[h] V2 →
+ â¬\86*[⫯i] V2 â\89¡ W2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ #i â¬\88[h] W2.
#h * #G #L #K #V #V2 #W2 #i #HLK *
/3 width=7 by cpg_ell_drops, cpg_delta_drops, ex_intro/
qed.
(* Advanced inversion lemmas ************************************************)
(* Basic_2A1: was: cpx_inv_atom1 *)
-lemma cpx_inv_atom1_drops: â\88\80h,I,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{I} â\9e¡[h] T2 →
+lemma cpx_inv_atom1_drops: â\88\80h,I,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{I} â¬\88[h] T2 →
∨∨ T2 = ⓪{I}
| ∃∃s. T2 = ⋆(next h s) & I = Sort s
- | â\88\83â\88\83J,K,V,V2,i. â¬\87*[i] L â\89¡ K.â\93\91{J}V & â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[h] V2 &
+ | â\88\83â\88\83J,K,V,V2,i. â¬\87*[i] L â\89¡ K.â\93\91{J}V & â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[h] V2 &
⬆*[⫯i] V2 ≡ T2 & I = LRef i.
#h #I #G #L #T2 * #c #H elim (cpg_inv_atom1_drops … H) -H *
/4 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex2_intro, ex_intro/
qed-.
(* Basic_2A1: was: cpx_inv_lref1 *)
-lemma cpx_inv_lref1_drops: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #i â\9e¡[h] T2 →
+lemma cpx_inv_lref1_drops: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #i â¬\88[h] T2 →
T2 = #i ∨
- â\88\83â\88\83J,K,V,V2. â¬\87*[i] L â\89¡ K. â\93\91{J}V & â¦\83G, Kâ¦\84 â\8a¢ V â\9e¡[h] V2 &
+ â\88\83â\88\83J,K,V,V2. â¬\87*[i] L â\89¡ K. â\93\91{J}V & â¦\83G, Kâ¦\84 â\8a¢ V â¬\88[h] V2 &
⬆*[⫯i] V2 ≡ T2.
#h #G #L #T1 #i * #c #H elim (cpg_inv_lref1_drops … H) -H *
/4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/
(* *)
(**************************************************************************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+
(* Properties on supclosure *************************************************)
lemma fqu_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡[h, o] U2 →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h, o] U2 →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
[ #I #G #L #V2 #U2 #HVU2
qed-.
lemma fquq_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡[h, o] U2 →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h, o] U2 →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
[ #HT12 elim (fqu_cpx_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/
| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
qed-.
lemma fqup_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡[h, o] U2 →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h, o] U2 →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h, o] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
[ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpx_trans … H12 … HTU2) -T2
/3 width=3 by fqu_fqup, ex2_intro/
qed-.
lemma fqus_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡[h, o] U2 →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h, o] U2 →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fqus_inv_gen … H) -H
[ #HT12 elim (fqup_cpx_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/
| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
qed-.
lemma fqu_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡[h, o] U2 → (T2 = U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h, o] U2 → (T2 = U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
#U2 #HVU2 @(ex3_intro … U2)
qed-.
lemma fquq_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡[h, o] U2 → (T2 = U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h, o] U2 → (T2 = U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12
[ #H12 elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fquq, ex3_intro/
qed-.
lemma fqup_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡[h, o] U2 → (T2 = U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h, o] U2 → (T2 = U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fqup, ex3_intro/
qed-.
lemma fqus_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â\9e¡[h, o] U2 → (T2 = U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h, o] U2 → (T2 = U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12
[ #H12 elim (fqup_cpx_trans_neq … H12 … HTU2 H) -T2
/3 width=4 by fqup_fqus, ex3_intro/
include "basic_2/multiple/lleq_drop.ma".
include "basic_2/reduction/cpx_llpx_sn.ma".
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
(* Properties on lazy equivalence for local environments ********************)
-lemma lleq_cpx_trans: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â\9e¡[h, o] T2 →
- â\88\80L1. L1 â\89¡[T1, 0] L2 â\86\92 â¦\83G, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] T2.
+lemma lleq_cpx_trans: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â¬\88[h, o] T2 →
+ â\88\80L1. L1 â\89¡[T1, 0] L2 â\86\92 â¦\83G, L1â¦\84 â\8a¢ T1 â¬\88[h, o] T2.
#h #o #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_st/
[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2
[ #H elim (ylt_yle_false … H) //
]
qed-.
-lemma cpx_lleq_conf: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â\9e¡[h, o] T2 →
- â\88\80L1. L2 â\89¡[T1, 0] L1 â\86\92 â¦\83G, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] T2.
+lemma cpx_lleq_conf: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â¬\88[h, o] T2 →
+ â\88\80L1. L2 â\89¡[T1, 0] L1 â\86\92 â¦\83G, L1â¦\84 â\8a¢ T1 â¬\88[h, o] T2.
/3 width=3 by lleq_cpx_trans, lleq_sym/ qed-.
lemma cpx_lleq_conf_sn: ∀h,o,G. b_c_confluent1 … (cpx h o G) (lleq 0).
/3 width=6 by cpx_llpx_sn_conf, lift_mono, ex2_intro/ qed-.
-lemma cpx_lleq_conf_dx: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â\9e¡[h, o] T2 →
+lemma cpx_lleq_conf_dx: â\88\80h,o,G,L2,T1,T2. â¦\83G, L2â¦\84 â\8a¢ T1 â¬\88[h, o] T2 →
∀L1. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2.
/4 width=6 by cpx_lleq_conf_sn, lleq_sym/ qed-.
include "basic_2/multiple/llpx_sn_drop.ma".
include "basic_2/reduction/cpx.ma".
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
(* Properties on lazy sn pointwise extensions *******************************)
include "basic_2/substitution/drop_lreq.ma".
include "basic_2/reduction/cpx.ma".
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
(* Properties on equivalence for local environments *************************)
include "basic_2/rt_transition/cpg_lsubr.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS *****************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
lemma lsubr_cpx_trans: ∀h,G. lsub_trans … (cpx h G) lsubr.
#h #G #L1 #T1 #T2 * /3 width=4 by lsubr_cpg_trans, ex_intro/
include "basic_2/rt_transition/cpg_simple.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS *****************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
-lemma cpx_inv_appl1_simple: â\88\80h,G,L,V1,T1,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â\9e¡[h] U → 𝐒⦃T1⦄ →
- â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[h] T2 &
+lemma cpx_inv_appl1_simple: â\88\80h,G,L,V1,T1,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â¬\88[h] U → 𝐒⦃T1⦄ →
+ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[h] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 &
U = ⓐV2.T2.
#h #G #L #V1 #T1 #U * #c #H #HT1 elim (cpg_inv_appl1_simple … H) -H
/3 width=5 by ex3_2_intro, ex_intro/
--- /dev/null
+cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma
+cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma
]
*)
[ { "uncounted context-sensitive rt-transition" * } {
- [ "cpx ( â¦\83?,?â¦\84 â\8a¢ ? â\9e¡[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
+ [ "cpx ( â¦\83?,?â¦\84 â\8a¢ ? â¬\88[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
}
]
[ { "counted context-sensitive rt-transition" * } {
- [ "cpg ( â¦\83?,?â¦\84 â\8a¢ ? â\9e¡[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
+ [ "cpg ( â¦\83?,?â¦\84 â\8a¢ ? â¬\88[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
}
]
}
class "orange"
[ { "relocation" * } {
[ { "generic slicing for local environments" * } {
- [ "drops_vector ( ⬇*[?,?] ? ≡ ? )" * ]
- [ "drops ( ⬇*[?,?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ceq" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
+ [ "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ]
+ [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ceq" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
}
]
[ { "generic relocation for terms" * } {
#!/bin/sh
-for MA in `find -name "*.ma"`; do
+#for MA in `find -name "*.ma"`; do
+for MA in `find -name "cpg*.ma" -or -name "cpx*.ma"`; do
echo ${MA}; sed "s!$1!$2!g" ${MA} > ${MA}.new
if diff ${MA} ${MA}.new > /dev/null;
then rm -f ${MA}.new;
["-"; "÷"; "⊢"; "⊩"; "⊟"; ];
["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≗"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ];
["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
- ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ;
+ ["â\87\92"; "â¤\87"; "â\9e¾"; "â\87¨"; "â\9e¡"; "â¬\88"; "â\9e¤"; "â\9e¸"; "â\87\89"; "⥰"; ] ;
["^"; "↑"; ] ;
["⇑"; "⇧"; "⬆"; ] ;
["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;
projects / helm.git / commitdiff