fact_3

fact_3.v

Theorem fact_3 :
  fact_in_coq / update empty_state X 3
              || (update
                    (update
                       (update
                          (update
                             (update
                                (update
                                   (update
                                      (update
                                         (update empty_state X 3)
                                         Z 3)
                                      Y 1)
                                   Y 3)
                                Z 2)
                             Y 6)
                          Z 1)
                       Y 6)
                    Z 0).
Proof.
  apply E_Seq with (update (update empty_state X 3) Z 3).
  Case "Z assignment command".
(*
  | E_Ass : forall (st : state) (a1 : aexp) (n : nat) (x : id),
            aeval st a1 = n -> (x ::= a1) / st || update st x n

    aeval (update empty_state X 3) X = 3 -> (* 3 = 3; st = update empty_state X 3 *)
    Z ::= AId X / update empty_state X 3 || update (update empty_state X 3) Z 3
*)
   apply E_Ass. reflexivity.
 apply E_Seq with (update (update (update empty_state X 3) Z 3) Y 1).
 Case "Y assignment command".
   apply E_Ass. reflexivity.
 Case "while command".
   apply E_WhileLoop with (update (update (update (update (update empty_state X 3) Z 3) Y 1) Y 3) Z 2).
   reflexivity.
   SCase "sequence command".
     apply E_Seq with (update (update (update (update empty_state X 3) Z 3) Y 1) Y 3).
     SSCase "Y assignment command".
       apply E_Ass. reflexivity.
     SSCase "Z assignment command".
       apply E_Ass. reflexivity.
   SCase "while command".
     apply E_WhileLoop with (update (update (update (update (update (update (update empty_state X 3) Z 3) Y 1) Y 3) Z 2) Y 6) Z 1).
     reflexivity.
     SSCase "sequence command".
       apply E_Seq with (update (update (update (update (update (update empty_state X 3) Z 3) Y 1) Y 3) Z 2) Y 6).
       SSSCase "Y assignment command".
         apply E_Ass. reflexivity.
       SSSCase "Z assignment command".
         apply E_Ass. reflexivity.
     SSCase "while command".
       apply E_WhileLoop with (update (update (update (update (update (update (update (update (update empty_state X 3) Z 3) Y 1) Y 3) Z 2) Y 6) Z 1) Y 6) Z 0).
       reflexivity.
       SSSCase "sequence command".
         apply E_Seq with (update (update (update (update (update (update (update (update empty_state X 3) Z 3) Y 1) Y 3) Z 2) Y 6) Z 1) Y 6).
         SSSSCase "Y assignment command".
           apply E_Ass. reflexivity.
         SSSSCase "Z assignment command".
           apply E_Ass. reflexivity.
       SSSCase "while command".
         apply E_WhileEnd. reflexivity.
Qed.