#j #Hg elim (at_inv_xnx ā¦ Hg ā¦ H) -Hg -H /2 width=2 by ex_intro/
qed-.
-(* Advanced forward lemmas on at ********************************************)
+(* Properties on tl *********************************************************)
-let corec at_ext: āf1,f2. šā¦f1ā¦ ā šā¦f2ā¦ ā
- (āi,i1,i2. @ā¦i, f1ā¦ ā” i1 ā @ā¦i, f2ā¦ ā” i2 ā i1 = i2) ā f1 ā f2 ā ?.
+lemma istot_tl: āf. šā¦fā¦ ā šā¦ā«±fā¦.
+#f cases (pn_split f) *
+#g * -f /2 width=3 by istot_inv_next, istot_inv_push/
+qed.
+
+(* Properties on tls ********************************************************)
+
+lemma istot_tls: ān,f. šā¦fā¦ ā šā¦ā«±*[n]fā¦.
+#n elim n -n /3 width=1 by istot_tl/
+qed.
+
+(* Main forward lemmas on at ************************************************)
+
+corec theorem at_ext: āf1,f2. šā¦f1ā¦ ā šā¦f2ā¦ ā
+ (āi,i1,i2. @ā¦i, f1ā¦ ā” i1 ā @ā¦i, f2ā¦ ā” i2 ā i1 = i2) ā
+ f1 ā f2.
#f1 cases (pn_split f1) * #g1 #H1
#f2 cases (pn_split f2) * #g2 #H2
#Hf1 #Hf2 #Hi
]
qed-.
-(* Main properties on at ****************************************************)
+(* Advanced properties on at ************************************************)
lemma at_dec: āf,i1,i2. šā¦fā¦ ā Decidable (@ā¦i1, fā¦ ā” i2).
#f #i1 #i2 #Hf lapply (Hf i1) -Hf *
]
qed-.
-lemma is_at_dec_le: āf,i2,i. šā¦fā¦ ā (āi1. i1 + i ā¤ i2 ā @ā¦i1, fā¦ ā” i2 ā ā„) ā Decidable (āi1. @ā¦i1, fā¦ ā” i2).
+lemma is_at_dec_le: āf,i2,i. šā¦fā¦ ā (āi1. i1 + i ā¤ i2 ā @ā¦i1, fā¦ ā” i2 ā ā„) ā
+ Decidable (āi1. @ā¦i1, fā¦ ā” i2).
#f #i2 #i #Hf elim i -i
[ #Ht @or_intror * /3 width=3 by at_increasing/
| #i #IH #Ht elim (at_dec f (i2-i) i2) /3 width=2 by ex_intro, or_introl/