#!force todo: Replace define/assert with define-symbol (def-symbol?)

clear-assumption-base

(define (fakederive p1 p2)
 (!force p1)
)

# Modus Tollens
(define mt 
 (method (premise1 premise2)
  (dmatch [premise1 premise2] 
   (
    [(if P Q)(not Q)] 
    (suppose-absurd P 
     (dseq 
      (!mp premise1 P)
      (!absurd Q (not Q))
))))))

# Law of the excluded middle
(define (excludedmiddle a)
 (!dn
  (suppose-absurd (not (or a (not a)))
   (!absurd
    (!either a
     (suppose-absurd a
      (!absurd 
       (!either a (not a))
       (not (or a (not a)))
    )))
    (not (or a (not a)))
))))

(domains Configuration Name Rule NodeSet Worldview ConvertedWorldview EdgeSet)

(datatype Transactor (Transactor Name Worldview))

(datatype Message (Message Name Worldview))

(datatype History 
 (InitialHistory) 
 (Stabilize History) 
 (Checkpoint History) 
 (Rollback History) 
)

(datatype Node (Node Name History))

(declare Noop Rule)
(declare Rcv1 Rule)
(declare Lose Rule)
(declare Invalidated (-> (History History) Boolean))
(declare Checkpointed (-> (History History) Boolean))
(declare Safe Boolean)
(declare ConfigurationSucceedsRule (-> (Configuration Configuration Rule)Boolean))
(declare ConfigurationSucceeds (-> (Configuration Configuration)Boolean))
(declare ConfigurationSucceeds* (-> (Configuration Configuration)Boolean))
(declare Independent (-> (Transactor) Boolean))
(declare Independent2 (-> (Transactor Configuration) Boolean))
(declare FollowsInvariant (-> (Configuration)Boolean))
(declare HistorySucceeds (-> (History History) Boolean))
(declare HistorySucceeds+ (-> (History History) Boolean))
(declare WorldviewUnion (-> (Worldview Worldview) Worldview))
(declare Simplify (-> (ConvertedWorldview) Worldview))
(declare GetHistory (-> (Worldview Name)History))
(declare DependsOn (-> (Worldview Name Name)Boolean))
(declare DependsOn* (-> (Worldview Name Name)Boolean))
(declare InName (-> (Worldview Name) Boolean))
(declare InHistoryC (-> (ConvertedWorldview Node) Boolean))
(declare DependsOnC (-> (ConvertedWorldview Node Node)Boolean))
(declare DependsOnC* (-> (ConvertedWorldview Node Node)Boolean))
(declare InNodeC (-> (ConvertedWorldview Node) Boolean))



(declare IsSafe (-> (Configuration)Boolean))

(declare InT (-> (Transactor Configuration)Boolean))

(declare InM (-> (Message Configuration)Boolean))

# A transactor ?Name with worldview ?Worldview is independent if its history
# is stable and all direct or indirect dependencies are also stable. 

(define (=H History1 History2)
 (or
  (= History1 History2)
  (= (Stabilize History1) History2)
  (= History1 (Stabilize History2))
))

# A transactor knows it is independent
(define DefIndependent
 (forall ?Name ?Worldview
  (iff
   (Independent (Transactor ?Name ?Worldview))
   (and
    (exists ?History
     (= (Stabilize ?History) (GetHistory ?Worldview ?Name))
    )
    (forall ?Dependency
     (if 
      (DependsOn* ?Worldview ?Name ?Dependency)
      (exists ?History
       (= (Stabilize ?History) (GetHistory ?Worldview ?Dependency))
)))))))

# A transactor is independent
(define DefIndependent2
 (forall ?Name ?Worldview ?Configuration
	 (iff
		 (Independent2 (Transactor ?Name ?Worldview) ?Configuration)
   (and
			 (exists ?History
				 (= (Stabilize ?History) (GetHistory ?Worldview ?Name))
				)
				(forall ?Dependency
				 (if
					 (DependsOn* ?Worldview ?Name ?Dependency)
						(exists ?ConfigurationOld ?WorldviewDependency
						 (and
								(=H (GetHistory ?Worldview ?Dependency) (GetHistory ?WorldviewDependency ?Dependency))
								(ConfigurationSucceeds* ?ConfigurationOld ?Configuration)
							 (InT (Transactor ?Dependency ?WorldviewDependency) ?ConfigurationOld)
								(Independent2 (Transactor ?Dependency ?WorldviewDependency) ?Configuration)
))))))))

(define Independent2CSSTool
 (forall ?Name ?Worldview ?Configuration ?Configuration2
  (if
		 (Independent2 (Transactor ?Name ?Worldview) ?Configuration)
		 (Independent2 (Transactor ?Name ?Worldview) ?Configuration2)
)))
			

# If a transactor knows it is independent, then it really is independent.
# (Transactors cannot know about information that will never be true, with the
# partial exception of knowing a transactor will roll back before it happens).
(define IndependentTool
 (forall ?Name ?Worldview ?Configuration
  (if
	  (and
	 	 (Independent (Transactor ?Name ?Worldview))
	 		(InT (Transactor ?Name ?Worldview) ?Configuration)
		 )
		 (Independent2 (Transactor ?Name ?Worldview) ?Configuration)
)))
		
(define DefHistorySucceeds
 (forall ?History1 ?History2
  (iff
   (HistorySucceeds ?History1 ?History2)
   (or
    (= (Stabilize ?History1) ?History2)
    (= (Checkpoint ?History1) ?History2)
    (= (Rollback ?History1) ?History2)    
))))

(define DefHistorySucceeds+
 (forall ?History1 ?History2
  (iff
   (HistorySucceeds+ ?History1 ?History2)
   (or
    (HistorySucceeds ?History1 ?History2)
    (exists ?SomeHistory
     (and
      (HistorySucceeds ?History1 ?SomeHistory)
      (HistorySucceeds+ ?SomeHistory ?History2)
))))))   

