Proof of Nuprl Lemma : new_23_sig

Step * 1 1 1 of Lemma new_23_sig_validity

1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. (f propose) = (ℤ × Cmd) ∈ Type
12. (f notify) = (ℤ × Cmd) ∈ Type
13. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
15. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
16. f ∈ Name ─→ Type
17. es : EO+(Message(f))
18. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
19. e : E@i
20. ∀e1:E
      ((e1 < e)
      ⇒ ((∀v:ℤ × Cmd
             (v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)
             ⇒ (↓∃e':E. ((e' < e1) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
         ∧ (∀v:ℤ × ℤ × Cmd × Id
              (v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
              ⇒ (↓∃e':E

                    ((e' < e1) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))

         ∧ (∀v:ℤ × ℤ × Cmd
              (v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e1)
              ⇒ (↓∃e':E. ((e' < e1) ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
         ∧ (∀e2:E
              (e2 c≤ e1
              ⇒ (∀n,rnd:ℤ. ∀c:Cmd.

                    ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e1)))

⇒ (↓∃e':E. ((e' < e1) ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))))))
21. v1 : ℤ@i
22. v2 : Cmd@i
23. <v1, v2> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)@i
24. e' : E
25. delay : ℤ
26. (e' < e)
27. loc(e') ↓∈ reps
28. e1 : {e1:E| e1 ≤loc e' }
29. z1 : ℤ
30. z2 : Cmd

31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))

∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
  ∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
  ∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
32. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
33. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
34. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
35. header(e') = ``new_23_sig vote`` ∈ Name
36. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)

37. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))

38. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
39. delay = 0 ∈ ℤ

40. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];sn\000Cd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ

41. loc(e) ↓∈ reps
42. msg-authentic(info(e)) = ff
43. v1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ

