DiagonalEvaluation.lean`

436 declarations, 0 contain sorry, 0 declared as axioms

Diagonal estimator evaluation, inherited queries, and resource bounds.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

structure OAI.ExactDerandomization.Vessel.OrbitV line 27
Source documentation
Prism for diagonal, endpoint channel frozen nevertheless read.
```
structure OrbitV (u:Line (q:=q) (w:=w) (h:=h)) where
…
```
abbrev OAI.ExactDerandomization.Vessel.OrbitV.tire line 33
abbrev OAI.ExactDerandomization.Vessel.OrbitV.r line 34
abbrev OAI.ExactDerandomization.Vessel.OrbitV.s line 35
abbrev OAI.ExactDerandomization.Vessel.OrbitV.d line 36
abbrev OAI.ExactDerandomization.Vessel.OrbitV.ds line 37
abbrev OAI.ExactDerandomization.Vessel.OrbitV.S line 38
abbrev OAI.ExactDerandomization.Vessel.OrbitV.channel line 39
def OAI.ExactDerandomization.Vessel.OrbitV.works line 40
def OAI.ExactDerandomization.Vessel.OrbitV.estate line 41
abbrev OAI.ExactDerandomization.Vessel.OrbitV.fwd0 line 42
abbrev OAI.ExactDerandomization.Vessel.OrbitV.raw0 line 43
abbrev OAI.ExactDerandomization.Vessel.OrbitV.chipV line 44
lemma OAI.ExactDerandomization.Vessel.OrbitV.goal0 line 45
lemma OAI.ExactDerandomization.Vessel.OrbitV.pos0 line 54
lemma OAI.ExactDerandomization.Vessel.OrbitV.next0 line 55
abbrev OAI.ExactDerandomization.Vessel.OrbitV.actual line 58
lemma OAI.ExactDerandomization.Vessel.OrbitV.pays line 61
abbrev OAI.ExactDerandomization.Vessel.OrbitV.VoteM line 63
lemma OAI.ExactDerandomization.Vessel.OrbitV.clamp0 line 65
lemma OAI.ExactDerandomization.Vessel.OrbitV.settle line 81
structure OAI.ExactDerandomization.Vessel.OrbitV.Counsel line 89
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.unitV line 96
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.pred0 line 99
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.heightZ line 106
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.costZ line 108
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.foreign line 110
structure OAI.ExactDerandomization.Vessel.OrbitV.Earn line 117
def OAI.ExactDerandomization.Vessel.OrbitV.FEnd line 122
abbrev OAI.ExactDerandomization.Vessel.PlanV.x line 146
abbrev OAI.ExactDerandomization.Vessel.PlanV.sensor line 147
abbrev OAI.ExactDerandomization.Vessel.PlanV.j line 148
def OAI.ExactDerandomization.Vessel.PlanV.trees line 149
def OAI.ExactDerandomization.Vessel.PlanV.lead line 152
abbrev OAI.ExactDerandomization.Vessel.PlanV.radius line 155
def OAI.ExactDerandomization.Vessel.PlanV.beats line 156
def OAI.ExactDerandomization.Vessel.PlanV.validV line 160
lemma OAI.ExactDerandomization.Vessel.PlanV.treeC line 165
lemma OAI.ExactDerandomization.Vessel.PlanV.playG line 174
lemma OAI.ExactDerandomization.Vessel.PlanV.formVK line 191
abbrev OAI.ExactDerandomization.Vessel.OrbitV.c line 202
abbrev OAI.ExactDerandomization.Vessel.OrbitV.areaV line 203
abbrev OAI.ExactDerandomization.Vessel.OrbitV.grounds line 204
lemma OAI.ExactDerandomization.Vessel.OrbitV.agroV line 205
lemma OAI.ExactDerandomization.Vessel.OrbitV.awakeV line 218
lemma OAI.ExactDerandomization.Vessel.OrbitV.fuel line 222
def OAI.ExactDerandomization.Vessel.Sun.appear line 248
def OAI.ExactDerandomization.Vessel.Sun.festival line 251
def OAI.ExactDerandomization.Vessel.Sun.trigger line 254
def OAI.ExactDerandomization.Vessel.Sun.crystal line 258
abbrev OAI.ExactDerandomization.Vessel.Sun.prior line 261
def OAI.ExactDerandomization.Vessel.Sun.velvet line 262
abbrev OAI.ExactDerandomization.Vessel.Sun.sail line 264
def OAI.ExactDerandomization.Vessel.Sun.chest line 266
def OAI.ExactDerandomization.Vessel.Sun.pasty line 269
abbrev OAI.ExactDerandomization.Vessel.Sun.scheduleR line 271
abbrev OAI.ExactDerandomization.Vessel.Sun.script line 272
def OAI.ExactDerandomization.Vessel.Sun.priceC line 275
lemma OAI.ExactDerandomization.Vessel.Sun.Script.invar line 281
lemma OAI.ExactDerandomization.Vessel.Sun.Script.estimate line 289
structure OAI.ExactDerandomization.Vessel.Basket.Sack line 303
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.a line 311
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.d line 312
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.Pn line 313
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.h0 line 314
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.wallet line 315
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.τ line 316
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.urn line 317
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.home line 318
abbrev OAI.ExactDerandomization.Vessel.Basket.Sack.I line 319
structure OAI.ExactDerandomization.Vessel.Basket.Sack.Ground line 320
def OAI.ExactDerandomization.Vessel.Basket.Sack.priorE line 327
structure OAI.ExactDerandomization.Vessel.Basket.Sack.harvest line 330
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.wages line 337
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.pro line 338
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.guest line 339
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.phase0 line 344
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.deco0 line 346
abbrev OAI.ExactDerandomization.Vessel.Fort.MeterQ line 369
abbrev OAI.ExactDerandomization.Vessel.Fort.Manta line 371
abbrev OAI.ExactDerandomization.Vessel.Fort.MeterQ.h0 line 373
abbrev OAI.ExactDerandomization.Vessel.Fort.MeterQ.headQ line 374
abbrev OAI.ExactDerandomization.Vessel.Fort.MeterQ.i line 375
abbrev OAI.ExactDerandomization.Vessel.Fort.MeterQ.value line 376
abbrev OAI.ExactDerandomization.Vessel.Fort.MeterQ.ago line 377
abbrev OAI.ExactDerandomization.Vessel.Fort.MeterQ.hereP line 378
abbrev OAI.ExactDerandomization.Vessel.Fort.MeterQ.pt line 379
abbrev OAI.ExactDerandomization.Vessel.Fort.tea line 382
abbrev OAI.ExactDerandomization.Vessel.Fort.whoseK0 line 383
def OAI.ExactDerandomization.Vessel.Fort.osky line 384
def OAI.ExactDerandomization.Vessel.Fort.surf line 387
def OAI.ExactDerandomization.Vessel.Fort.light line 388
lemma OAI.ExactDerandomization.Vessel.Fort.lightK line 390
def OAI.ExactDerandomization.Vessel.Fort.nearC line 397
abbrev OAI.ExactDerandomization.Vessel.Fort.atQ line 399
abbrev OAI.ExactDerandomization.Vessel.Fort.hereId line 400
abbrev OAI.ExactDerandomization.Vessel.Fort.presentQ line 401
abbrev OAI.ExactDerandomization.Vessel.Fort.upQ line 402
abbrev OAI.ExactDerandomization.Vessel.Fort.elder line 403
abbrev OAI.ExactDerandomization.Vessel.Fort.stampF line 404
abbrev OAI.ExactDerandomization.Vessel.Fort.leave line 406
def OAI.ExactDerandomization.Vessel.Fort.secondC line 407
def OAI.ExactDerandomization.Vessel.Fort.premier line 411
def OAI.ExactDerandomization.Vessel.Fort.chip line 416
abbrev OAI.ExactDerandomization.Vessel.Fort.priorF line 417
def OAI.ExactDerandomization.Vessel.Fort.boost0 line 424
def OAI.ExactDerandomization.Vessel.Fort.bootsY line 427
abbrev OAI.ExactDerandomization.Vessel.Fort.P line 432
def OAI.ExactDerandomization.Vessel.Fort.genus line 433
abbrev OAI.ExactDerandomization.Vessel.Fort.starC line 434
def OAI.ExactDerandomization.Vessel.Fort.actorP line 435
def OAI.ExactDerandomization.Vessel.Fort.fresh line 436
def OAI.ExactDerandomization.Vessel.Fort.mixC line 437
def OAI.ExactDerandomization.Vessel.Fort.syncC line 440
def OAI.ExactDerandomization.Vessel.Fort.drill line 443
def OAI.ExactDerandomization.Vessel.Fort.base line 447
def OAI.ExactDerandomization.Vessel.Fort.radiate line 455
def OAI.ExactDerandomization.Vessel.PrintV.topHull line 482
lemma OAI.ExactDerandomization.Vessel.PrintV.topK line 489
abbrev OAI.ExactDerandomization.Vessel.PrintV.sh line 493
abbrev OAI.ExactDerandomization.Vessel.PrintV.vshot line 494
abbrev OAI.ExactDerandomization.Vessel.PrintV.dshot line 495
abbrev OAI.ExactDerandomization.Vessel.PrintV.eshot line 496
def OAI.ExactDerandomization.Vessel.PrintV.detectors line 498
def OAI.ExactDerandomization.Vessel.PrintV.roy line 500
abbrev OAI.ExactDerandomization.Vessel.PrintV.dawn line 508
abbrev OAI.ExactDerandomization.Vessel.PrintV.black line 509
def OAI.ExactDerandomization.Vessel.PrintV.model line 512
lemma OAI.ExactDerandomization.Vessel.PrintV.shK line 531
lemma OAI.ExactDerandomization.Vessel.PrintV.vhK line 533
lemma OAI.ExactDerandomization.Vessel.PrintV.dhK line 535
lemma OAI.ExactDerandomization.Vessel.PrintV.ehK line 537
lemma OAI.ExactDerandomization.Vessel.PrintV.dewK line 539
lemma OAI.ExactDerandomization.Vessel.PrintV.royp line 544
lemma OAI.ExactDerandomization.Vessel.PrintV.modelK line 557
def OAI.ExactDerandomization.Vessel.PrintV.garment line 580
lemma OAI.ExactDerandomization.Vessel.PrintV.garmentK line 587
def OAI.ExactDerandomization.Vessel.PrintV.shell line 595
lemma OAI.ExactDerandomization.Gamut.Shift.audible line 616
lemma OAI.ExactDerandomization.Gamut.Shift.motion line 622

lemma OAI.ExactDerandomization.Gamut.Shift.asked line 636

Source documentation

Hear open units by two predicates.

lemma asked(a) (hm : ∀ i j o,a≠0→Orbit.taps (uphold a).1 o j→u.smallQ a i→j  ≤  u.D.high a→
                    ∀ x∈u.D.P,∃ z,u.D.swears (post a o i j) x z)
     (hc :∀ i t,u.D.dual (hole a i) t→ ∃ f,u.D.Streams (hole a i) f) :
   u.D.Ears0 a:=by
…

lemma OAI.ExactDerandomization.Gamut.Shift.incline line 649
lemma OAI.ExactDerandomization.Gamut.Shift.free line 655
lemma OAI.ExactDerandomization.Gamut.Shift.basic line 658
lemma OAI.ExactDerandomization.Gamut.Shift.earsTag line 662
lemma OAI.ExactDerandomization.Gamut.Shift.terminal line 673
lemma OAI.ExactDerandomization.Gamut.Shift.eventE line 691
lemma OAI.ExactDerandomization.Gamut.Shift.court line 706
abbrev OAI.ExactDerandomization.Gamut.Pond.serveR line 735
abbrev OAI.ExactDerandomization.Gamut.Pond.serveE line 736
abbrev OAI.ExactDerandomization.Gamut.Pond.reapT line 737
abbrev OAI.ExactDerandomization.Gamut.Pond.reapE line 738
abbrev OAI.ExactDerandomization.Gamut.Pond.rankR line 739
abbrev OAI.ExactDerandomization.Gamut.Pond.rankE line 740
def OAI.ExactDerandomization.Gamut.Pond.TracedR line 741
def OAI.ExactDerandomization.Gamut.Pond.TracedE line 744
structure OAI.ExactDerandomization.Gamut.Pond.Books line 747
lemma OAI.ExactDerandomization.Gamut.Pond.Books.nonn line 758
lemma OAI.ExactDerandomization.Gamut.Pond.Books.echoR line 760
lemma OAI.ExactDerandomization.Gamut.Pond.Books.sunny line 775
lemma OAI.ExactDerandomization.Gamut.Pond.Books.echoE line 777
abbrev OAI.ExactDerandomization.Vessel.GoodF.hour line 822
abbrev OAI.ExactDerandomization.Vessel.GoodF.treasury line 823
lemma OAI.ExactDerandomization.Vessel.GoodF.bloss line 827
lemma OAI.ExactDerandomization.Vessel.GoodF.estimated line 833
structure OAI.ExactDerandomization.Vessel.Sleigh.Wax line 862
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.quote0 line 869
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.s0 line 870
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.f line 871
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.g line 872
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.plant line 873
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.due line 874
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.k0 line 875
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.H line 876
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.T line 877
structure OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good line 879
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.meter line 890
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.nums line 891
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.charged line 896
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.through line 897
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.remains line 899
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.foster line 915
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.lampY line 916
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.shines line 917
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.body0 line 924
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.trunk line 927
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.void0 line 930
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.snows line 931
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.dark line 935
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.Approved line 968
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.postX line 970
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.moneyX line 973
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.tunesF line 975
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.amountP line 976
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.pullP line 977
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.middleP line 978
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.spend0 line 986
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.abi line 987
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.bornC line 992
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.crust0 line 1000
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.power0 line 1006
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.solvent line 1010
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.stamp0 line 1018
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.boil0 line 1030
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.money_ok line 1039
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.boonBase line 1042
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.headC line 1052
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.boonEye line 1054
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.smoke line 1085
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.choir0 line 1089
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.waitsage line 1098
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.aware line 1130
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.surfaces line 1136
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.housing line 1143
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.total line 1160
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.console line 1172
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.pastlore line 1195
lemma OAI.ExactDerandomization.Vessel.Basket.Sack.Ground.advances line 1199
abbrev OAI.ExactDerandomization.Vessel.Ferry.core0 line 1235
abbrev OAI.ExactDerandomization.Vessel.Ferry.valid0 line 1236
abbrev OAI.ExactDerandomization.Vessel.Ferry.blanket line 1237
abbrev OAI.ExactDerandomization.Vessel.Ferry.flareP line 1238
abbrev OAI.ExactDerandomization.Vessel.Ferry.phantom line 1239
abbrev OAI.ExactDerandomization.Vessel.Ferry.AE line 1240
abbrev OAI.ExactDerandomization.Vessel.Ferry.W0 line 1241
abbrev OAI.ExactDerandomization.Vessel.Ferry.heats line 1242
abbrev OAI.ExactDerandomization.Vessel.Ferry.Wlive line 1243
structure OAI.ExactDerandomization.Vessel.Ferry.TorchE line 1245
structure OAI.ExactDerandomization.Vessel.Ferry.Wells line 1251
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.vfen line 1260
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.hou0 line 1262
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.Qyet line 1265
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.Qend line 1279
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.lampq line 1291
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.parked line 1298
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.fitted line 1301
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.else0 line 1306
lemma OAI.ExactDerandomization.Vessel.Ferry.TorchE.tabs0 line 1313
structure OAI.ExactDerandomization.Vessel.Ferry.ArcQ line 1320
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.k line 1325
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.φ line 1326
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.bx line 1327
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.cur line 1328
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.forward line 1329
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.α line 1330
def OAI.ExactDerandomization.Vessel.Ferry.ArcQ.routeP line 1331
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.bill0 line 1333
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.intended line 1334
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.okQ line 1335
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.hullK line 1336
structure OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand line 1338
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.zone line 1344
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.price0 line 1346
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.cost0 line 1348
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.swift line 1351
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.ll0 line 1358
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.sigmas line 1359
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.stanza line 1364
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.chaste line 1371
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.voice0 line 1375
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.steam0 line 1385
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.K line 1411
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.M line 1412
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.palette line 1413
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.amber line 1414
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.pores line 1415
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.horn line 1416
structure OAI.ExactDerandomization.Vessel.Ferry.ArcQ.VisitF line 1419
abbrev OAI.ExactDerandomization.Vessel.Ferry.ArcQ.prickF line 1422
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.united0 line 1427
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.signalF line 1432
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.deserted line 1435
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.aged line 1440
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.reading line 1441
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.poresReady line 1444
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.step0 line 1451
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.red0 line 1456
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.cuvette line 1476
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.hearC line 1495
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.heightB line 1504
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.marsD line 1508
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.voyage line 1531
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.midOld line 1559
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.trace0 line 1560
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.prismV line 1563
def OAI.ExactDerandomization.Vessel.Sleigh.Wax.carrierV line 1564
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.recordP line 1567
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.scoreP line 1568
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.spriteV line 1569
structure OAI.ExactDerandomization.Vessel.Sleigh.Wax.EscortV line 1571
structure OAI.ExactDerandomization.Vessel.Sleigh.Wax.PayV line 1574
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.ancient line 1582
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.whatV line 1585
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.springs line 1587
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.beforeC line 1597
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.dominion line 1618
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.influx line 1622
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.oldera line 1627
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.freshC line 1632
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.already line 1640
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.crafts line 1643
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.sperm line 1647
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.mixG line 1649
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.frostC line 1658
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.received line 1662
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.stamped line 1676
abbrev OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.shunt line 1680
lemma OAI.ExactDerandomization.Vessel.Sleigh.Wax.Good.sidle line 1682
structure OAI.ExactDerandomization.Vessel.Ferry.Slant line 1712
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.k line 1719
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.xB line 1720
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.xR line 1721
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.blade0 line 1722
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.born line 1723
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.g0 line 1724
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.impala line 1725
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.startO line 1726
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.temple line 1727
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.stopE line 1728
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.Hport line 1729
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.f0 line 1730
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.hitC line 1731
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.onC line 1732
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.dyeV line 1733
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.ptr line 1734
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.pad0 line 1735
structure OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride line 1736
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.frost line 1746
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.agedE line 1747
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.north line 1752
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.ap0 line 1755
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.startS line 1757
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.stopS line 1762
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.clay line 1767
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.pointI line 1802
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.autocross line 1811
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.dim line 1817
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.pale line 1825
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.hop line 1855
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.boot0 line 1856
def OAI.ExactDerandomization.Vessel.Ferry.Slant.archive line 1857
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.Y line 1858
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.Z line 1859
structure OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward line 1861
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.fame0 line 1869
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.clue0 line 1870
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.dawn0 line 1871
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.canon0 line 1872
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.watt0 line 1873
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.serves line 1874
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.northV line 1881
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.cycleF line 1888
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.arctic line 1898
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.Ybound line 1920
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.genuine line 1924
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.Zbound line 1929
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.routeC line 1931
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.stroke0 line 1933
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.dives line 1937
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.flow1 line 1987
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.hueP line 1988
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.flowQ line 1989
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.score0 line 1993
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.songC line 1999
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.tagL line 2010
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.mot line 2021
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.blood line 2031
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.used1 line 2043
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ward.usedQ line 2059
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.SceneF line 2114
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.headA line 2115
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.headB line 2116
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.beacon line 2117
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.sense1 line 2119
abbrev OAI.ExactDerandomization.Vessel.Ferry.Slant.senseB line 2120
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.glimpse line 2124
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.prumb line 2129
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.mumb line 2153
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.primes line 2180
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.ship1 line 2207
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.shipB line 2228
lemma OAI.ExactDerandomization.Vessel.Ferry.Slant.Ride.transported line 2242
lemma OAI.ExactDerandomization.Vessel.Ferry.ArcQ.Hand.inherit0 line 2271
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.ZeroS line 2294
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.zero0 line 2295
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.bandF line 2296
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.bandS line 2297
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.zcost line 2298
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.areaS line 2299
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.stars line 2300
def OAI.ExactDerandomization.Vessel.Ferry.Perch.brief line 2301
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.jar line 2302
abbrev OAI.ExactDerandomization.Vessel.Ferry.Perch.jug line 2303
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.rayC line 2304
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.urn_id line 2310
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.sensed line 2330
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.begun line 2333
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.aperture line 2342
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.TorchE.kosmos line 2353
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.TorchE.value0 line 2373
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.TorchE.cheap line 2381
lemma OAI.ExactDerandomization.Vessel.Ferry.Perch.TorchE.quietC line 2398
abbrev OAI.ExactDerandomization.Vessel.Ferry.galaxy line 2430
abbrev OAI.ExactDerandomization.Vessel.Ferry.orbitZ line 2431
abbrev OAI.ExactDerandomization.Vessel.Ferry.flowC line 2432
lemma OAI.ExactDerandomization.Vessel.Ferry.tagroot line 2434
lemma OAI.ExactDerandomization.Vessel.Ferry.haunt line 2436
lemma OAI.ExactDerandomization.Vessel.Ferry.atmosphere line 2441
lemma OAI.ExactDerandomization.Vessel.Ferry.Wells.grouped line 2451
lemma OAI.ExactDerandomization.Vessel.Ferry.Wells.spentQ line 2460
lemma OAI.ExactDerandomization.Vessel.Ferry.Wells.harvests line 2484
lemma OAI.ExactDerandomization.Vessel.Ferry.Wells.cockpit line 2514
abbrev OAI.ExactDerandomization.Vessel.Ma.essence line 2536
def OAI.ExactDerandomization.Vessel.Ma.brain line 2537
def OAI.ExactDerandomization.Vessel.Ma.mature line 2541
def OAI.ExactDerandomization.Vessel.Ma.sourceP line 2544
def OAI.ExactDerandomization.Vessel.Ma.shine line 2545
abbrev OAI.ExactDerandomization.Vessel.Ma.promptV line 2548
abbrev OAI.ExactDerandomization.Vessel.Ma.coal line 2549
def OAI.ExactDerandomization.Vessel.Ma.render line 2550
lemma OAI.ExactDerandomization.Vessel.Ma.wealthy line 2551
abbrev OAI.ExactDerandomization.Vessel.OrbitV.topE line 2561
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.due line 2568
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.working line 2570
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.waltz line 2584
abbrev OAI.ExactDerandomization.Vessel.OrbitV.Counsel.Hx line 2596
abbrev OAI.ExactDerandomization.Vessel.OrbitV.Counsel.Hpay line 2597
abbrev OAI.ExactDerandomization.Vessel.OrbitV.Counsel.Home line 2598
abbrev OAI.ExactDerandomization.Vessel.OrbitV.Counsel.visc line 2599
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.zen line 2601
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.piecewise line 2606
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.liveF line 2622
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.deadL line 2643
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.smallC line 2652
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.lever line 2657
lemma OAI.ExactDerandomization.Vessel.OrbitV.Counsel.knownEnd line 2668