# Transitive dependency: a dep b dep* c implies a dep* c
# Also, a dep b implies a dep* b
(define DefDep*
 (forall ?x ?y ?z
  (iff
  (DependsOn* ?x ?y ?z)
   (or
    (DependsOn ?x ?y ?z)
    (exists ?a 
     (and
      (DependsOn ?x ?y ?a)
      (DependsOn* ?x ?a ?z)
))))))

# Once a transactor rolls back, it does not matter if it had been stable when it
# rolled back.
(define RollbackStable
 (forall ?History
  (= (Rollback ?History) (Stabilize (Rollback ?History)))
))

# If a history map in a union operation shows a transactor is stable, then that
# transactor's history was known to W1 or W2, but may have been volatile.
(define AlgorithmTool1
 (forall ?W1 ?W2 ?Name ?History
  (if
   (= (GetHistory (WorldviewUnion ?W1 ?W2) ?Name) (Stabilize ?History))
   (or
    (= (GetHistory ?W1 ?Name) ?History)
    (= (GetHistory ?W2 ?Name) ?History)
    (= (GetHistory ?W1 ?Name) (Stabilize ?History))
    (= (GetHistory ?W2 ?Name) (Stabilize ?History))
))))

(define (InSimplifyNodeAntecedent CW1 Name History)
 (and
  (InHistoryC CW1 (Node Name History))
  (forall ?History2
   (if 
    (InHistoryC CW1 (Node Name ?History2))
    (not (HistorySucceeds+ History ?History2))
  ))
  (forall ?Name2 ?History2
   (if
    (DependsOnC* CW1 (Node Name History) (Node ?Name2 ?History2))
    (not
     (exists ?History3
      (and
       (InHistoryC CW1 (Node ?Name2 ?History3))
       (Invalidated ?History2 ?History3) 
  )))))
  (forall ?Name2 ?History2
   (if
    (DependsOnC* CW1 (Node ?Name2 ?History2) (Node Name History))
    (or
     (exists ?SomeHistory (= History (Stabilize ?SomeHistory)))
     (not
      (exists ?History3
       (and
        (InHistoryC CW1 (Node ?Name2 ?History3))
        (Checkpointed ?History2 ?History3)
)))))))) 

#!Force: 
# Technically, one should instead state that there exists a ?CW2 for which the
# antecedent is true and for which (Simplify ?CW2) = (Simplify ?CW1).
(define InSimplifyNode
 (forall ?CW1 ?Name ?History
  (iff
   (= (GetHistory (Simplify ?CW1) ?Name) ?History)
   (InSimplifyNodeAntecedent ?CW1 ?Name ?History)
)))
              
#!Force: 
# Technically, one should instead state that there exists a ?CW2 for which the
# antecedent is true and for which (Simplify ?CW2) = (Simplify ?CW1).
(define InSimplifyEdge
 (forall ?CW1 ?Name ?History ?Name2 ?History2
  (iff
   (and
    (DependsOnC ?CW1 (Node ?Name ?History) (Node ?Name2 ?History2))
    (= (GetHistory (Simplify ?CW1) ?Name) ?History)
    (= (GetHistory (Simplify ?CW1) ?Name2) ?History2)
   )
   (DependsOn (Simplify ?CW1) ?Name ?Name2)
)))

# In 'Configuration', there is some transactor or message with 'Worldview'.
# That has name or destination 'Name'.
# 'Worldview' indicates that 'NameOld' is stable
(define
 (NameinConfigFollowsInvariantAntecedent Configuration Name NameOld Worldview)
 (and
  (or
   (InT (Transactor Name Worldview) Configuration)
   (InM (Message Name Worldview) Configuration)
  ) 
  (exists ?History (= (GetHistory Worldview NameOld) (Stabilize ?History)))
))

# 'Worldview' knows about 'NameOld' depending on 'Dependency' and
# 'WorldviewOld' and 'Worldview' share approximately the same history for it.
(define
 (NameOldKnowsADependencyLeft Worldview NameOld WorldviewOld Dependency)
 (and
  (DependsOn Worldview NameOld Dependency)
  (=H (GetHistory Worldview Dependency) (GetHistory WorldviewOld Dependency))
))

# !force Transactor doesn't actually need to know it is independent, so long as
# all of its dependencies (transitive or not) are stable.
# At some point before or during 'Configuration', 'Dependency' had some
# particular 'WorldviewDependency'.  Either [that dependency shares the about the
# same history with 'WorldviewOld' and that dependency indicates Dependency is
# independent] or ['WorldviewOld' indicates that Dependency has checkpointed after
# 'WorldviewDependency'.

(define
 (NameOldKnowsADependencyRight Configuration NameOld WorldviewOld Dependency)
 (exists ?WorldviewDependency ?ConfigurationDependency
  (and
   (ConfigurationSucceeds* ?ConfigurationDependency Configuration)
   (InT (Transactor Dependency ?WorldviewDependency) ?ConfigurationDependency)
   (or
    (and
     (=H (GetHistory ?WorldviewDependency Dependency) (GetHistory WorldviewOld Dependency))
     (Independent2 (Transactor Dependency ?WorldviewDependency) Configuration)
    )
    (Checkpointed (GetHistory WorldviewOld Dependency) (GetHistory ?WorldviewDependency Dependency))
))))

(define
 (NameOldKnowsADependency Configuration Worldview NameOld WorldviewOld Dependency)
 (or
  (NameOldKnowsADependencyLeft Worldview NameOld WorldviewOld Dependency)
  (NameOldKnowsADependencyRight Configuration NameOld WorldviewOld Dependency)
))

