author | wenzelm |

Thu Feb 28 14:22:14 2013 +0100 (2013-02-28) | |

changeset 51309 | 473303ef6e34 |

parent 51308 | 51e158e988a5 |

child 51310 | d2aeb3dffb8f |

eliminated legacy 'axioms';

1.1 --- a/src/Sequents/ILL.thy Thu Feb 28 14:10:54 2013 +0100 1.2 +++ b/src/Sequents/ILL.thy Thu Feb 28 14:22:14 2013 +0100 1.3 @@ -54,47 +54,47 @@ 1.4 aneg_def: "~A == A -o 0" 1.5 1.6 1.7 -axioms 1.8 +axiomatization where 1.9 1.10 -identity: "P |- P" 1.11 +identity: "P |- P" and 1.12 1.13 -zerol: "$G, 0, $H |- A" 1.14 +zerol: "$G, 0, $H |- A" and 1.15 1.16 (* RULES THAT DO NOT DIVIDE CONTEXT *) 1.17 1.18 -derelict: "$F, A, $G |- C ==> $F, !A, $G |- C" 1.19 +derelict: "$F, A, $G |- C ==> $F, !A, $G |- C" and 1.20 (* unfortunately, this one removes !A *) 1.21 1.22 -contract: "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" 1.23 +contract: "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" and 1.24 1.25 -weaken: "$F, $G |- C ==> $G, !A, $F |- C" 1.26 +weaken: "$F, $G |- C ==> $G, !A, $F |- C" and 1.27 (* weak form of weakening, in practice just to clean context *) 1.28 (* weaken and contract not needed (CHECK) *) 1.29 1.30 -promote2: "promaux{ || $H || B} ==> $H |- !B" 1.31 +promote2: "promaux{ || $H || B} ==> $H |- !B" and 1.32 promote1: "promaux{!A, $G || $H || B} 1.33 - ==> promaux {$G || $H, !A || B}" 1.34 -promote0: "$G |- A ==> promaux {$G || || A}" 1.35 + ==> promaux {$G || $H, !A || B}" and 1.36 +promote0: "$G |- A ==> promaux {$G || || A}" and 1.37 1.38 1.39 1.40 -tensl: "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" 1.41 +tensl: "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" and 1.42 1.43 -impr: "A, $F |- B ==> $F |- A -o B" 1.44 +impr: "A, $F |- B ==> $F |- A -o B" and 1.45 1.46 conjr: "[| $F |- A ; 1.47 $F |- B |] 1.48 - ==> $F |- (A && B)" 1.49 + ==> $F |- (A && B)" and 1.50 1.51 -conjll: "$G, A, $H |- C ==> $G, A && B, $H |- C" 1.52 +conjll: "$G, A, $H |- C ==> $G, A && B, $H |- C" and 1.53 1.54 -conjlr: "$G, B, $H |- C ==> $G, A && B, $H |- C" 1.55 +conjlr: "$G, B, $H |- C ==> $G, A && B, $H |- C" and 1.56 1.57 -disjrl: "$G |- A ==> $G |- A ++ B" 1.58 -disjrr: "$G |- B ==> $G |- A ++ B" 1.59 +disjrl: "$G |- A ==> $G |- A ++ B" and 1.60 +disjrr: "$G |- B ==> $G |- A ++ B" and 1.61 disjl: "[| $G, A, $H |- C ; 1.62 $G, B, $H |- C |] 1.63 - ==> $G, A ++ B, $H |- C" 1.64 + ==> $G, A ++ B, $H |- C" and 1.65 1.66 1.67 (* RULES THAT DIVIDE CONTEXT *) 1.68 @@ -102,26 +102,26 @@ 1.69 tensr: "[| $F, $J :=: $G; 1.70 $F |- A ; 1.71 $J |- B |] 1.72 - ==> $G |- A >< B" 1.73 + ==> $G |- A >< B" and 1.74 1.75 impl: "[| $G, $F :=: $J, $H ; 1.76 B, $F |- C ; 1.77 $G |- A |] 1.78 - ==> $J, A -o B, $H |- C" 1.79 + ==> $J, A -o B, $H |- C" and 1.80 1.81 1.82 cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ; 1.83 $H1, $H2, $H3, $H4 |- A ; 1.84 - $J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B" 1.85 + $J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B" and 1.86 1.87 1.88 (* CONTEXT RULES *) 1.89 1.90 -context1: "$G :=: $G" 1.91 -context2: "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" 1.92 -context3: "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" 1.93 -context4a: "$F :=: $H, $G ==> $F :=: $H, !A, $G" 1.94 -context4b: "$F, $H :=: $G ==> $F, !A, $H :=: $G" 1.95 +context1: "$G :=: $G" and 1.96 +context2: "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" and 1.97 +context3: "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" and 1.98 +context4a: "$F :=: $H, $G ==> $F :=: $H, !A, $G" and 1.99 +context4b: "$F, $H :=: $G ==> $F, !A, $H :=: $G" and 1.100 context5: "$F, $G :=: $H ==> $G, $F :=: $H" 1.101 1.102

