pvsServer.tccs

%% TCCs associated with theory pvsServer
%% This file was automatically generated by PVS, please **do not modify** by hand.
pvsServer_TCCS: THEORY BEGIN

	% The disjointness TCC (at line 34, column 9) in decl nil for
	% term generated from enter
	%  COND st`mode = AWAIT_CMD -> LET st = st WITH [req := NULL_REQ] IN st,
	%      st`mode = READY -> LET st = st WITH [req := NULL_REQ] IN st,
	%      ELSE -> st
	% ENDCOND
	% was not generated because it simplifies to TRUE.
	% Disjointness TCC generated (at line 45, column 9) for
	% COND mode(st) = PARSING ->
	%        LET st = st WITH [defs := UPDATED_DEFS] IN st,
	%      mode(st) = READY ->
	%        LET st = st WITH [unsavedProof := FALSE] IN st,
	%      mode(st) = TYPECHECKING ->
	%        LET st = st WITH [defs := UPDATED_DEFS] IN st,
	%      ELSE -> st
	% ENDCOND
	  % proved
	leave_TCC1: OBLIGATION
	FORALL (m: Mode, st: State, st1: State):
	    st1 = st WITH [mode := m] IMPLIES
	     NOT (st1`mode = PARSING AND st1`mode = READY) AND
	      NOT (st1`mode = READY AND st1`mode = TYPECHECKING)
	
	% Disjointness TCC generated (at line 131, column 5) for
	% COND mode(st) = GET_PROOF_SCRIPT AND (typechecked(st) = TRUE) ->
	%        LET st = leave(GET_PROOF_SCRIPT)(st),
	%            st = st WITH [res := ERROR_PROOF_NOT_FOUND]
	%          IN enter(READY)(st),
	%      mode(st) = PARSING ->
	%        LET st = leave(PARSING)(st),
	%            st = st WITH [parsed := FALSE],
	%            st = st WITH [res := PARSE_ERROR]
	%          IN enter(READY)(st),
	%      mode(st) = TYPECHECKING ->
	%        LET st = leave(TYPECHECKING)(st),
	%            st = st WITH [typechecked := FALSE],
	%            st = st WITH [res := TYPECHECK_ERROR]
	%          IN enter(READY)(st),
	%      ELSE -> st
	% ENDCOND
	  % proved
	notify_ERROR_TCC1: OBLIGATION
	FORALL (st: (per_notify_ERROR)):
	    NOT ((st`mode = GET_PROOF_SCRIPT AND (st`typechecked = TRUE)) AND
	          st`mode = PARSING)
	     AND
	     NOT ((st`mode = GET_PROOF_SCRIPT AND (st`typechecked = TRUE)) AND
	           st`mode = TYPECHECKING)
	      AND NOT (st`mode = PARSING AND st`mode = TYPECHECKING)
	
	% Disjointness TCC generated (at line 192, column 5) for
	% COND mode(st) = START_PROVER AND (typechecked(st) = TRUE) ->
	%        LET st = leave(START_PROVER)(st),
	%            st = st WITH [res := SEQUENT_QED]
	%          IN enter(READY)(st),
	%      mode(st) = PROVING ->
	%        LET st = leave(PROVING)(st), st = st WITH [res := SEQUENT_QED]
	%          IN enter(SAVE_PROOF)(st),
	%      ELSE -> st
	% ENDCOND
	  % proved
	notify_QED_TCC1: OBLIGATION
	FORALL (st: (per_notify_QED)):
	    NOT ((st`mode = START_PROVER AND (st`typechecked = TRUE)) AND
	          st`mode = PROVING)
	
	% Disjointness TCC generated (at line 207, column 5) for
	% COND mode(st) = START_PROVER AND (typechecked(st) = TRUE) ->
	%        LET st = leave(START_PROVER)(st),
	%            st = st WITH [res := SEQUENT]
	%          IN enter(AWAIT_CMD)(st),
	%      mode(st) = PROVING ->
	%        LET st = leave(PROVING)(st), st = st WITH [res := SEQUENT] IN
	%          enter(AWAIT_CMD)(st),
	%      ELSE -> st
	% ENDCOND
	  % proved
	notify_SEQUENT_TCC1: OBLIGATION
	FORALL (st: (per_notify_SEQUENT)):
	    NOT ((st`mode = START_PROVER AND (st`typechecked = TRUE)) AND
	          st`mode = PROVING)
	
	% Disjointness TCC generated (at line 222, column 5) for
	% COND mode(st) = TYPECHECKING AND (previous_mode(st) = READY) ->
	%        LET st = leave(TYPECHECKING)(st),
	%            st = st WITH [typechecked := TRUE],
	%            st = st WITH [res := TYPECHECK_SUCCESS]
	%          IN enter(READY)(st),
	%      mode(st) = PARSING ->
	%        LET st = leave(PARSING)(st),
	%            st = st WITH [parsed := TRUE],
	%            st = st WITH [res := PARSE_SUCCESS]
	%          IN enter(READY)(st),
	%      ELSE -> st
	% ENDCOND
	  % proved
	notify_SUCCESS_TCC1: OBLIGATION
	FORALL (st: (per_notify_SUCCESS)):
	    NOT ((st`mode = TYPECHECKING AND (st`previous_mode = READY)) AND
	          st`mode = PARSING)
	
	% Disjointness TCC generated (at line 269, column 5) for
	% COND mode(st) = READY ->
	%        LET st = leave(READY)(st),
	%            st = st WITH [req := FILENAME_FORMULANAME]
	%          IN enter(GET_PROOF_SCRIPT)(st),
	%      mode(st) = AWAIT_CMD ->
	%        LET st = leave(AWAIT_CMD)(st),
	%            st = st WITH [res := ERROR_MUST_EXIT_PROVER_FIRST]
	%          IN enter(AWAIT_CMD)(st),
	%      ELSE -> st
	% ENDCOND
	  % proved
	proofScript_TCC1: OBLIGATION
	FORALL (st: (per_proofScript)): NOT (st`mode = READY AND st`mode = AWAIT_CMD)
	
	% Disjointness TCC generated (at line 284, column 5) for
	% COND mode(st) = READY ->
	%        LET st = leave(READY)(st),
	%            st = st WITH [req := FORMULANAME_FULLTHEORYNAME]
	%          IN enter(START_PROVER)(st),
	%      mode(st) = AWAIT_CMD ->
	%        LET st = leave(AWAIT_CMD)(st),
	%            st = st WITH [res := ERROR_MUST_EXIT_PROVER_FIRST]
	%          IN enter(AWAIT_CMD)(st),
	%      ELSE -> st
	% ENDCOND
	  % proved
	proveFormula_TCC1: OBLIGATION
	FORALL (st: (per_proveFormula)):
	    NOT (st`mode = READY AND st`mode = AWAIT_CMD)
	
	% Disjointness TCC generated (at line 329, column 5) for
	% COND mode(st) = INTERRUPTING ->
	%        LET st = leave(INTERRUPTING)(st) IN enter(PROVING)(st),
	%      mode(st) = SW_UPDATE ->
	%        LET st = leave(SW_UPDATE)(st) IN enter(READY)(st),
	%      mode(st) = TYPECHECKING AND
	%       (previous_mode(st) = GET_PROOF_SCRIPT)
	%        ->
	%        LET st = leave(TYPECHECKING)(st),
	%            st = st WITH [typechecked := TRUE]
	%          IN enter(GET_PROOF_SCRIPT)(st),
	%      mode(st) = TYPECHECKING AND (previous_mode(st) = TCCS) ->
	%        LET st = leave(TYPECHECKING)(st),
	%            st = st WITH [typechecked := TRUE]
	%          IN enter(TCCS)(st),
	%      mode(st) = TCCS AND (typechecked(st) = FALSE) ->
	%        LET st = leave(TCCS)(st) IN enter(TYPECHECKING)(st),
	%      mode(st) = TYPECHECKING AND (previous_mode(st) = START_PROVER)
	%        ->
	%        LET st = leave(TYPECHECKING)(st),
	%            st = st WITH [typechecked := TRUE]
	%          IN enter(START_PROVER)(st),
	%      mode(st) = WORKSPACE_UPDATE AND (req(st) = CLEAR) ->
	%        LET st = leave(WORKSPACE_UPDATE)(st),
	%            st = st WITH [defs := EMPTY],
	%            st = st WITH [parsed := FALSE],
	%            st = st WITH [typechecked := FALSE]
	%          IN enter(READY)(st),
	%      mode(st) = WORKSPACE_UPDATE AND (req(st) = FOLDERNAME) ->
	%        LET st = leave(WORKSPACE_UPDATE)(st),
	%            st = st WITH [res := FOLDERNAME]
	%          IN enter(READY)(st),
	%      mode(st) = GET_PROOF_SCRIPT AND (typechecked(st) = FALSE) ->
	%        LET st = leave(GET_PROOF_SCRIPT)(st) IN
	%          enter(TYPECHECKING)(st),
	%      mode(st) = START_PROVER AND (typechecked(st) = FALSE) ->
	%        LET st = leave(START_PROVER)(st) IN enter(TYPECHECKING)(st),
	%      mode(st) = FS_UPDATE ->
	%        LET st = leave(FS_UPDATE)(st),
	%            st = st WITH [parsed := FALSE],
	%            st = st WITH [typechecked := FALSE]
	%          IN enter(READY)(st),
	%      mode(st) = SAVE_PROOF ->
	%        LET st = leave(SAVE_PROOF)(st),
	%            st = st WITH [unsavedProof := FALSE]
	%          IN enter(READY)(st),
	%      ELSE -> st
	% ENDCOND
	  % proved
	tick_TCC1: OBLIGATION
	FORALL (st: (per_tick)):
	         (NOT (st`mode = INTERRUPTING AND st`mode = SW_UPDATE))
	     AND (NOT (st`mode = INTERRUPTING AND
	                st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT)))
	     AND (NOT (st`mode = INTERRUPTING AND
	                st`mode = TYPECHECKING AND (st`previous_mode = TCCS)))
	     AND (NOT (st`mode = INTERRUPTING AND
	                st`mode = TCCS AND (st`typechecked = FALSE)))
	     AND (NOT (st`mode = INTERRUPTING AND
	                st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER)))
	     AND (NOT (st`mode = INTERRUPTING AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)))
	     AND (NOT (st`mode = INTERRUPTING AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)))
	     AND (NOT (st`mode = INTERRUPTING AND
	                st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)))
	     AND (NOT (st`mode = INTERRUPTING AND
	                st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT (st`mode = INTERRUPTING AND st`mode = FS_UPDATE))
	     AND (NOT (st`mode = INTERRUPTING AND st`mode = SAVE_PROOF))
	     AND (NOT (st`mode = SW_UPDATE AND
	                st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT)))
	     AND (NOT (st`mode = SW_UPDATE AND
	                st`mode = TYPECHECKING AND (st`previous_mode = TCCS)))
	     AND (NOT (st`mode = SW_UPDATE AND
	                st`mode = TCCS AND (st`typechecked = FALSE)))
	     AND (NOT (st`mode = SW_UPDATE AND
	                st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER)))
	     AND (NOT (st`mode = SW_UPDATE AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)))
	     AND (NOT (st`mode = SW_UPDATE AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)))
	     AND (NOT (st`mode = SW_UPDATE AND
	                st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)))
	     AND (NOT (st`mode = SW_UPDATE AND
	                st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT (st`mode = SW_UPDATE AND st`mode = FS_UPDATE))
	     AND (NOT (st`mode = SW_UPDATE AND st`mode = SAVE_PROOF))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND st`mode = TYPECHECKING AND (st`previous_mode = TCCS)))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND st`mode = TCCS AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND
	                st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER)))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND st`mode = FS_UPDATE))
	     AND (NOT ((st`mode = TYPECHECKING AND
	                 (st`previous_mode = GET_PROOF_SCRIPT))
	                AND st`mode = SAVE_PROOF))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = TCCS)) AND
	                st`mode = TCCS AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = TCCS)) AND
	                st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = TCCS)) AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = TCCS)) AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = TCCS)) AND
	                st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = TCCS)) AND
	                st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = TCCS)) AND
	                st`mode = FS_UPDATE))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = TCCS)) AND
	                st`mode = SAVE_PROOF))
	     AND (NOT ((st`mode = TCCS AND (st`typechecked = FALSE)) AND
	                st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER)))
	     AND (NOT ((st`mode = TCCS AND (st`typechecked = FALSE)) AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)))
	     AND (NOT ((st`mode = TCCS AND (st`typechecked = FALSE)) AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)))
	     AND (NOT ((st`mode = TCCS AND (st`typechecked = FALSE)) AND
	                st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TCCS AND (st`typechecked = FALSE)) AND
	                st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TCCS AND (st`typechecked = FALSE)) AND
	                st`mode = FS_UPDATE))
	     AND (NOT ((st`mode = TCCS AND (st`typechecked = FALSE)) AND
	                st`mode = SAVE_PROOF))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER))
	                AND st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER))
	                AND st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER))
	                AND st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER))
	                AND st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER))
	                AND st`mode = FS_UPDATE))
	     AND (NOT ((st`mode = TYPECHECKING AND (st`previous_mode = START_PROVER))
	                AND st`mode = SAVE_PROOF))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)) AND
	                st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)) AND
	                st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)) AND
	                st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)) AND
	                st`mode = FS_UPDATE))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = CLEAR)) AND
	                st`mode = SAVE_PROOF))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)) AND
	                st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)) AND
	                st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)) AND
	                st`mode = FS_UPDATE))
	     AND (NOT ((st`mode = WORKSPACE_UPDATE AND (st`req = FOLDERNAME)) AND
	                st`mode = SAVE_PROOF))
	     AND (NOT ((st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)) AND
	                st`mode = START_PROVER AND (st`typechecked = FALSE)))
	     AND (NOT ((st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)) AND
	                st`mode = FS_UPDATE))
	     AND (NOT ((st`mode = GET_PROOF_SCRIPT AND (st`typechecked = FALSE)) AND
	                st`mode = SAVE_PROOF))
	     AND (NOT ((st`mode = START_PROVER AND (st`typechecked = FALSE)) AND
	                st`mode = FS_UPDATE))
	     AND (NOT ((st`mode = START_PROVER AND (st`typechecked = FALSE)) AND
	                st`mode = SAVE_PROOF))
	     AND NOT (st`mode = FS_UPDATE AND st`mode = SAVE_PROOF)

END pvsServer_TCCS