# There exists some configuration older than 'Configuration' for which 'NameOld' knows it is stable
# and 'NameOld' has the history 'Worldview' thinks it has.  All dependencies of 'NameOld'
# Follow NameOldKnowsADependency
(define
 (NameinConfigFollowsInvariantConsequent Configuration NameOld Worldview)
 (exists ?WorldviewOld ?ConfigurationOld
  (and
   (ConfigurationSucceeds* ?ConfigurationOld Configuration)
   (InT (Transactor NameOld ?WorldviewOld) ?ConfigurationOld)
   (= (GetHistory ?WorldviewOld NameOld) (GetHistory Worldview NameOld))
   (forall ?Dependency
    (if
     (DependsOn ?WorldviewOld NameOld ?Dependency)
     (NameOldKnowsADependency Configuration Worldview NameOld ?WorldviewOld ?Dependency)
)))))


(define DefFollowsInvariant
 (forall ?Configuration
  (iff
   (FollowsInvariant ?Configuration)
   (forall ?Name ?NameOld ?Worldview
    (if
     (NameinConfigFollowsInvariantAntecedent ?Configuration ?Name ?NameOld ?Worldview)
     (NameinConfigFollowsInvariantConsequent ?Configuration ?NameOld ?Worldview)
)))))
 
(define DefSimplify
 (forall ?CW1 ?Name1 ?History1 ?History2
  (if
   (and
    (InHistoryC ?CW1 (Node ?Name1 ?History1))
    (InHistoryC ?CW1 (Node ?Name1 ?History2))
    (HistorySucceeds+ ?History1 ?History2)
   )
   (exists ?CW
    (and
     (= (Simplify ?CW) (Simplify ?CW1))
     (forall ?Node (iff (InNodeC ?CW ?Node) (InNodeC ?CW1 ?Node)))
     (if 
      (= (Stabilize ?History1) ?History2)
      (and
       (forall ?Node 
        (if
         (and
          (InHistoryC ?CW1 ?Node)
          (not (= ?Node (Node ?Name1 ?History1)))
         )
         (InHistoryC ?CW ?Node)
       ))         
       (forall ?NodeA ?NodeB
        (and
         (if
          (and
           (DependsOnC ?CW1 ?NodeA ?NodeB)
           (not (= ?NodeA (Node ?Name1 ?History1)))
           (not (= ?NodeB (Node ?Name1 ?History1)))
          )
          (DependsOnC ?CW ?NodeA ?NodeB)
         )
         (if
          (and
           (DependsOnC ?CW1 ?NodeA ?NodeB)
           (= ?NodeA (Node ?Name1 ?History1))
          )
          (DependsOnC ?CW (Node ?Name1 ?History2) ?NodeB)
         )
         (if
          (and
           (DependsOnC ?CW1 ?NodeA ?NodeB)
           (= ?NodeB (Node ?Name1 ?History1))
          )
          (DependsOnC ?CW ?NodeA (Node ?Name1 ?History2))
     )))))
     
     (if
      (Invalidated ?History1 ?History2)
      (and
       (forall ?Node 
        (if
         (and
          (InHistoryC ?CW1 ?Node)
          (not (= ?Node (Node ?Name1 ?History1)))
         )
         (InHistoryC ?CW ?Node)
       ))         
       (forall ?Name ?History
        (if
         (DependsOnC ?CW1 (Node ?Name ?History) (Node ?Name1 ?History1))
         (InHistoryC ?CW (Node ?Name (Rollback ?History)))
       ))
       (forall ?NodeA ?NodeB
        (and
         (if
          (and
           (DependsOnC ?CW1 ?NodeA ?NodeB)
           (not (= ?NodeA (Node ?Name1 ?History1)))
           (not (= ?NodeB (Node ?Name1 ?History1)))
          )
          (DependsOnC ?CW ?NodeA ?NodeB)
     )))))
           
     (if
      (Checkpointed ?History1 ?History2)
      (and
       (forall ?Node 
        (if
         (and
          (InHistoryC ?CW1 ?Node)
          (not (= ?Node (Node ?Name1 ?History1)))
         )
         (InHistoryC ?CW ?Node)
       ))         
       (forall ?Name ?History
        (if
         (DependsOnC* ?CW1 (Node ?Name1 ?History1) (Node ?Name ?History))
         (InHistoryC ?CW (Node ?Name (Stabilize ?History)))
       ))
       (forall ?NodeA ?NodeB
        (and
         (if
          (and
           (DependsOnC ?CW1 ?NodeA ?NodeB)
           (not (= ?NodeA (Node ?Name1 ?History1)))
           (not (= ?NodeB (Node ?Name1 ?History1)))
          )
          (DependsOnC ?CW ?NodeA ?NodeB)
))))))))))
 
(define DefWorldviewUnion
 (forall ?W1 ?W2
  (exists ?ConvertedWorldView
   (and
    (forall ?NameA ?HistoryA
     (iff
      (or
       (= (GetHistory ?W1 ?NameA) ?HistoryA)
       (= (GetHistory ?W2 ?NameA) ?HistoryA)       
      )
      (InHistoryC ?ConvertedWorldView (Node ?NameA ?HistoryA))
    ))

    (forall ?NameA ?HistoryA ?NameB ?HistoryB
     (iff
      (or
       (and
        (= (GetHistory ?W1 ?NameA) ?HistoryA)
        (= (GetHistory ?W1 ?NameB) ?HistoryB)
        (DependsOn ?W1 ?NameA ?NameB)
       )
       (and
        (= (GetHistory ?W2 ?NameA) ?HistoryA)
        (= (GetHistory ?W2 ?NameB) ?HistoryB)
        (DependsOn ?W2 ?NameA ?NameB)
      ))
      (DependsOnC ?ConvertedWorldView (Node ?NameA ?HistoryA) (Node ?NameB ?HistoryB))
    ))

    (forall ?NameA ?HistoryA
     (iff
      (or
       (and
        (= (GetHistory ?W1 ?NameA) ?HistoryA)
        (InName ?W1 ?NameA)
       )
       (and
        (= (GetHistory ?W2 ?NameA) ?HistoryA)
        (InName ?W2 ?NameA)
       )
      )
      (InNodeC ?ConvertedWorldView (Node ?NameA ?HistoryA))
    ))
    (= (WorldviewUnion ?W1 ?W2) (Simplify ?ConvertedWorldView))
))))

