| NotL: ∀l1,l2,f.
derive 〈l1,f::l2〉 → derive 〈FNot f :: l1,l2〉.
-alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)".
let rec and_of_list l ≝
match l with
- [ Nil ⇒ FTrue
- | Cons F l' ⇒ FAnd F (and_of_list l')
+ [ nil ⇒ FTrue
+ | cons F l' ⇒ FAnd F (and_of_list l')
].
let rec or_of_list l ≝
match l with
- [ Nil ⇒ FFalse
- | Cons F l' ⇒ FOr F (or_of_list l')
+ [ nil ⇒ FFalse
+ | cons F l' ⇒ FOr F (or_of_list l')
].
definition formula_of_sequent ≝
qed.
alias num (instance 0) = "natural number".
-alias symbol "plus" = "natural plus".
let rec size F ≝
match F with
[ FTrue ⇒ 0
let rec sizel l ≝
match l with
- [ Nil ⇒ 0
- | Cons F l' ⇒ size F + sizel l'
+ [ nil ⇒ 0
+ | cons F l' ⇒ size F + sizel l'
].
definition size_of_sequent ≝
qed.
definition symmetricb ≝
- λA:Type.λeq:A → A → bool.
- ∀x,y. eq x y = eq y x.
+ λA:Type.λeq:A → A → bool. ∀x,y. eq x y = eq y x.
theorem symmetricb_eqb: symmetricb ? eqb.
intro;
|4,5:
simplify in H2;
destruct H2
- | simplify in H2;
+ | simplify in H1;
destruct H1
]
|4,5:
[ decompose;
rewrite > H2; clear H2;
rewrite > H4; clear H4;
- apply (exchangeL ? a1 a2 (FAtom a));
- apply (exchangeR ? a3 a4 (FAtom a));
- apply axiom
+ apply (ExchangeL ? a1 a2 (FAtom a));
+ apply (ExchangeR ? a3 a4 (FAtom a));
+ apply Axiom
| elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2);
[ decompose;
rewrite > H3;
- apply (exchangeL ? a a1 FFalse);
- apply falseL
+ apply (ExchangeL ? a a1 FFalse);
+ apply FalseL
| decompose;
rewrite > H3;
- apply (exchangeR ? a a1 FTrue);
- apply trueR
+ apply (ExchangeR ? a a1 FTrue);
+ apply TrueR
]
]
qed.
| apply NotR;
simplify in H1;
*)
-*)