2.1 --- a/src/Sequents/LK/Nat.thy Thu Feb 28 14:10:54 2013 +0100 2.2 +++ b/src/Sequents/LK/Nat.thy Thu Feb 28 14:22:14 2013 +0100 2.3 @@ -11,20 +11,22 @@ 2.4 2.5 typedecl nat 2.6 arities nat :: "term" 2.7 -consts Zero :: nat ("0") 2.8 - Suc :: "nat=>nat" 2.9 - rec :: "[nat, 'a, [nat,'a]=>'a] => 'a" 2.10 - add :: "[nat, nat] => nat" (infixl "+" 60) 2.11 2.12 -axioms 2.13 +axiomatization 2.14 + Zero :: nat ("0") and 2.15 + Suc :: "nat=>nat" and 2.16 + rec :: "[nat, 'a, [nat,'a]=>'a] => 'a" 2.17 +where 2.18 induct: "[| $H |- $E, P(0), $F; 2.19 - !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" 2.20 + !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" and 2.21 2.22 - Suc_inject: "|- Suc(m)=Suc(n) --> m=n" 2.23 - Suc_neq_0: "|- Suc(m) ~= 0" 2.24 - rec_0: "|- rec(0,a,f) = a" 2.25 + Suc_inject: "|- Suc(m)=Suc(n) --> m=n" and 2.26 + Suc_neq_0: "|- Suc(m) ~= 0" and 2.27 + rec_0: "|- rec(0,a,f) = a" and 2.28 rec_Suc: "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))" 2.29 - add_def: "m+n == rec(m, n, %x y. Suc(y))" 2.30 + 2.31 +definition add :: "[nat, nat] => nat" (infixl "+" 60) 2.32 + where "m + n == rec(m, n, %x y. Suc(y))" 2.33 2.34 2.35 declare Suc_neq_0 [simp]

3.1 --- a/src/Sequents/LK0.thy Thu Feb 28 14:10:54 2013 +0100 3.2 +++ b/src/Sequents/LK0.thy Thu Feb 28 14:22:14 2013 +0100 3.3 @@ -59,67 +59,69 @@ 3.4 Ex (binder "\<exists>" 10) and 3.5 not_equal (infixl "\<noteq>" 50) 3.6 3.7 -axioms 3.8 +axiomatization where 3.9 3.10 (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *) 3.11 3.12 - contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" 3.13 - contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" 3.14 + contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" and 3.15 + contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" and 3.16 3.17 - thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" 3.18 - thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" 3.19 + thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" and 3.20 + thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" and 3.21 3.22 - exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" 3.23 - exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" 3.24 + exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" and 3.25 + exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" and 3.26 3.27 - cut: "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" 3.28 + cut: "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" and 3.29 3.30 (*Propositional rules*) 3.31 3.32 - basic: "$H, P, $G |- $E, P, $F" 3.33 + basic: "$H, P, $G |- $E, P, $F" and 3.34 3.35 - conjR: "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" 3.36 - conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" 3.37 + conjR: "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" and 3.38 + conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" and 3.39 3.40 - disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" 3.41 - disjL: "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" 3.42 + disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" and 3.43 + disjL: "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" and 3.44 3.45 - impR: "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" 3.46 - impL: "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" 3.47 + impR: "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" and 3.48 + impL: "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" and 3.49 3.50 - notR: "$H, P |- $E, $F ==> $H |- $E, ~P, $F" 3.51 - notL: "$H, $G |- $E, P ==> $H, ~P, $G |- $E" 3.52 + notR: "$H, P |- $E, $F ==> $H |- $E, ~P, $F" and 3.53 + notL: "$H, $G |- $E, P ==> $H, ~P, $G |- $E" and 3.54 3.55 - FalseL: "$H, False, $G |- $E" 3.56 + FalseL: "$H, False, $G |- $E" and 3.57 3.58 - True_def: "True == False-->False" 3.59 + True_def: "True == False-->False" and 3.60 iff_def: "P<->Q == (P-->Q) & (Q-->P)" 3.61 3.62 +axiomatization where 3.63 (*Quantifiers*) 3.64 3.65 - allR: "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" 3.66 - allL: "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" 3.67 + allR: "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" and 3.68 + allL: "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" and 3.69 3.70 - exR: "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" 3.71 - exL: "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" 3.72 + exR: "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" and 3.73 + exL: "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" and 3.74 3.75 (*Equality*) 3.76 - 3.77 - refl: "$H |- $E, a=a, $F" 3.78 - subst: "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)" 3.79 + refl: "$H |- $E, a=a, $F" and 3.80 + subst: "\<And>G H E. $H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)" 3.81 3.82 (* Reflection *) 3.83 3.84 - eq_reflection: "|- x=y ==> (x==y)" 3.85 +axiomatization where 3.86 + eq_reflection: "|- x=y ==> (x==y)" and 3.87 iff_reflection: "|- P<->Q ==> (P==Q)" 3.88 3.89 (*Descriptions*) 3.90 3.91 +axiomatization where 3.92 The: "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> 3.93 $H |- $E, P(THE x. P(x)), $F" 3.94 3.95 -definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) where 3.96 - "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)" 3.97 +definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) 3.98 + where "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)" 3.99 3.100 3.101 (** Structural Rules on formulas **)