# Given two history maps, ?H1 is invalidated by ?H2 if ?H2 is a rolledback ?H1
(define DefInvalidate
 (forall ?H1 ?H2
  (iff
   (Invalidated ?H1 ?H2)
   (or
    (HistorySucceeds+ (Rollback ?H1) ?H2) 
    (HistorySucceeds+ (Rollback (Stabilize ?H1)) ?H2) 
))))

(define DefCheckpointed
 (forall ?H1 ?H2
  (iff
   (Checkpointed ?H1 ?H2)
   (or
    (HistorySucceeds+ (Checkpoint ?H1) ?H2) 
    (HistorySucceeds+ (Checkpoint (Stabilize ?H1)) ?H2) 
))))
 
# Transitive dependency: a dep b dep c implies a dep* c
(define DefDep*
 (forall ?x ?y ?z
  (iff
  (DependsOn* ?x ?y ?z)
   (or
   (DependsOn ?x ?y ?z)
    (exists ?a 
     (and
      (DependsOn ?x ?y ?a)
      (DependsOn* ?x ?a ?z)
))))))

# Transitive dependency: a dep b dep c implies a dep* c
(define DefDepC*
 (forall ?x ?y ?z
  (iff
  (DependsOnC* ?x ?y ?z)
   (or
    (DependsOnC ?x ?y ?z)
    (exists ?a 
     (and
      (DependsOnC ?x ?y ?a)
      (DependsOnC* ?x ?a ?z)
))))))


#!force y should be an existential quantifier, not a universal quantifier (like DefDep*)
# A ->* B if B either comes after A or B is A
(define DefCSS*
 (forall ?x ?z
  (iff (ConfigurationSucceeds* ?x ?z)
   (or
    (= ?x ?z)
    (exists ?y
				 (and 
      (ConfigurationSucceeds ?x ?y)
      (ConfigurationSucceeds* ?y ?z)
))))))

# Consider execution trace to be a tree.
(define DefInjection
 (forall ?x ?y ?z
  (if 
   (and
    (ConfigurationSucceeds ?x ?y)
    (ConfigurationSucceeds ?z ?y)
   )
   (= ?x ?z)
)))

# Only one instance of a transactor name can run at once.
(define DefUniqueness
 (forall ?a ?b ?c ?d
  (if
   (and
    (InT (Transactor ?a ?b)?d)
    (InT (Transactor ?a ?c)?d)
   )
   (and
    (= ?b ?c)
))))

(assert DefIndependent DefIndependent2 DefHistorySucceeds DefHistorySucceeds+ DefDep*
RollbackStable InSimplifyNode InSimplifyEdge DefFollowsInvariant
DefSimplify DefWorldviewUnion DefInvalidate DefCheckpointed DefDep* DefDepC*
DefCSS* DefInjection DefUniqueness AlgorithmTool1 IndependentTool Independent2CSSTool)


