my forest
weeknotes, isa finished
+282
-3
assets/lss1.jpeg
assets/lss1.jpeg
This is a binary file and will not be displayed.
assets/lss2.jpeg
assets/lss2.jpeg
This is a binary file and will not be displayed.
assets/lss3.jpeg
assets/lss3.jpeg
This is a binary file and will not be displayed.
assets/lss4.jpeg
assets/lss4.jpeg
This is a binary file and will not be displayed.
assets/lss5.jpeg
assets/lss5.jpeg
This is a binary file and will not be displayed.
+2
-2
trees/isa/isa-0001.tree
+2
-2
trees/isa/isa-0001.tree
···
1
-
\title{Interactive theorem proving (draft)}
1
+
\title{Interactive theorem proving}
2
2
\author{liamoc}
3
3
\taxon{Lecture Notes}
4
-
\p{These notes are the basis of my short course at the [ANU Logic Summer School]() 2025. \strong{THEY ARE NOT YET COMPLETE.}}
4
+
\p{These notes are the basis of my short course at the [ANU](anu) Logic Summer School 2025.}
5
5
\transclude{isa-0002}
6
6
\transclude{isa-001B}
7
7
\transclude{isa-002N}
+1
trees/loc-001B.tree
+1
trees/loc-001B.tree
+1
-1
trees/loc-002I.tree
+1
-1
trees/loc-002I.tree
···
7
7
\date{2025-11-30}
8
8
\author{liamoc}
9
9
\quote{
10
-
Ad te levávi ánimam méam: Déus méus in te oncido, non erubéscam: neque irrídeant me inimíci mei: étenim univérsi qui te expéctant, non confundéntur.}
10
+
Ad te levávi ánimam méam: Déus méus in te confido, non erubéscam: neque irrídeant me inimíci mei: étenim univérsi qui te expéctant, non confundéntur.}
11
11
\p{This Sunday at [All Saints Ainslie](https://allsaintsainslie.org.au) we were almost pre-warmed up from our rehearsal yesterday (for next week's Carol service). We sang Waters' lovely short anthem [I sing of a maiden that is mateless](https://www.youtube.com/watch?v=s6uU6lk4kd4):}
12
12
\quote{
13
13
\poem{
+256
trees/loc-002L.tree
+256
trees/loc-002L.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{2nd Sunday of Advent 2025}
6
+
\tag{cmc}
7
+
\date{2025-12-07}
8
+
\author{liamoc}
9
+
\quote{
10
+
Populus Sion, ecce Dóminus véniet ad salvándas gentes: et audítam fáciet Dóminus glóriam vocis suæ, in lætítia cordis vestri.}
11
+
\p{This was a big Sunday at [All Saints Ainslie](https://allsaintsainslie.org.au). In the morning a small group of us sang Bach's [Jesu, Joy of Man's Desiring](https://www.youtube.com/watch?v=T5Df7f_BLU8):}
12
+
\quote{
13
+
\poem{
14
+
\line{Jesu, joy of man's desiring,}
15
+
\line{Holy wisdom, love most bright;}
16
+
\line{Drawn by Thee, our souls aspiring}
17
+
\line{Soar to uncreated light.\br}
18
+
19
+
\line{Word of God, our flesh that fashioned,}
20
+
\line{With the fire of life impassioned,}
21
+
\line{Striving still to truth unknown,}
22
+
\line{Soaring, dying round Thy throne.\br}
23
+
24
+
\line{Through the way where hope is guiding,}
25
+
\line{Hark, what peaceful music rings;}
26
+
\line{Where the flock, in Thee confiding,}
27
+
\line{Drink of joy from deathless springs.\br}
28
+
29
+
\line{Theirs is beauty's fairest pleasure;}
30
+
\line{Theirs is wisdom's holiest treasure.}
31
+
\line{Thou dost ever lead Thine own}
32
+
\line{In the love of joys unknown.}
33
+
}
34
+
}
35
+
\p{But, more significantly, we had our annual Lessons and Carols service. I cantored for the initial [Matin Responsory](https://www.youtube.com/watch?v=9uJdSvo1e2U) based on a Nunc Dimittis by Palestrina (despite the fact the Carols for Choirs edition says it's based on a Magnificat):}
36
+
\quote{\poem{\line{\strong{I look from afar,}}
37
+
\line{And lo, I see the power of God coming, and a cloud covering the whole Earth.}
38
+
\line{\strong{Go ye out to meet him and say:}}
39
+
\line{Tell us, art thou he that should come to reign over thy people Israel?}
40
+
\line{High and low, rich and poor, one with another,}
41
+
\line{Go ye out to meet him and say:}
42
+
\line{Hear, O thou Shepherd of Israel, thou that leadest Joseph like a sheep,}
43
+
\line{Tell us, art thou he that should come?}
44
+
\line{Stir up thy strength, O Lord, and come}
45
+
\line{To reign over thy people, Israel.}
46
+
\line{\strong{Glory be to the Father and to the Son, and to the Holy Ghost.}}
47
+
\line{I look from afar,}
48
+
\line{And lo, I see the power of God coming, and a cloud covering the whole Earth.}
49
+
\line{Go ye out to meet him and say:}
50
+
\line{Tell us, art thou he that should come to reign over thy people Israel?}}}
51
+
52
+
\p{ We had several guest singers join us including Rachel Mink and Dan Walker from Luminescence. Rachel sang the initial verse of [Once In Royal David's City](https://www.youtube.com/watch?v=rA4Ng96nb3Y), after which we processed to the remaining verses. After the first lesson from yours truly, we performed Ord's [Adam Lay Ybounden](https://www.youtube.com/watch?v=oykLGvCfGCI): }
53
+
\quote{\poem{\line{Adam lay ybounden, bounden in a bond.}
54
+
\line{Four thousand winter thought he not too long.}
55
+
\line{And all was for an apple, an apple that he took,}
56
+
\line{As clerkes finden written in their book.}
57
+
\line{Ne had the apple taken been, the apple taken been,}
58
+
\line{Ne had never our ladye a been heavené queen.}
59
+
\line{Blessed be the time that apple taken was,}
60
+
\line{Therefore we moun singen \em{Deo Gracias}.}}}
61
+
\p{Following another reading, we had one of my favourite Christmas classics, Prätorius' [Es ist ein Ros' entsprungen](https://www.youtube.com/watch?v=7RjAXOcTebI). }
62
+
\quote{
63
+
\table{
64
+
\tr{
65
+
\td{Es ist ein Ros entsprungen,}
66
+
\td{There is a rose up-springing,}
67
+
}\tr{
68
+
\td{aus einer Wurzel zart,}
69
+
\td{from a tender root,}
70
+
}\tr{
71
+
\td{wie uns die Alten sungen,}
72
+
\td{as the ancients have sung,}
73
+
}\tr{
74
+
\td{von Jesse kam die Art}
75
+
\td{it comes from Jesse's branch.}
76
+
}\tr{
77
+
\td{und hat ein Blümlein bracht}
78
+
\td{Its blossom flowering bright,}
79
+
}\tr{
80
+
\td{mitten im kalten Winter,}
81
+
\td{amidst the cold winter,}
82
+
}\tr{
83
+
\td{wohl zu der halben Nacht.}
84
+
\td{when half the night remains.}
85
+
}\tr{
86
+
\td{\br}
87
+
\td{}
88
+
}\tr{
89
+
\td{Das Röslein, das ich meine,}
90
+
\td{This little rose of which I sing,}
91
+
}\tr{
92
+
\td{davon Jesaja sagt,}
93
+
\td{of which Isaiah spoke, }
94
+
}\tr{
95
+
\td{hat uns gebracht alleine}
96
+
\td{was brought to us solely by}
97
+
}\tr{
98
+
\td{Marie, die reine Magd.}
99
+
\td{Mary, the pure maiden.}
100
+
}\tr{
101
+
\td{Aus Gottes ew'gem Rat}
102
+
\td{By God's eternal plan,}
103
+
}\tr{
104
+
\td{hat sie ein Kind geboren}
105
+
\td{a child was born to her}
106
+
}\tr{
107
+
\td{und blieb doch reine Magd.}
108
+
\td{but she remained a pure Maiden.}
109
+
}\tr{
110
+
\td{\br}
111
+
\td{}
112
+
}\tr{
113
+
\td{Das Blümelein so kleine,}
114
+
\td{That little blossom, so tiny,}
115
+
}\tr{
116
+
\td{das duftet uns so süß,}
117
+
\td{that to us smells so sweet,}
118
+
}\tr{
119
+
\td{mit seinem hellen Scheine}
120
+
\td{with its bright shining}
121
+
}\tr{
122
+
\td{Vertreibt's die Finsternis.}
123
+
\td{drives away the darkness.}
124
+
}\tr{
125
+
\td{Wahr' Mensch und wahrer Gott,}
126
+
\td{True man and truer God,}
127
+
}\tr{
128
+
\td{hilft uns aus allem Leide,}
129
+
\td{He aids us from all suffering,}
130
+
}\tr{
131
+
\td{rettet von Sünd und Tod.}
132
+
\td{and saves us from sin and death.}
133
+
}
134
+
}
135
+
}
136
+
\p{After the next reading was the original traditonal arrangement of the [Coventry Carol](https://www.youtube.com/watch?v=WII-nEAykqY) with the crunchy false relation in the cadence.}
137
+
\quote{
138
+
\poem{
139
+
\line{Lully, lullay, þow littell tyne childe,}
140
+
\line{by, by, lully, lullay.}
141
+
\line{þow littell tyne childe:}
142
+
\line{by, by, lully, lullay.}
143
+
\line{\br}
144
+
\line{O! Sisters too, how may we do}
145
+
\line{for to preserve this day}
146
+
\line{this pore yongling for whom we do singe:}
147
+
\line{by, by, lully, lullay?}
148
+
\line{\br}
149
+
\line{Herod, the king, in his raging,}
150
+
\line{chargid he hath this day,}
151
+
\line{his men of might in his owne sight,}
152
+
\line{all yonge children to slay.}
153
+
\line{\br}
154
+
\line{That wo is me, pore childe, for Thee}
155
+
\line{and ever morne and day}
156
+
\line{for thi parting nether say nor singe:}
157
+
\line{by, by, lully, lullay.}
158
+
}
159
+
}
160
+
\p{The next reading was followed by [O little town of Bethlehem](https://www.youtube.com/watch?v=LRuXdOb6TrA) with the Willcocks descant. Then, after the next reading we sang the \em{significantly} less common arrangement of the Basque carol \em{Gabriel's Message}, also known as \em{the Angel Gabriel} or the [Most Highly Flavoured Gravy](https://www.youtube.com/watch?v=RJnJ6Ko_kyw).}
161
+
\quote{
162
+
\poem{
163
+
\line{The Angel Gabriel from heaven came,}
164
+
\line{his wings as drifted snow, his eyes as flame;}
165
+
\line{'All hail', said he, 'thou lowly maiden Mary}
166
+
\line{Most highly favoured lady, \em{Gloria}.'}
167
+
\line{\br}
168
+
\line{'For known a blesséd Mother thou shalt be,}
169
+
\line{all generations laud and honour thee,}
170
+
\line{thy Son shall be Immanuel by seers foretold;}
171
+
\line{Most highly favoured lady, \em{Gloria}.'}
172
+
\line{\br}
173
+
\line{Then gentle Mary meekly bowed her head,}
174
+
\line{'To me be as it pleaseth God', she said,}
175
+
\line{'My soul shall laud and magnify his holy name':}
176
+
\line{most highly favoured lady, \em{Gloria}.}
177
+
\line{\br}
178
+
\line{Of her, Immanuel, the Christ was born}
179
+
\line{in Bethlehem all on a Christmas morn,}
180
+
\line{and Christian folk throughout the world will ever say:}
181
+
\line{'most highly favoured lady, \em{Gloria}.'}
182
+
}
183
+
}
184
+
\p{After one more reading, we performed what I think was a highlight of the whole service, and one of our best performances, Lauridsen's [O Magnum Mysterium](https://www.youtube.com/watch?v=tZ-nuU-hda8):}
185
+
\quote{
186
+
\table{
187
+
\tr{
188
+
\td{O mágnum mystérium}
189
+
\td{O great mystery,}
190
+
}\tr{
191
+
\td{et admirábile sacraméntum,}
192
+
\td{and wondrous sacrament,}
193
+
}\tr{
194
+
\td{ut animália vidérent Dóminum nátum,}
195
+
\td{that animals should see the newborn Lord,}
196
+
}\tr{
197
+
\td{jacéntem in præsépio.}
198
+
\td{lying in a manger.}
199
+
}\tr{
200
+
\td{Beáta virgo, cújus víscera meruérunt}
201
+
\td{Blessed virgin, whose womb was worthy}
202
+
}\tr{
203
+
\td{portáre Dóminum Chrístum. Alleluia}
204
+
\td{to bear the Lord Christ. Alleluia}
205
+
}
206
+
}
207
+
}
208
+
\p{Then we processed out [while shepherds washed their socks](https://www.youtube.com/watch?v=ZOA2Y9Ms34s) and ascended to the organ loft for the remainder of the service, where we performed Warlock's [Bethlehem Down](https://www.youtube.com/watch?v=gQnuxaqbYx8). I heard that anthem was written on a napkin by an alcoholic and antitheist Peter Warlock in exchange for beer money, and that he died a few years after writing it. But the anthem itself is quite special.}
209
+
\quote{\poem{\line{When He is King we will give him the King's gifts,}
210
+
\line{Myrrh for its sweetness, and gold for a crown,}
211
+
\line{"Beautiful robes", said the young girl to Joseph}
212
+
\line{Fair with her first-born on Bethlehem Down.}
213
+
\line{\br}
214
+
\line{Bethlehem Down is full of the starlight}
215
+
\line{Winds for the spices, and stars for the gold,}
216
+
\line{Mary for sleep, and for lullaby music}
217
+
\line{Songs of a shepherd by Bethlehem fold.}
218
+
\line{\br}
219
+
\line{When He is King they will clothe Him in grave-sheets,}
220
+
\line{Myrrh for embalming, and wood for a crown,}
221
+
\line{He that lies now in the white arms of Mary}
222
+
\line{Sleeping so lightly on Bethlehem Down.}
223
+
\line{\br}
224
+
\line{Here He has peace and a short while for dreaming,}
225
+
\line{Close-huddled oxen to keep Him from cold,}
226
+
\line{Mary for love, and for lullaby music}
227
+
\line{Songs of a shepherd by Bethlehem fold.}}}
228
+
\p{This was followed by another congregational carol with Willcocks descant, [Hark the Herald Angels Sing](https://www.youtube.com/watch?v=9Bwn0k0k8xI) and our last anthem of the evening, Wood's [Hey you! The Middle Ball](https://www.youtube.com/watch?v=Qf202pdjMZk). }
229
+
\quote{
230
+
\poem{
231
+
\line{O thou the central orb of righteous love,}
232
+
\line{Pure beam of the Most High,}
233
+
\line{Eternal Light of this our wintry world,}
234
+
\line{Thy radiance bright awakes new joy in faith,}
235
+
\line{Hope soars above.}
236
+
\line{\br}
237
+
\line{Come, quickly come and let thy glory shine,}
238
+
\line{Gilding our darksome heav'n with rays divine.}
239
+
\line{Thy saints with holy lustre round thee move,}
240
+
\line{As stars about thy throne, set in the height}
241
+
\line{Of God's ordaining counsel, }
242
+
\line{As thy sight gives measured grace to each.}
243
+
\line{Thy power to prove.}
244
+
\line{\br}
245
+
\line{Let thy bright beams disperse the gloom of sin,}
246
+
\line{Our nature all shall feel eternal day,}
247
+
\line{In fellowship with thee,}
248
+
\line{Transforming day to souls erewhile unclean,}
249
+
\line{now pure within.}
250
+
\line{\br}
251
+
\line{Amen.}
252
+
}
253
+
}
254
+
\p{Of course, it wouldn't be a Christmas Carols service without the "Word of the Father" chord, so we finished up with Willcocks' arrangement of [O Come, All Ye Faithful](https://www.youtube.com/watch?v=RkS57yCIk7E).
255
+
}
256
+
+15
trees/loc-002M.tree
+15
trees/loc-002M.tree
···
1
+
\date{2025-12-06T06:45:05Z}
2
+
\author{liamoc}
3
+
\title{The first week of LSS is over}
4
+
\figure{
5
+
\<html:img>[width]{250px}[src]{\route-asset{assets/lss5.jpeg}}{}
6
+
}
7
+
\p{The first week of the [ANU](anu) Logic Summer School has concluded, including my introductory course on [[isa-0001]]. I think the course went well and students learnt a little of what makes theorem proving fun. Chelsea Edmonds will follow on from my course in week 2 with her own course on software verification. I hope I prepared the students well. We went on an excursion to the Tidbinbilla nature reserve (photos of which I have also previously shared on [[2025-W27]] and [[2025-W44]]).}
8
+
\figure{
9
+
\<html:img>[width]{250px}[src]{\route-asset{assets/lss4.jpeg}}{}
10
+
\<html:img>[width]{250px}[src]{\route-asset{assets/lss3.jpeg}}{}
11
+
\<html:img>[width]{250px}[src]{\route-asset{assets/lss2.jpeg}}{}
12
+
\<html:img>[width]{250px}[src]{\route-asset{assets/lss1.jpeg}}{}
13
+
\figcaption{Various Australian fauna seen at Tidbinbilla}
14
+
}
15
+
\p{It was a lot of fun to show some of our visiting students some of the natural landscapes so easily accessible from Canberra. I think we all had a really good day, even though it was sweltering hot. }
+7
trees/weeknotes/2025-W49.tree
+7
trees/weeknotes/2025-W49.tree
···
1
+
\import{table-macros}
2
+
\title{Weeknotes 2025-W49}
3
+
\author{liamoc}
4
+
\date{2025-12-07}
5
+
\p{Much of this past week was spent organising for my Logic Summer School course or preparing for the Service of Lessons and Carols at Ainslie. Both went well I think! But I was so exhausted last night that these weeknotes are a day late.}
6
+
\transclude{loc-002M}
7
+
\transclude{loc-002L}