4.1 --- a/src/Sequents/S4.thy Thu Feb 28 14:10:54 2013 +0100 4.2 +++ b/src/Sequents/S4.thy Thu Feb 28 14:22:14 2013 +0100 4.3 @@ -7,26 +7,26 @@ 4.4 imports Modal0 4.5 begin 4.6 4.7 -axioms 4.8 +axiomatization where 4.9 (* Definition of the star operation using a set of Horn clauses *) 4.10 (* For system S4: gamma * == {[]P | []P : gamma} *) 4.11 (* delta * == {<>P | <>P : delta} *) 4.12 4.13 - lstar0: "|L>" 4.14 - lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" 4.15 - lstar2: "$G |L> $H ==> P, $G |L> $H" 4.16 - rstar0: "|R>" 4.17 - rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H" 4.18 - rstar2: "$G |R> $H ==> P, $G |R> $H" 4.19 + lstar0: "|L>" and 4.20 + lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" and 4.21 + lstar2: "$G |L> $H ==> P, $G |L> $H" and 4.22 + rstar0: "|R>" and 4.23 + rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H" and 4.24 + rstar2: "$G |R> $H ==> P, $G |R> $H" and 4.25 4.26 (* Rules for [] and <> *) 4.27 4.28 boxR: 4.29 "[| $E |L> $E'; $F |R> $F'; $G |R> $G'; 4.30 - $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G" 4.31 - boxL: "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G" 4.32 + $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G" and 4.33 + boxL: "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G" and 4.34 4.35 - diaR: "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" 4.36 + diaR: "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" and 4.37 diaL: 4.38 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; 4.39 $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G"