# This definition is used below in order to avoid redundancy.
(define
 (StableAlreadyKnownProof assumptionchoice worldviewchoice Worldview assumption MessageDestination DestinationWorldview NameOld SomeHistory MessageWorldview NewConfiguration OldConfiguration)
 (assume-let (assumptionStable2 (= (GetHistory worldviewchoice NameOld) (Stabilize SomeHistory)))
  (dlet
   (
    (Reiterate (!claim (InT (Transactor MessageDestination (WorldviewUnion DestinationWorldview MessageWorldview)) NewConfiguration)))
    (OldConfigFollowsInvariant (!mp (!left-iff (!uspec DefFollowsInvariant OldConfiguration)) (FollowsInvariant OldConfiguration)))
    (SpecificChoice (!uspec* OldConfigFollowsInvariant [MessageDestination NameOld worldviewchoice]))
    (ChoiceMP
     (
      (NameinConfigFollowsInvariantConsequent OldConfiguration NameOld worldviewchoice)
      BY
      (!mp
       SpecificChoice 
       (!both 
        assumptionchoice
        (!egen (exists ?History (= (GetHistory worldviewchoice NameOld) (Stabilize ?History))) SomeHistory)
    ))))
   )
   (pick-witnesses (WitWorldviewOld WitConfigurationOld) ChoiceMP witpremise
    (dlet
     (
      (OldConfigThenNewConfig ((ConfigurationSucceeds OldConfiguration NewConfiguration) BY (!left-and (!right-and (!right-and (!right-and assumption))))))
      (WitConfigOldthenOldConfig ((ConfigurationSucceeds* WitConfigurationOld OldConfiguration) BY (!left-and witpremise)))
      (Goal1 (!derive (ConfigurationSucceeds* WitConfigurationOld NewConfiguration) [OldConfigThenNewConfig WitConfigOldthenOldConfig DefCSS*]))
      (Goal2 ((InT (Transactor NameOld WitWorldviewOld) WitConfigurationOld) BY (!left-and (!right-and witpremise))))
      (Goal3a ((= (GetHistory WitWorldviewOld NameOld) (GetHistory worldviewchoice NameOld)) BY (!left-and (!right-and (!right-and witpremise)))))
      (Goal3
       # Transitivity of =
       (!derive
        (= (GetHistory WitWorldviewOld NameOld) (GetHistory Worldview NameOld))
        [
         (= (GetHistory WitWorldviewOld NameOld) (GetHistory worldviewchoice NameOld))
         (= (GetHistory worldviewchoice NameOld) (Stabilize SomeHistory))
         (= (GetHistory Worldview NameOld) (Stabilize SomeHistory))
        ]
      ))
      (Goal4a
       (!derive
        (forall ?Dependency
         (if
          (DependsOn WitWorldviewOld NameOld ?Dependency)
          (NameOldKnowsADependency OldConfiguration worldviewchoice NameOld WitWorldviewOld ?Dependency)
        ))
        [witpremise]
      ))
      (Goal4 
       (pick-any Dependency
        (pick-witness ConvertedWorldView (!uspec* DefWorldviewUnion [DestinationWorldview MessageWorldview]) UnionDef
         (assume (DependsOn WitWorldviewOld NameOld Dependency)
          (dlet
           (
            (P1
             (
              (NameOldKnowsADependency OldConfiguration worldviewchoice NameOld WitWorldviewOld Dependency)
              BY
              (!mp (!uspec Goal4a Dependency) (DependsOn WitWorldviewOld NameOld Dependency))
            ))
            (ReitUnion (!claim (= Worldview (WorldviewUnion DestinationWorldview MessageWorldview))))
            (ReitHist1 (!claim (= (GetHistory worldviewchoice NameOld) (Stabilize SomeHistory))))
            (ReitHist2 (!claim (= (GetHistory Worldview NameOld) (Stabilize SomeHistory))))
            (UnionDef1 ((= (WorldviewUnion DestinationWorldview MessageWorldview) (Simplify ConvertedWorldView)) BY (!right-and (!right-and (!right-and UnionDef)))))
            #Applications of step 1 of union algorithm
            (UnionIn1 (!derive (InHistoryC ConvertedWorldView (Node NameOld (Stabilize SomeHistory))) [UnionDef ReitHist1]))
            #Reverse application of union algorithm
            (UnionIn2 (!derive (= (GetHistory (Simplify ConvertedWorldView) NameOld) (Stabilize SomeHistory)) [ReitUnion ReitHist2 UnionDef1]))
            (UnionIn3 (!mp (!left-iff (!uspec* InSimplifyNode [ConvertedWorldView NameOld (Stabilize SomeHistory)])) UnionIn2))
            (UnionIn4 (!derive (InHistoryC ConvertedWorldView (Node Dependency (GetHistory worldviewchoice Dependency))) [UnionDef]))
            (LeftSide
             (assume-let
              (dependassump (NameOldKnowsADependencyLeft worldviewchoice NameOld WitWorldviewOld Dependency))
              (dlet
               (
                (UnionInM1
                 (!derive
                  (DependsOnC ConvertedWorldView (Node NameOld (Stabilize SomeHistory)) (Node Dependency (GetHistory worldviewchoice Dependency)))
                  [ReitHist1 dependassump UnionDef]
                ))
                (UnionInM2
                 (!derive
                  (or
                   (= (GetHistory (Simplify ConvertedWorldView) Dependency) (GetHistory worldviewchoice Dependency))
                   (not (InSimplifyNodeAntecedent ConvertedWorldView Dependency (GetHistory worldviewchoice Dependency)))
                  )
                  [InSimplifyNode]
                ))
                (UnionInAntecedent1 (!claim UnionIn4))
                (UnionInAntecedent2
                 (assume
                  (exists ?History2
                   (and
                    (InHistoryC ConvertedWorldView (Node Dependency ?History2))
                    (HistorySucceeds+ (GetHistory worldviewchoice Dependency) ?History2)
                  ))
                 # If Dependency rolled back, NameOld would not have been stable in Worldview.  If it checkpointed,
                 # It is independent and NameOldKnowsADependencyRight is true.
                 # Finally, if none of these apply, it must have become stable because the other operand of the union knew
                 # It was stable, in which case apply all of this to the other operand (and this specific case will not
                 # apply circularly, since this version is not stable.
                  (!force (NameOldKnowsADependency NewConfiguration Worldview NameOld WitWorldviewOld Dependency)) 
                ))
                (UnionInAntecedent3
                 (suppose-absurd-let
                  (absurdity
                   (not (forall ?Name2 ?History2
                     (if
                      (DependsOnC* ConvertedWorldView (Node Dependency (GetHistory worldviewchoice Dependency)) (Node ?Name2 ?History2))
                      (not
                       (exists ?History3
                        (and
                         (InHistoryC ConvertedWorldView (Node ?Name2 ?History3))
                         (Invalidated ?History2 ?History3) 
                  )))))))
                  # NameOld can't depend on something that rolled back, since the version in the convertedworldview did not rollback.
                  (!derive false [absurdity InSimplifyNode UnionIn2 DefDepC* UnionInM1])
                ))
                (UnionInAntecedent4
                 (assume
                  (exists ?Name2 ?History2
                   (and 
                    (DependsOnC* ConvertedWorldView (Node ?Name2 ?History2) (Node Dependency (GetHistory worldviewchoice Dependency)))
                    (and
                     (not (exists ?SomeHistory (= (GetHistory worldviewchoice Dependency) (Stabilize ?SomeHistory))))
                     (exists ?History3
                      (and
                       (InHistoryC ConvertedWorldView (Node ?Name2 ?History3))
                       (Checkpointed ?History2 ?History3)
                  )))))
                  # Given that ?Name2 depends on this version of Dependency and has checkpointed, this version of Dependency must be independent (checkpoint happened before message was received, at which time safety invariant was being followed).
                  (!force (NameOldKnowsADependencyRight NewConfiguration NameOld WitWorldviewOld Dependency))                                      )))
               (!derive
                (NameOldKnowsADependency NewConfiguration Worldview NameOld WitWorldviewOld Dependency)
                [UnionIn2 UnionInM1 UnionInM2 InSimplifyEdge UnionInAntecedent1 UnionInAntecedent2 UnionInAntecedent3 UnionInAntecedent4]
               )
            )))
            
												(RightSide
             (assume
              (NameOldKnowsADependencyRight OldConfiguration NameOld WitWorldviewOld Dependency)
              # Uses transitivity of time progression
              (!derive
               (NameOldKnowsADependency NewConfiguration Worldview NameOld WitWorldviewOld Dependency)
               [
                (NameOldKnowsADependencyRight OldConfiguration NameOld WitWorldviewOld Dependency)
                DefCSS*
                (ConfigurationSucceeds OldConfiguration NewConfiguration)
                Independent2CSSTool
               ]
           ))))
           (!cd P1 LeftSide RightSide)
         ))
     ))))
     # Many uses of !both
     (!derive (NameinConfigFollowsInvariantConsequent NewConfiguration NameOld Worldview)[Goal1 Goal2 Goal3 Goal4])
)))))



