- [#w normalize % [/2/ | * //]
- |/2/
- |#x normalize #w % [ /2/ | * [@False_ind | //]]
- |#x normalize #w % [ /2/ | * // ]
- |#i1 #i2 #IH1 #IH2 >eclose_dot
- @eqP_trans [|@odot_dot_aux //] >sem_cat
- @eqP_trans
- [|@eqP_union_r
- [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
- @eqP_trans [|@union_assoc]
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l //
- |#i1 #i2 #IH1 #IH2 >eclose_plus
- @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
- @eqP_trans [|@(eqP_union_l … IH2)]
- @eqP_trans [|@eqP_sym @union_assoc]
- @eqP_trans [||@union_assoc] @eqP_union_r
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_trans [||@eqP_union_l [|@union_comm]]
- @eqP_trans [||@union_assoc] /2/
- |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
- @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
- @eqP_sym @star_fix_eps
+ [#w normalize % [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * //]
+ |/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#x normalize #w % [ /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * [@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 | //]]
+ |#x normalize #w % [ /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * // ]
+ |#i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_dot.def(5)"\ 6eclose_dot\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_pcl_aux.def(11)"\ 6sem_pcl_aux\ 5/a\ 6 //] >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6
+ [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6
+ [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@(\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 … IH1)] @\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 //
+ |#i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_plus.def(5)"\ 6eclose_plus\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_oplus.def(9)"\ 6sem_oplus\ 5/a\ 6] >\ 5a href="cic:/matita/tutorial/chapter7/sem_plus.def(8)"\ 6sem_plus\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/erase_plus.def(4)"\ 6erase_plus\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@(\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 … IH2)]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_comm.def(3)"\ 6union_comm\ 5/a\ 6]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#i #H >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/erase_bull.def(6)"\ 6erase_bull\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/minus_eps_pre_aux.def(11)"\ 6minus_eps_pre_aux\ 5/a\ 6 //]]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]]
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/erase_star.def(4)"\ 6erase_star\ 5/a\ 6
+ @\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/star_fix_eps.def(7)"\ 6star_fix_eps\ 5/a\ 6