5.1 --- a/src/Sequents/S43.thy Thu Feb 28 14:10:54 2013 +0100 5.2 +++ b/src/Sequents/S43.thy Thu Feb 28 14:22:14 2013 +0100 5.3 @@ -32,17 +32,17 @@ 5.4 in [(@{const_syntax S43pi}, s43pi_tr')] end 5.5 *} 5.6 5.7 -axioms 5.8 +axiomatization where 5.9 (* Definition of the star operation using a set of Horn clauses *) 5.10 (* For system S43: gamma * == {[]P | []P : gamma} *) 5.11 (* delta * == {<>P | <>P : delta} *) 5.12 5.13 - lstar0: "|L>" 5.14 - lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" 5.15 - lstar2: "$G |L> $H ==> P, $G |L> $H" 5.16 - rstar0: "|R>" 5.17 - rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H" 5.18 - rstar2: "$G |R> $H ==> P, $G |R> $H" 5.19 + lstar0: "|L>" and 5.20 + lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" and 5.21 + lstar2: "$G |L> $H ==> P, $G |L> $H" and 5.22 + rstar0: "|R>" and 5.23 + rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H" and 5.24 + rstar2: "$G |R> $H ==> P, $G |R> $H" and 5.25 5.26 (* Set of Horn clauses to generate the antecedents for the S43 pi rule *) 5.27 (* ie *) 5.28 @@ -54,22 +54,22 @@ 5.29 (* and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj *) 5.30 (* and 1<=i<=k and k<j<=k+m *) 5.31 5.32 - S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia" 5.33 + S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia" and 5.34 S43pi1: 5.35 "[| (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==> 5.36 - S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" 5.37 + S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" and 5.38 S43pi2: 5.39 "[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==> 5.40 - S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" 5.41 + S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" and 5.42 5.43 (* Rules for [] and <> for S43 *) 5.44 5.45 - boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" 5.46 - diaR: "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" 5.47 + boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and 5.48 + diaR: "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" and 5.49 pi1: 5.50 "[| $L1,<>P,$L2 |L> $Lbox; $L1,<>P,$L2 |R> $Ldia; $R |L> $Rbox; $R |R> $Rdia; 5.51 S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 5.52 - $L1, <>P, $L2 |- $R" 5.53 + $L1, <>P, $L2 |- $R" and 5.54 pi2: 5.55 "[| $L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia; 5.56 S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>

6.1 --- a/src/Sequents/T.thy Thu Feb 28 14:10:54 2013 +0100 6.2 +++ b/src/Sequents/T.thy Thu Feb 28 14:22:14 2013 +0100 6.3 @@ -7,25 +7,25 @@ 6.4 imports Modal0 6.5 begin 6.6 6.7 -axioms 6.8 +axiomatization where 6.9 (* Definition of the star operation using a set of Horn clauses *) 6.10 (* For system T: gamma * == {P | []P : gamma} *) 6.11 (* delta * == {P | <>P : delta} *) 6.12 6.13 - lstar0: "|L>" 6.14 - lstar1: "$G |L> $H ==> []P, $G |L> P, $H" 6.15 - lstar2: "$G |L> $H ==> P, $G |L> $H" 6.16 - rstar0: "|R>" 6.17 - rstar1: "$G |R> $H ==> <>P, $G |R> P, $H" 6.18 - rstar2: "$G |R> $H ==> P, $G |R> $H" 6.19 + lstar0: "|L>" and 6.20 + lstar1: "$G |L> $H ==> []P, $G |L> P, $H" and 6.21 + lstar2: "$G |L> $H ==> P, $G |L> $H" and 6.22 + rstar0: "|R>" and 6.23 + rstar1: "$G |R> $H ==> <>P, $G |R> P, $H" and 6.24 + rstar2: "$G |R> $H ==> P, $G |R> $H" and 6.25 6.26 (* Rules for [] and <> *) 6.27 6.28 boxR: 6.29 "[| $E |L> $E'; $F |R> $F'; $G |R> $G'; 6.30 - $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G" 6.31 - boxL: "$E, P, $F |- $G ==> $E, []P, $F |- $G" 6.32 - diaR: "$E |- $F, P, $G ==> $E |- $F, <>P, $G" 6.33 + $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G" and 6.34 + boxL: "$E, P, $F |- $G ==> $E, []P, $F |- $G" and 6.35 + diaR: "$E |- $F, P, $G ==> $E |- $F, <>P, $G" and 6.36 diaL: 6.37 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; 6.38 $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G"

7.1 --- a/src/Sequents/Washing.thy Thu Feb 28 14:10:54 2013 +0100 7.2 +++ b/src/Sequents/Washing.thy Thu Feb 28 14:22:14 2013 +0100 7.3 @@ -6,26 +6,25 @@ 7.4 imports ILL 7.5 begin 7.6 7.7 -consts 7.8 - dollar :: o 7.9 - quarter :: o 7.10 - loaded :: o 7.11 - dirty :: o 7.12 - wet :: o 7.13 +axiomatization 7.14 + dollar :: o and 7.15 + quarter :: o and 7.16 + loaded :: o and 7.17 + dirty :: o and 7.18 + wet :: o and 7.19 clean :: o 7.20 - 7.21 -axioms 7.22 +where 7.23 change: 7.24 - "dollar |- (quarter >< quarter >< quarter >< quarter)" 7.25 + "dollar |- (quarter >< quarter >< quarter >< quarter)" and 7.26 7.27 load1: 7.28 - "quarter , quarter , quarter , quarter , quarter |- loaded" 7.29 + "quarter , quarter , quarter , quarter , quarter |- loaded" and 7.30 7.31 load2: 7.32 - "dollar , quarter |- loaded" 7.33 + "dollar , quarter |- loaded" and 7.34 7.35 wash: 7.36 - "loaded , dirty |- wet" 7.37 + "loaded , dirty |- wet" and 7.38 7.39 dry: 7.40 "wet, quarter , quarter , quarter |- clean"