(define LemmaOriginOfStableHistory
 (pick-any W1 W2 Name SomeHistory
  (assume-let
   (assumption
    (and
     (not (= (GetHistory W1 Name) (Stabilize SomeHistory)))
     (not (= (GetHistory W2 Name) (Stabilize SomeHistory)))
     (= (GetHistory (WorldviewUnion W1 W2) Name) (Stabilize SomeHistory))
   ))
   (dlet
    (
     (Simple 
      (!mp
       (!uspec* AlgorithmTool1 [W1 W2 Name SomeHistory]) 
       (!right-and (!right-and assumption))
    )))
    (!derive
     (or (= (GetHistory W1 Name) SomeHistory) (= (GetHistory W2 Name) SomeHistory))
     [Simple assumption]
)))))
 
    
# A worldview following the safety invariant will not violate it in the future
# if the worldview is unchanged.
(define
 (LemmaImmutablePast Name Worldview OldConfiguration NewConfiguration NameOld)
 (assume-let
# Some message or transactor is in two consecutive Configurations.  The
# Corresponding 'Worldview' indicates that 'NameOld' is stable.
  (assumption3
   (and
    (or
     (and
      (InM (Message Name Worldview) OldConfiguration)
      (InM (Message Name Worldview) NewConfiguration)
     )
     (and
      (InT (Transactor Name Worldview) OldConfiguration)
      (InT (Transactor Name Worldview) NewConfiguration)
    ))
    (FollowsInvariant OldConfiguration)
    (exists ?History (= (GetHistory Worldview NameOld) (Stabilize ?History)))
    (ConfigurationSucceeds OldConfiguration NewConfiguration)
  ))
  (dlet
   (
    # This instantiates the safety invariant definition with OldConfiguration.  Note that technically (FollowsInvariant OldConfiguration)
				# Should be obtained from assumption3, but it is currently in the assumption base any time the lemma is called
				(OldConfigFollowsInvariant (!mp (!left-iff (!uspec DefFollowsInvariant OldConfiguration)) (FollowsInvariant OldConfiguration)))
    (NoNewMessages (!left-and assumption3))
    (OldVersionOfMessageAlsoKnewHistoryWasStable
     # Break apart disjunction and pull out individual conjuncts.
     (!derive
      (or
       (InT (Transactor Name Worldview) OldConfiguration)
       (InM (Message Name Worldview) OldConfiguration)
      )
      [NoNewMessages]
    ))
    # This makes the invariant application even more specific, applying it a specific
				# transactor known to the worldview.  That transactor is actually given by
				# the caller of the lemma, but will usually be a universal quantifier.
				(MatchingTransactorExists
     (
      (NameinConfigFollowsInvariantConsequent OldConfiguration NameOld Worldview)
      BY
      (!mp
       (!uspec* OldConfigFollowsInvariant [Name NameOld Worldview])
       (!both OldVersionOfMessageAlsoKnewHistoryWasStable (!left-and (!right-and (!right-and assumption3))))
   ))))

   # The witnesses are the specific worldview and configuration of the stable transactor.
   (pick-witnesses (WitWorldviewOld WitConfigurationOld) MatchingTransactorExists witpremise
    (dlet
     (
      (OldConfigThenNewConfig ((ConfigurationSucceeds OldConfiguration NewConfiguration) BY (!right-and (!right-and (!right-and assumption3)))))
      (WitConfigOldthenOldConfig ((ConfigurationSucceeds* WitConfigurationOld OldConfiguration) BY (!left-and witpremise)))
      (WitConfigOldthenNewConfig (!derive (ConfigurationSucceeds* WitConfigurationOld NewConfiguration) [OldConfigThenNewConfig WitConfigOldthenOldConfig DefCSS*]))
      (P2 ((InT (Transactor NameOld WitWorldviewOld) WitConfigurationOld) BY (!left-and (!right-and witpremise))))
      (P3 ((= (GetHistory WitWorldviewOld NameOld) (GetHistory Worldview NameOld)) BY (!left-and (!right-and (!right-and witpremise)))))
      (P4a (!right-and (!right-and (!right-and witpremise))))
      #Using DefCSS* directly for P4 is slow.
      (P4b (!derive (forall ?Configuration1 ?Configuration2 (iff 
          (ConfigurationSucceeds* ?Configuration1 NewConfiguration)
          (or
           (and (ConfigurationSucceeds ?Configuration1 ?Configuration2) (ConfigurationSucceeds* ?Configuration2 NewConfiguration))
           (= ?Configuration1 NewConfiguration)
        ))) [DefCSS*]
      ))
      (P4
      #Use transitivity of ConfigurationSucceeds* to adjust witness to use newer configuration 
       (!derive
        (forall ?Dependency
         (if
          (DependsOn WitWorldviewOld NameOld ?Dependency)
          (NameOldKnowsADependency NewConfiguration Worldview NameOld WitWorldviewOld ?Dependency)
        ))
        [Independent2CSSTool P4a P4b OldConfigThenNewConfig]
     )))              
     #Use !both and !egen multiple times.  The witness was (NameinConfigFollowsInvariantConsequent OldConfiguration NameOld Worldview)
     (!derive
      (NameinConfigFollowsInvariantConsequent NewConfiguration NameOld Worldview)
      [WitConfigOldthenNewConfig P2 P3 P4]
))))))


