notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
-let rec moves (S : DeqSet) w e on w : pre S ≝
+let rec moves (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) w e on w : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
match w with
[ nil ⇒ e
- | cons x w' ⇒ w' ↦* (move S x (\fst e))].
+ | cons x w' ⇒ w' ↦* (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e))].
-lemma moves_empty: ∀S:DeqSet.∀e:pre S.
- moves ? [ ] e = e.
+lemma moves_empty: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e.
// qed.
-lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S.
- moves ? (a::w) e = moves ? w (move S a (\fst e)).
+lemma moves_cons: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e)).
// qed.
lemma moves_left : ∀S,a,w,e.
- moves S (w@[a]) e = move S a (\fst (moves S w e)).
-#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
+ \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S (w\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])) e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e)).
+#S #a #w elim w // #x #tl #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 //
qed.
-lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S.
- iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+lemma not_epsilon_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e) ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
#S #a #w * #i #b cases b normalize
- [% /2/ * // #H destruct |% normalize /2/]
+ [% /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * // #H destruct |% normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]
qed.
-lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
- |\fst (moves ? w e)| = |\fst e|.
+lemma same_kernel_moves: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e)| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|.
#S #w elim w //
qed.
-theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
- (\snd (moves ? w e) = true) ↔ \sem{e} w.
+theorem decidable_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e} w.
#S #w elim w
- [* #i #b >moves_empty cases b % /2/
- |#a #w1 #Hind #e >moves_cons
- @iff_trans [||@iff_sym @not_epsilon_sem]
- @iff_trans [||@move_ok] @Hind
+ [* #i #b >\ 5a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"\ 6moves_empty\ 5/a\ 6 cases b % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"\ 6true_to_epsilon\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/\ 5span class="error" title="error location"\ 6\ 5/span\ 6 #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#a #w1 #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6
+ @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter9/not_epsilon_sem.def(9)"\ 6not_epsilon_sem\ 5/a\ 6]
+ @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter9/move_ok.def(14)"\ 6move_ok\ 5/a\ 6] @Hind
]
qed.
\ 5b\ 6Example\ 5/b\ 6.
Below is the DFA associated with the regular expression (ac+bc)*.
-\ 5img src="acUbc.gif" alt="some_text"/\ 6
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"\ 6
The graphical description of the automaton is the traditional one, with nodes for
states and labelled arcs for transitions. Unreachable states are not shown.
\ 5b\ 6Example\ 5/b\ 6.
Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
-\ 5img src="automaton.pdf" alt="some_text"/\ 6
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"\ 6
Remarkably, this DFA is minimal, testifying the small number of states produced by our
-technique (the pair ofstates $6-8$ and $7-9$ differ for the fact that $6$ and $7$
-are final, while $8$ and $9$ are not).
-*)
+technique (the pair of states 6-8 and 7-9 differ for the fact that 6 and 7
+are final, while 8 and 9 are not).
-(************************ pit state ***************************)
-definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
-let rec occur (S: DeqSet) (i: re S) on i ≝
+\ 5h2\ 6Move to pit\ 5/h2\ 6.
+
+We conclude this chapter with a few properties of the move opertions in relation
+with the pit state. *)
+
+definition pit_pre ≝ λS.λi.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|), \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉.
+
+(* The following function compute the list of characters occurring in a given
+item i. *)
+
+let rec occur (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (i: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on i ≝
match i with
- [ z ⇒ [ ]
- | e ⇒ [ ]
- | s y ⇒ [y]
- | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
- | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
+ [ z ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
+ | e ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
+ | s y ⇒ y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
+ | o e1 e2 ⇒ \ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (occur S e1) (occur S e2)
+ | c e1 e2 ⇒ \ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (occur S e1) (occur S e2)
| k e ⇒ occur S e].
-lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
- move S a i = pit_pre S i.
+(* If a symbol a does not occur in i, then move(i,a) gets to the
+pit state. *)
+
+lemma not_occur_to_pit: ∀S,a.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"\ 6occur\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|)) \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
+ \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.
#S #a #i elim i //
- [#x normalize cases (a==x) normalize // #H @False_ind /2/
- |#i1 #i2 #Hind1 #Hind2 #H >move_cat
- >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
- >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
- |#i1 #i2 #Hind1 #Hind2 #H >move_plus
- >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
- >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
- |#i #Hind #H >move_star >Hind //
+ [#x normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x) normalize // #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#i1 #i2 #Hind1 #Hind2 #H >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6
+ >Hind1 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"\ 6sublist_unique_append_l1\ 5/a\ 6 //]
+ >Hind2 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"\ 6sublist_unique_append_l2\ 5/a\ 6 //] //
+ |#i1 #i2 #Hind1 #Hind2 #H >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6
+ >Hind1 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"\ 6sublist_unique_append_l1\ 5/a\ 6 //]
+ >Hind2 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"\ 6sublist_unique_append_l2\ 5/a\ 6 //] //
+ |#i #Hind #H >\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"\ 6move_star\ 5/a\ 6 >Hind //
]
qed.
-lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+(* We cannot escape form the pit state. *)
+
+lemma move_pit: ∀S,a,i. \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.
#S #a #i elim i //
- [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
- |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
- |#i #Hind >move_star >Hind //
+ [#i1 #i2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6 >Hind1 >Hind2 //
+ |#i1 #i2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 >Hind1 >Hind2 //
+ |#i #Hind >\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"\ 6move_star\ 5/a\ 6 >Hind //
]
qed.
-lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
+lemma moves_pit: ∀S,w,i. \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.
#S #w #i elim w //
qed.
-lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
- moves S w e = pit_pre S (\fst e).
+(* If any character in w does not occur in i, then moves(i,w) gets
+to the pit state. *)
+
+lemma to_pit: ∀S,w,e. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"\ 6occur\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|)) →
+ \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
#S #w elim w
- [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
- |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
- [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
- @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
+ [#e * #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @H normalize #a #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#a #tl #Hind #e #H cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"\ 6occur\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|))))
+ [#Htrue >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 whd in ⊢ (???%); <(\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"\ 6same_kernel\ 5/a\ 6 … a)
+ @Hind >\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"\ 6same_kernel\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 #b #memb cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … memb)
[#H2 >(\P H2) // |#H2 @H1 //]
- |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
+ |#Hfalse >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/not_occur_to_pit.def(8)"\ 6not_occur_to_pit\ 5/a\ 6 // >Hfalse /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
]
-qed.
\ No newline at end of file
+qed.
projects / helm.git / blobdiff