44. v2 = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))\000C)];snd(fst(msgval(e')))))) ∈ Cmd

45. ∀v:ℤ × Cmd
      (v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e')
      ⇒ (↓∃e'@0:E. ((e'@0 < e') ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))
46. ∀v:ℤ × ℤ × Cmd × Id
      (v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
      ⇒ (↓∃e'@0:E

            ((e'@0 < e') ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

47. ∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e')
⇒

 (↓∃e'@0:E. ((e'@0 < e') ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

48. ∀e2:E
      (e2 c≤ e'
      ⇒ (∀n,rnd:ℤ. ∀c:Cmd.
            ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e')))
            ⇒ (↓∃e'@0:E. ((e'@0 < e') ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))))
49. e'@0 : E
50. (e'@0 < e')
51. <v1, snd(fst(msgval(e')))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0)
⊢ ↓∃e':E. ((e' < e) ∧ <v1, v2> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))
BY
{ (InstLemma `poss-maj-unanimous` [⌈Cmd⌉;⌈eq⌉;⌈[snd(fst(msgval(e'))) /

                                                (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))]\000C⌉;⌈snd(fst(msgval(e')))⌉;⌈v2⌉]⋅

   THENA Try (QuickAuto)
   ) }

1
.....antecedent.....
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. (f propose) = (ℤ × Cmd) ∈ Type
12. (f notify) = (ℤ × Cmd) ∈ Type
13. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
15. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
16. f ∈ Name ─→ Type
17. es : EO+(Message(f))
18. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
19. e : E@i
20. ∀e1:E
      ((e1 < e)
      ⇒ ((∀v:ℤ × Cmd
             (v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)
             ⇒ (↓∃e':E. ((e' < e1) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
         ∧ (∀v:ℤ × ℤ × Cmd × Id
              (v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
              ⇒ (↓∃e':E

                    ((e' < e1) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))

                    ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e1)))

31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))

37. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))

38. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
39. delay = 0 ∈ ℤ

40. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];sn\000Cd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ

41. loc(e) ↓∈ reps
42. msg-authentic(info(e)) = ff
43. v1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ

44. v2 = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))\000C)];snd(fst(msgval(e')))))) ∈ Cmd

            ((e'@0 < e') ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

47. ∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e')
⇒

 (↓∃e'@0:E. ((e'@0 < e') ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

⊢ poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];snd(fst(m\000Csgval(e'))))

= <||[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))]||, v2>
∈ (ℕ × Cmd)

2
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. (f propose) = (ℤ × Cmd) ∈ Type
12. (f notify) = (ℤ × Cmd) ∈ Type
13. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
15. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
16. f ∈ Name ─→ Type
17. es : EO+(Message(f))
18. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
19. e : E@i
20. ∀e1:E
      ((e1 < e)
      ⇒ ((∀v:ℤ × Cmd
             (v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)
             ⇒ (↓∃e':E. ((e' < e1) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
         ∧ (∀v:ℤ × ℤ × Cmd × Id
              (v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
              ⇒ (↓∃e':E

                    ((e' < e1) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))

                    ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e1)))

31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))

37. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))

38. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
39. delay = 0 ∈ ℤ

40. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];sn\000Cd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ

41. loc(e) ↓∈ reps
42. msg-authentic(info(e)) = ff
43. v1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ

44. v2 = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))\000C)];snd(fst(msgval(e')))))) ∈ Cmd

            ((e'@0 < e') ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

47. ∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e')
⇒

 (↓∃e'@0:E. ((e'@0 < e') ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

52. (∀z∈[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))].z = v2 ∈ Cmd)

⊢ ↓∃e':E. ((e' < e) ∧ <v1, v2> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))

Latex:

Latex:
1. Cmd : \{T:Type| valueall-type(T)\} 2. eq : EqDecider(Cmd) 3. reps : bag(Id) 4. clients : bag(Id) 5. coeff : \{2...\} 6. flrs : \mBbbN{} 7. propose : Atom List 8. notify : Atom List 9. slots : set-sig\{i:l\}(\mBbbZ{}) 10. f : new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose) 11. (f propose) = (\mBbbZ{} \mtimes{} Cmd) 12. (f notify) = (\mBbbZ{} \mtimes{} Cmd) 13. (f ``new\_23\_sig decided``) = (\mBbbZ{} \mtimes{} Cmd) 14. (f ``new\_23\_sig retry``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd) 15. (f ``new\_23\_sig vote``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id) 16. f \mmember{} Name {}\mrightarrow{} Type 17. es : EO+(Message(f)) 18. new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i' 19. e : E@i 20. \mforall{}e1:E ((e1 < e) {}\mRightarrow{} ((\mforall{}v:\mBbbZ{} \mtimes{} Cmd (v \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e1) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} v \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'))))) \mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id (v \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e1) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E ((e' < e1) \mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'))))) \mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd (v \mmember{} new\_23\_sig\_retry'base(Cmd;notify;propose;f)(e1) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E ((e' < e1) \mwedge{} <fst(fst(v)), snd(v)> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'))))) \mwedge{} (\mforall{}e2:E (e2 c\mleq{} e1 {}\mRightarrow{} (\mforall{}n,rnd:\mBbbZ{}. \mforall{}c:Cmd. ((c \mmember{} fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>es.e2;e1))) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E ((e' < e1) \mwedge{} <n, c> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'))))))))) 21. v1 : \mBbbZ{}@i 22. v2 : Cmd@i 23. <v1, v2> \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e)@i 24. e' : E 25. delay : \mBbbZ{} 26. (e' < e) 27. loc(e') \mdownarrow{}\mmember{} reps 28. e1 : \{e1:E| e1 \mleq{}loc e' \} 29. z1 : \mBbbZ{} 30. z2 : Cmd 31. ((header(e1) = propose) \mwedge{} has-es-info-type(es;e1;f;\mBbbZ{} \mtimes{} Cmd) \mwedge{} (<z1, z2> = msgval(e1))) \mvee{} ((header(e1) = ``new\_23\_sig vote``) \mwedge{} has-es-info-type(es;e1;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id) \mwedge{} (z1 = (fst(fst(fst(msgval(e1)))))) \mwedge{} (z2 = (snd(fst(msgval(e1)))))) 32. \mneg{}\muparrow{}(set-sig-member(slots) z1 new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1)) 33. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e') 34. (no new\_23\_sig\_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e') 35. header(e') = ``new\_23\_sig vote`` 36. has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id) 37. \muparrow{}(new\_23\_sig\_newvote(Cmd) <z1, 0> msgval(e') new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,\000C 0>es.e1;e')) 38. ||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e'))|| = (coeff * flrs) 39. delay = 0 40. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e')))];snd(f\000Cst(msgval(e')))))) = ((coeff * flrs) + 1) 41. loc(e) \mdownarrow{}\mmember{} reps 42. msg-authentic(info(e)) = ff 43. v1 = (fst(fst(fst(msgval(e'))))) 44. v2 = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e')))];snd(fst\000C(msgval(e')))))) 45. \mforall{}v:\mBbbZ{} \mtimes{} Cmd (v \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} v \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'@0)))) 46. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id (v \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E ((e'@0 < e') \mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)( e'@0)))) 47. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd (v \mmember{} new\_23\_sig\_retry'base(Cmd;notify;propose;f)(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E ((e'@0 < e') \mwedge{} <fst(fst(v)), snd(v)> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'@0)))) 48. \mforall{}e2:E (e2 c\mleq{} e' {}\mRightarrow{} (\mforall{}n,rnd:\mBbbZ{}. \mforall{}c:Cmd. ((c \mmember{} fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>es.e2;e'))) {}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E ((e'@0 < e') \mwedge{} <n, c> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'@0)))))) 49. e'@0 : E 50. (e'@0 < e') 51. <v1, snd(fst(msgval(e')))> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'@0) \mvdash{} \mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <v1, v2> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')) By Latex: (InstLemma `poss-maj-unanimous` [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}; \mkleeneopen{}[snd(fst(msgval(e'))) / (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e')))]\mkleeneclose{};\000C\mkleeneopen{}snd(fst(msgval(e')))\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]\mcdot{} THENA Try (QuickAuto) ) Home Index