# Proof of stabilization following the safety invariant.
(pick-any OldConfiguration NewConfiguration Name Worldview1 Worldview2
 (assume 
  (FollowsInvariant OldConfiguration)
  (assume-let
   (assumption 
    (and
     (InT (Transactor Name Worldview1) OldConfiguration)
     (InT (Transactor Name Worldview2) NewConfiguration)
					(exists ?History 
					 (and
						 (= (GetHistory Worldview1 Name) ?History)
						 (= (GetHistory Worldview2 Name) (Stabilize ?History))
					))
					(forall ?Name2
					 (if
						 (not (= ?Name2 Name))
							(= (GetHistory Worldview1 ?Name2) (GetHistory Worldview2 ?Name2))
					))
					(ConfigurationSucceeds OldConfiguration NewConfiguration)
     (forall ?UnchangedMessage ?UnchangedWorldview
      (iff 
       (InM (Message ?UnchangedMessage ?UnchangedWorldview) NewConfiguration)
       (InM (Message ?UnchangedMessage ?UnchangedWorldview) OldConfiguration)
     ))
     (forall ?NameAlt ?Worldview
						(if
							(not (= Name ?NameAlt))
							(iff
								(InT (Transactor ?NameAlt ?Worldview) OldConfiguration)
								(InT (Transactor ?NameAlt ?Worldview) NewConfiguration)
   )))))
			(!mp
			 (!right-iff (!uspec DefFollowsInvariant NewConfiguration))
				(pick-any ArbName NameOld Worldview
				 (assume-let
					 (assumption2
						 (and
							 (or
								 (InT (Transactor ArbName Worldview) NewConfiguration)
									(InM (Message ArbName Worldview) NewConfiguration)
								)
								(exists ?History (= (GetHistory Worldview NameOld) (Stabilize ?History)))
						))
						(dlet
						 (
							 (IsNewStabilizeorNot (!excludedmiddle (or (not (= ArbName Name)) (InM (Message ArbName Worldview) OldConfiguration))))
								(RightCD
								 (assume-let (assumptionalt (not (or (not (= ArbName Name)) (InM (Message ArbName Worldview) OldConfiguration))))
									 (dlet
										 (
				        (OldConfigFollowsInvariant (!mp (!left-iff (!uspec DefFollowsInvariant OldConfiguration)) (FollowsInvariant OldConfiguration)))
												(Test
												 (!derive
													 (InT (Transactor Name Worldview) NewConfiguration)
														[assumptionalt assumption assumption2]
												))
#												(OldCons
#													(
#														(NameinConfigFollowsInvariantConsequent OldConfiguration NameOld Worldview1) BY
#														(!mp
#														(!uspec* OldConfigFollowsInvariant [Name NameOld Worldview1])
#														(!both
#																(!either
#																	(!left-and assumption)
#																	(InM (Message Name Worldview1) OldConfiguration)
#																)
#																(!right-and assumption2)
#											 ))))
											)
										 (!force (NameinConfigFollowsInvariantConsequent NewConfiguration NameOld Worldview))
								  )
								))
								(LeftCD
								 (assume (or (not (= ArbName Name)) (InM (Message ArbName Worldview) OldConfiguration))
										(!mp
											(!LemmaImmutablePast ArbName Worldview OldConfiguration NewConfiguration NameOld)  
											(!derive
												(and
													(or
														(and
															(InM (Message ArbName Worldview) OldConfiguration)
															(InM (Message ArbName Worldview) NewConfiguration)
														)
														(and
															(InT (Transactor ArbName Worldview) OldConfiguration)
															(InT (Transactor ArbName Worldview) NewConfiguration)
													))
													(FollowsInvariant OldConfiguration)
													(exists ?History (= (GetHistory Worldview NameOld) (Stabilize ?History)))
													(ConfigurationSucceeds OldConfiguration NewConfiguration)
												)
												[(or (not (= ArbName Name)) (InM (Message ArbName Worldview) OldConfiguration)) assumption assumption2 (FollowsInvariant OldConfiguration)]
							)))))
						 (!cd IsNewStabilizeorNot LeftCD RightCD)
)))))))


