:: by Andrzej Trybulec

::

:: Received May 19, 2013

:: Copyright (c) 2014-2017 Association of Mizar Users

definition

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

coherence

(((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of ;

;

end;
let I be MacroInstruction of SCM+FSA ;

func if=0 (a,I) -> Program of equals :: SCMFSA_X:def 1

(((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

correctness (((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

coherence

(((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of ;

;

:: deftheorem defines if=0 SCMFSA_X:def 1 :

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds if=0 (a,I) = (((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds if=0 (a,I) = (((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

definition

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

coherence

(((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of ;

;

end;
let I be MacroInstruction of SCM+FSA ;

func if>0 (a,I) -> Program of equals :: SCMFSA_X:def 2

(((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

correctness (((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

coherence

(((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of ;

;

:: deftheorem defines if>0 SCMFSA_X:def 2 :

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds if>0 (a,I) = (((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds if>0 (a,I) = (((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

Lm1: card (Stop SCM+FSA) = 1

by AFINSQ_1:34;

Lm2: (Stop SCM+FSA) . 0 = halt SCM+FSA

;

Lm3: 0 in dom (Stop SCM+FSA)

by COMPOS_1:3;

theorem Th1: :: SCMFSA_X:1

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds card (if=0 (a,I)) = (card I) + 4

for a being Int-Location holds card (if=0 (a,I)) = (card I) + 4

proof end;

theorem Th2: :: SCMFSA_X:2

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds card (if>0 (a,I)) = (card I) + 4

for a being Int-Location holds card (if>0 (a,I)) = (card I) + 4

proof end;

definition

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

coherence

(if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)) is Program of ;

;

coherence

(if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)) is Program of ;

;

end;
let I be MacroInstruction of SCM+FSA ;

func while=0 (a,I) -> Program of equals :: SCMFSA_X:def 3

(if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

correctness (if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

coherence

(if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)) is Program of ;

;

func while>0 (a,I) -> Program of equals :: SCMFSA_X:def 4

(if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

correctness (if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

coherence

(if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)) is Program of ;

;

:: deftheorem defines while=0 SCMFSA_X:def 3 :

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds while=0 (a,I) = (if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds while=0 (a,I) = (if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

:: deftheorem defines while>0 SCMFSA_X:def 4 :

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds while>0 (a,I) = (if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds while>0 (a,I) = (if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

theorem Th3: :: SCMFSA_X:3

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds card (while=0 (a,I)) = (card I) + 5

for a being Int-Location holds card (while=0 (a,I)) = (card I) + 5

proof end;

theorem Th4: :: SCMFSA_X:4

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds card (while>0 (a,I)) = (card I) + 5

for a being Int-Location holds card (while>0 (a,I)) = (card I) + 5

proof end;

theorem Th5: :: SCMFSA_X:5

for a being Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

k in dom (while=0 (a,I))

for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

k in dom (while=0 (a,I))

proof end;

theorem Th6: :: SCMFSA_X:6

for a being Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

(card I) + k in dom (while=0 (a,I))

for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

(card I) + k in dom (while=0 (a,I))

proof end;

theorem Th7: :: SCMFSA_X:7

for a being Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

k in dom (while>0 (a,I))

for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

k in dom (while>0 (a,I))

proof end;

theorem Th8: :: SCMFSA_X:8

for a being Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

(card I) + k in dom (while>0 (a,I))

for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

(card I) + k in dom (while>0 (a,I))

proof end;

theorem :: SCMFSA_X:9

theorem :: SCMFSA_X:10

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds

( (while=0 (a,I)) . 0 = a =0_goto 3 & (while=0 (a,I)) . 1 = goto 2 & (while>0 (a,I)) . 0 = a >0_goto 3 & (while>0 (a,I)) . 1 = goto 2 )

for I being MacroInstruction of SCM+FSA holds

( (while=0 (a,I)) . 0 = a =0_goto 3 & (while=0 (a,I)) . 1 = goto 2 & (while>0 (a,I)) . 0 = a >0_goto 3 & (while>0 (a,I)) . 1 = goto 2 )

proof end;

theorem :: SCMFSA_X:11

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . ((card I) + 4) = halt SCM+FSA

for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . ((card I) + 4) = halt SCM+FSA

proof end;

theorem :: SCMFSA_X:12

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . 2 = goto ((card I) + 4)

for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . 2 = goto ((card I) + 4)

proof end;

::$CT

theorem :: SCMFSA_X:14

for a being Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st k < (card I) + 5 holds

k in dom (while=0 (a,I))

for I being MacroInstruction of SCM+FSA

for k being Nat st k < (card I) + 5 holds

k in dom (while=0 (a,I))

proof end;

theorem :: SCMFSA_X:15

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . ((card I) + 2) = goto 0

for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . ((card I) + 2) = goto 0

proof end;

theorem :: SCMFSA_X:16

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . ((card I) + 4) = halt SCM+FSA

for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . ((card I) + 4) = halt SCM+FSA

proof end;

theorem :: SCMFSA_X:17

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . 2 = goto ((card I) + 4)

for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . 2 = goto ((card I) + 4)

proof end;

::$CT

theorem :: SCMFSA_X:19

for a being Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st k < (card I) + 5 holds

k in dom (while>0 (a,I))

for I being MacroInstruction of SCM+FSA

for k being Nat st k < (card I) + 5 holds

k in dom (while>0 (a,I))

proof end;

theorem :: SCMFSA_X:20

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . ((card I) + 2) = goto 0

for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . ((card I) + 2) = goto 0

proof end;

definition

let a be Int-Location;

let I be Program of ;

((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA) is Program of ;

end;
let I be Program of ;

func if<0 (a,I) -> Program of equals :: SCMFSA_X:def 5

((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA);

coherence ((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA);

((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA) is Program of ;

:: deftheorem defines if<0 SCMFSA_X:def 5 :

for a being Int-Location

for I being Program of holds if<0 (a,I) = ((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA);

for a being Int-Location

for I being Program of holds if<0 (a,I) = ((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA);

definition

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

coherence

(if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0)) is Program of ;

;

end;
let I be MacroInstruction of SCM+FSA ;

func while<0 (a,I) -> Program of equals :: SCMFSA_X:def 6

(if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0));

correctness (if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0));

coherence

(if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0)) is Program of ;

;

:: deftheorem defines while<0 SCMFSA_X:def 6 :

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds while<0 (a,I) = (if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0));

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds while<0 (a,I) = (if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0));

theorem :: SCMFSA_X:22

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds card (while<0 (a,I)) = (card I) + 6

for a being Int-Location holds card (while<0 (a,I)) = (card I) + 6

proof end;

theorem Th21: :: SCMFSA_X:23

for I being MacroInstruction of SCM+FSA

for i being No-StopCode Instruction of SCM+FSA

for n being Nat st n + 1 < card I holds

I +* (n,i) is MacroInstruction of SCM+FSA

for i being No-StopCode Instruction of SCM+FSA

for n being Nat st n + 1 < card I holds

I +* (n,i) is MacroInstruction of SCM+FSA

proof end;

registration

let I be MacroInstruction of SCM+FSA ;

let a be Int-Location;

coherence

( while=0 (a,I) is halt-ending & while=0 (a,I) is unique-halt )

( while>0 (a,I) is halt-ending & while>0 (a,I) is unique-halt )

end;
let a be Int-Location;

coherence

( while=0 (a,I) is halt-ending & while=0 (a,I) is unique-halt )

proof end;

coherence ( while>0 (a,I) is halt-ending & while>0 (a,I) is unique-halt )

proof end;

theorem Th22: :: SCMFSA_X:24

for I being really-closed MacroInstruction of SCM+FSA

for n, k being Nat st n < card I & k < card I holds

I +* (n,(goto k)) is really-closed

for n, k being Nat st n < card I & k < card I holds

I +* (n,(goto k)) is really-closed

proof end;

theorem Th24: :: SCMFSA_X:26

for I being really-closed Program of

for k being Nat st k <= card I holds

(Macro (goto k)) ';' I is really-closed

for k being Nat st k <= card I holds

(Macro (goto k)) ';' I is really-closed

proof end;

theorem Th25: :: SCMFSA_X:27

for I being really-closed MacroInstruction of SCM+FSA

for k being Nat st k <= card I holds

(Goto k) ";" I is really-closed

for k being Nat st k <= card I holds

(Goto k) ";" I is really-closed

proof end;

theorem Th26: :: SCMFSA_X:28

for I being really-closed Program of holds ((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA) is really-closed

proof end;

theorem Th27: :: SCMFSA_X:29

for I being really-closed MacroInstruction of SCM+FSA

for a being Int-Location

for k being Nat st k <= card I holds

(Macro (a =0_goto k)) ';' I is really-closed

for a being Int-Location

for k being Nat st k <= card I holds

(Macro (a =0_goto k)) ';' I is really-closed

proof end;

Lm4: for i being No-StopCode Instruction of SCM+FSA holds Directed (Macro i) = (Macro i) ';' (Goto 1)

proof end;

Lm5: for I being Program of

for k being Nat holds stop (I ';' (Goto k)) = I ';' (Macro (goto k))

proof end;

theorem Th28: :: SCMFSA_X:30

for I being really-closed MacroInstruction of SCM+FSA

for a being Int-Location

for k being Nat st k <= card I holds

(Macro (a >0_goto k)) ';' I is really-closed

for a being Int-Location

for k being Nat st k <= card I holds

(Macro (a >0_goto k)) ';' I is really-closed

proof end;

theorem Th29: :: SCMFSA_X:31

for I being really-closed MacroInstruction of SCM+FSA

for a being Int-Location

for k being Nat st k <= card I holds

(a =0_goto k) ";" I is really-closed

for a being Int-Location

for k being Nat st k <= card I holds

(a =0_goto k) ";" I is really-closed

proof end;

theorem Th30: :: SCMFSA_X:32

for I being really-closed MacroInstruction of SCM+FSA

for a being Int-Location

for k being Nat st k <= card I holds

(a >0_goto k) ";" I is really-closed

for a being Int-Location

for k being Nat st k <= card I holds

(a >0_goto k) ";" I is really-closed

proof end;

registration

let I be really-closed MacroInstruction of SCM+FSA ;

let a be Int-Location;

coherence

if=0 (a,I) is really-closed

if>0 (a,I) is really-closed

end;
let a be Int-Location;

coherence

if=0 (a,I) is really-closed

proof end;

coherence if>0 (a,I) is really-closed

proof end;

registration

let I be really-closed MacroInstruction of SCM+FSA ;

let a be Int-Location;

coherence

while=0 (a,I) is really-closed

while>0 (a,I) is really-closed

end;
let a be Int-Location;

coherence

while=0 (a,I) is really-closed

proof end;

coherence while>0 (a,I) is really-closed

proof end;

theorem :: SCMFSA_X:35

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds if=0 (a,(I ';' (goto 0))) = ((((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA)

for a being Int-Location holds if=0 (a,(I ';' (goto 0))) = ((((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA)

proof end;

theorem :: SCMFSA_X:36

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds if>0 (a,(I ';' (goto 0))) = ((((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA)

for a being Int-Location holds if>0 (a,(I ';' (goto 0))) = ((((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA)

proof end;