include "Csyntax.ma".
include "Csem.ma".

naxiom main : ident.
naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i).

ndefinition trivial : program.
@ [ 〈main, Internal ?〉 ] main [];
@ (Tint I32 Signed) [ ] [ ] (Sreturn (Some ??));
@ ? (Tint I32 Signed); napply (Econst_int zero);
nqed.

nremark trivial_behaves : ∃behaviour. exec_program trivial behaviour.
@; ##[ ##2:
  napply program_terminates;
  ##[ ##5: @; (* initial state *)
    ##[ ##3: nnormalize; nrewrite > (ident_eq_eq ?); //;
    ##| ##4: nnormalize; //;
    ##| ##*: ##skip
    ##] 
  ##| ##6:
    @2; ##[ ##4: napply step_internal_function;
          ##[ ##4: //;  ##| ##5: //; ##| ##*: ##skip ##] 
        ##| ##5: @2;
          ##[ ##4: napply step_return_1; //; napply nmk; #H; ndestruct;
          ##| ##5: @1; 
          ##| ##6: //;
          ##| ##*: ##skip ##]
        ##| ##6: //;
        ##| ##*: ##skip
        ##]
  ##| ##7: @;
  ##]
##] nqed.