(pick-any OldConfiguration NewConfiguration MessageDestination MessageWorldview DestinationWorldview
 (assume 
  (FollowsInvariant OldConfiguration)
  (assume-let
   (assumption 
    (and
     (InM (Message MessageDestination MessageWorldview) OldConfiguration)
     (InT (Transactor MessageDestination DestinationWorldview) OldConfiguration)
     (InT (Transactor MessageDestination (WorldviewUnion DestinationWorldview MessageWorldview)) NewConfiguration)
     (ConfigurationSucceeds OldConfiguration NewConfiguration)
     (forall ?UnchangedMessage ?UnchangedWorldview
      (if 
       (InM (Message ?UnchangedMessage ?UnchangedWorldview) NewConfiguration)
       (InM (Message ?UnchangedMessage ?UnchangedWorldview) OldConfiguration)
     ))
     (forall ?Transactor ?Worldview
      (and
       (if
        (not (= ?Transactor MessageDestination))
        (iff
         (InT (Transactor ?Transactor ?Worldview) NewConfiguration)
         (InT (Transactor ?Transactor ?Worldview) OldConfiguration)
   ))))))
   (!mp 
    (!right-iff (!uspec DefFollowsInvariant NewConfiguration))
    (pick-any Name NameOld Worldview
     (assume-let
      (assumption2
       (and
        (or
         (InT (Transactor Name Worldview) NewConfiguration)
         (InM (Message Name Worldview) NewConfiguration)
        ) 
        (exists ?History (= (GetHistory Worldview NameOld) (Stabilize ?History)))
      ))
      (dlet
       (
        (MostTransUnchanged (!right-and (!right-and (!right-and (!right-and (!right-and assumption))))))
        (Disjunction (!left-and assumption2))
        (LeftCD
         (assume (InT (Transactor Name Worldview) NewConfiguration)
          (dlet
           (
            (TransactorisDestinationorNot (!excludedmiddle (= Name MessageDestination)))
            (IsDest
             (assume
              (= Name MessageDestination)
              (dlet
               (
                (ThirdAssumptionConjunct (!left-and (!right-and (!right-and assumption))))
                (NameSharesDestinationWorldview
                 (!derive
                  (= Worldview (WorldviewUnion DestinationWorldview MessageWorldview))
                  [(InT (Transactor Name Worldview) NewConfiguration) DefUniqueness (= Name MessageDestination) ThirdAssumptionConjunct]
                ))                
               )
               (pick-witness SomeHistory
                (!right-and assumption2) 
                (dlet
                 (
                  (TheWitness (!claim (= (GetHistory Worldview NameOld) (Stabilize SomeHistory))))
                  (StableOrigin (!uspec* LemmaOriginOfStableHistory [DestinationWorldview MessageWorldview NameOld SomeHistory]))
                  (MyName
                   (!derive
                    (or
                     (or
                      (= (GetHistory DestinationWorldview NameOld) (Stabilize SomeHistory))
                      (= (GetHistory MessageWorldview NameOld) (Stabilize SomeHistory))
                     )
                     (and
                      (not (= (GetHistory DestinationWorldview NameOld) (Stabilize SomeHistory)))
                      (not (= (GetHistory MessageWorldview NameOld) (Stabilize SomeHistory)))
                      (or
                       (= (GetHistory DestinationWorldview NameOld) SomeHistory)
                       (= (GetHistory MessageWorldview NameOld) SomeHistory)
                    )))
                    [StableOrigin TheWitness NameSharesDestinationWorldview]
                  ))
                  (StableAlreadyKnown
                   (assume-let
                    (assumptionStable
                     (or
                      (= (GetHistory DestinationWorldview NameOld) (Stabilize SomeHistory))
                      (= (GetHistory MessageWorldview NameOld) (Stabilize SomeHistory))
                    ))
                    (dlet
                     (
                      (LeftStable 
                       (!StableAlreadyKnownProof 
                        (!either
                         (!left-and (!right-and assumption))
                         (InM (Message MessageDestination DestinationWorldview) OldConfiguration)
                        )
                        DestinationWorldview Worldview assumption MessageDestination DestinationWorldview NameOld SomeHistory MessageWorldview NewConfiguration OldConfiguration)
                      )
                      (RightStable
                       (!StableAlreadyKnownProof
                        (!either
                         (InT (Transactor MessageDestination MessageWorldview) OldConfiguration)
                         (!left-and assumption)
                        )
                        MessageWorldview Worldview assumption MessageDestination DestinationWorldview NameOld SomeHistory MessageWorldview NewConfiguration OldConfiguration)
                      )
                     )
                     (!cd assumptionStable LeftStable RightStable)
                  )))
                  (StableNotAlreadyKnown
                   (assume-let
                    (assumptionVolatile
                     (and
                      (not (= (GetHistory DestinationWorldview NameOld) (Stabilize SomeHistory)))
                      (not (= (GetHistory MessageWorldview NameOld) (Stabilize SomeHistory)))
                      (or
                       (= (GetHistory DestinationWorldview NameOld) SomeHistory)
                       (= (GetHistory MessageWorldview NameOld) SomeHistory)
                    )))
                    # Discovering a transactor is stable after a worldviewunion means something that previously
																				# Depended on it checkpointed, thus anything it became independent and knowing about it is not required.
																				(!force (NameinConfigFollowsInvariantConsequent NewConfiguration NameOld Worldview))
                 )))
                 (!cd MyName StableAlreadyKnown StableNotAlreadyKnown)
            )))))
            (NotDest
             (assume
              (not (= Name MessageDestination))
              (!mp
               (!LemmaImmutablePast Name Worldview OldConfiguration NewConfiguration NameOld)  
               (!derive
                (and
                 (or
                  (and
                   (InM (Message Name Worldview) OldConfiguration)
                   (InM (Message Name Worldview) NewConfiguration)
                  )
                  (and
                   (InT (Transactor Name Worldview) OldConfiguration)
                   (InT (Transactor Name Worldview) NewConfiguration)
                 ))
                 (FollowsInvariant OldConfiguration)
                 (exists ?History (= (GetHistory Worldview NameOld) (Stabilize ?History)))
                 (ConfigurationSucceeds OldConfiguration NewConfiguration)
                )
                [(not (= Name MessageDestination)) assumption assumption2 (FollowsInvariant OldConfiguration)]
           )))))
           (!cd TransactorisDestinationorNot IsDest NotDest)
        )))
        (RightCD
         (assume 
          (InM (Message Name Worldview) NewConfiguration)
          (!mp
           (!LemmaImmutablePast Name Worldview OldConfiguration NewConfiguration NameOld)  
           #Just simple application of !both, !either, and !left-and/!right-and
           (!derive
            (and
             (or
              (and
               (InM (Message Name Worldview) OldConfiguration)
               (InM (Message Name Worldview) NewConfiguration)
              )
              (and
               (InT (Transactor Name Worldview) OldConfiguration)
               (InT (Transactor Name Worldview) NewConfiguration)
              )
             )
             (FollowsInvariant OldConfiguration)
             (exists ?History (= (GetHistory Worldview NameOld) (Stabilize ?History)))
             (ConfigurationSucceeds OldConfiguration NewConfiguration)
            )
            [(InM (Message Name Worldview) NewConfiguration) assumption assumption2 (FollowsInvariant OldConfiguration)]
       )))))
       (!cd Disjunction LeftCD RightCD)
)))))))

# (declare X Transactor)
# (assume 
#  (forall ?X (Independent ?X))
#  (dseq
#   (!uspec (forall ?X (Independent ?X)) X)
#   (!egen (exists ?X (Independent ?X)) X)
# ))