Code

Twp#11

Code

Merged

hei411 merged 43 commits intomainlogsem/clutch:mainfrom twplogsem/clutch:twpCopy head branch name to clipboardJan 26, 2024

+2,541-39

Commits

Commits on Jan 9, 2024

• starting to write total weakest pre

  hei411

  committed
  0694eb9

  Copy full SHA for 0694eb9

Commits on Jan 10, 2024

• First file for twp completed

  hei411

  committed
  6b53586

  Copy full SHA for 6b53586

• start working on adequacy

  hei411

  committed
  68e9aa4

  Copy full SHA for 68e9aa4

• some progress

  hei411

  committed
  605f0c0

  Copy full SHA for 605f0c0

• state lemma of another induction hypothesis for twp, it is admitted for now

  hei411

  committed
  71e3be4

  Copy full SHA for 71e3be4

• Added real_le_limit lemma

  hei411

  committed
  d2b2b80

  Copy full SHA for d2b2b80

• Added limit rules

  hei411

  committed
  230143e

  Copy full SHA for 230143e

Commits on Jan 11, 2024

• added strong fixpoint rule

  hei411

  committed
  a1c39e5

  Copy full SHA for a1c39e5

• Complete stronger induction lemma

  hei411

  committed
  45e2230

  Copy full SHA for 45e2230

• small add

  hei411

  committed
  7886b53

  Copy full SHA for 7886b53

• Small fix

  hei411

  committed
  fc60504

  Copy full SHA for fc60504

• make more progress on another induction lemma

  hei411

  committed
  efdcc0e

  Copy full SHA for efdcc0e

• Solved ind'

  hei411

  committed
  5d04db1

  Copy full SHA for 5d04db1

Commits on Jan 12, 2024

• simplify some hypothesis

  hei411

  committed
  be10159

  Copy full SHA for be10159

• translate adequacy to just pure lemmas

  hei411

  committed
  ac69142

  Copy full SHA for ac69142

• small change

  hei411

  committed
  3bced86

  Copy full SHA for 3bced86

• Completed val case

  hei411

  committed
  ac3d35d

  Copy full SHA for ac3d35d

Commits on Jan 22, 2024

• Now remaining two ugly lemmas

  hei411

  committed
  89af689

  Copy full SHA for 89af689

• COMPLETED

  hei411

  committed
  1931b32

  Copy full SHA for 1931b32

Commits on Jan 23, 2024

• ported continuity laws and prove the ones for ub_logic wp and app coupl wp

  hei411

  committed
  88ba1b3

  Copy full SHA for 88ba1b3

• Implement limit adequacy theorem for ub twp

  hei411

  committed
  c048e6d

  Copy full SHA for c048e6d

• Merge pull request #10 from hei411/twp

  Show description for 15d2530
  hei411

  authored
  15d2530

  Copy full SHA for 15d2530

• Finish total_ub_lift lemmas

  hei411

  committed
  871899c

  Copy full SHA for 871899c

• Merge branch 'logsem:twp' into twp

  hei411

  authored
  8ea885b

  Copy full SHA for 8ea885b

• Merge pull request #12 from hei411/twp

  Show description for e544408
  hei411

  authored
  e544408

  Copy full SHA for e544408

• Add lemma on total_ub_lift and termination ineq

  hei411

  committed
  2347013

  Copy full SHA for 2347013

Commits on Jan 24, 2024

• strengthened adequacy!

  hei411

  committed
  34f7954

  Copy full SHA for 34f7954

• Merge pull request #13 from hei411/twp

  Show description for 02acbd0
  hei411

  authored
  02acbd0

  Copy full SHA for 02acbd0

• added total lifting

  hei411

  committed
  866d89a

  Copy full SHA for 866d89a

• Added total ectx lifting lemmas

  hei411

  committed
  1194fab

  Copy full SHA for 1194fab

• added stronger total_ub_lift implies ub_lift_strong

  hei411

  committed
  4d4ac7c

  Copy full SHA for 4d4ac7c

Commits on Jan 25, 2024

• total_primitive_laws

  hei411

  committed
  f52a190

  Copy full SHA for f52a190

• TODO: proofmode

  hei411

  committed
  ee86b90

  Copy full SHA for ee86b90

• started proofmode

  hei411

  committed
  af5267e

  Copy full SHA for af5267e

• Adding total proof_mode

  hei411

  committed
  e4666ed

  Copy full SHA for e4666ed

• Merge pull request #4 from hei411/main

  Show description for 6223b70
  hei411

  authored
  6223b70

  Copy full SHA for 6223b70

• working on ub_rules

  hei411

  committed
  4feb23c

  Copy full SHA for 4feb23c

• added merge of the rand adv lemma

  hei411

  committed
  12ec67e

  Copy full SHA for 12ec67e

• twp lemmas in ub_rules except those in approximate lifting

  hei411

  committed
  17c8098

  Copy full SHA for 17c8098

• Changed ub_rules completely

  hei411

  committed
  c7f2e72

  Copy full SHA for c7f2e72

Commits on Jan 26, 2024

• Merge pull request #16 from hei411/twp

  Show description for e5638af
  hei411

  authored
  e5638af

  Copy full SHA for e5638af

• Merge branch 'main' into twp

  hei411

  authored
  5a30f5c

  Copy full SHA for 5a30f5c

• Fix build to include Markus' stuff

  hei411

  committed
  b6601e3

  Copy full SHA for b6601e3